Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Primitive::Asymmetric::Cipher::RSA's IntegerRSACorrectKeyGen property take an extraordinarily long time to :check #204

Open
RyanGlScott opened this issue Dec 9, 2024 · 0 comments

Comments

@RyanGlScott
Copy link
Contributor

If you attempt to :check the properties in Primitive::Asymmetric::Cipher::RSA, it will take an extremely long to complete:

$ ~/Software/cryptol-3.2.0/bin/cryptol Primitive/Asymmetric/Cipher/RSA.cry -c ":check"
Loading module Cryptol
Loading module Common::bv
Loading module Common::mod_arith
Loading module Primitive::Asymmetric::Cipher::RSA
property I2OSConversionCorrect Showing a specific instance of polymorphic result:
  * Using '1' for signature variable 'xLen'
Using random testing.
Testing... Passed 100 tests.
Expected test coverage: 32.39% (83 of 256 values)
property RSACorrect Showing a specific instance of polymorphic result:
  * Using '1' for signature variable 'K'
Using exhaustive testing.
Testing... ERROR for the following inputs:
RSACorrect 0x0 0x0 0x1 0x0 ~> ERROR
Run-time error: ciphertext representative out of range
-- Backtrace --
Cryptol::error called at Primitive/Asymmetric/Cipher/RSA.cry:39:50--39:55
Primitive::Asymmetric::Cipher::RSA::RSADP called at Primitive/Asymmetric/Cipher/RSA.cry:45:64--45:69
(Cryptol::==) called at Primitive/Asymmetric/Cipher/RSA.cry:45:33--45:104
(Cryptol::==>) called at Primitive/Asymmetric/Cipher/RSA.cry:45:33--45:104
Primitive::Asymmetric::Cipher::RSA::RSACorrect
<interactive>::it
property testsPass Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property IntegerRSACorrectKeyGen Using random testing.
Testing...

Specifically, the IntegerRSACorrectKeyGen property seems to take well over an hour to :check. (I did not attempt to wait for the tests to complete after that.)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant