GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-01 16:42:56 +03:00
Code Issues Projects Releases Wiki Activity

add note about solvers for ZUC theorem

Browse Source
This commit is contained in:
Adam C. Foltzer 2014-09-08 14:45:01 -07:00
parent b2f0e3db4e
commit a0bb572388
1 changed files with 3 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
examples/ZUC.cry
View File

@ -300,7 +300,9 @@ property LoadKey_TestVectors =
// cuts down on the problem size and is sufficient to ensure the iv's will be // cuts down on the problem size and is sufficient to ensure the iv's will be
// the same. That is, if this theorem fails, then so would the final iv's used // the same. That is, if this theorem fails, then so would the final iv's used
// by ZUC. // by ZUC.
property ZUC_isResistantToCollisionAttack (k, iv1, iv2) = //
// Use a solver other than CVC4; Z3 and Boolector do it quickly.
property ZUC_isResistantToCollisionAttack k iv1 iv2 =
if iv1 != iv2 if iv1 != iv2
then InitializeZUC (k, iv1) @ 1 != InitializeZUC (k, iv2) @ 1 then InitializeZUC (k, iv1) @ 1 != InitializeZUC (k, iv2) @ 1
else True else True