Download on the CryptoVerif page
Changes since the previous release:
- Translation of CryptoVerif models into F* implementations, by
Benjamin Lipp. (More documentation and the translation of
properties proved in CryptoVerif into F* axioms will be added later.) - Added notions of secrecy as reachability and secrecy for a bit.
- Added predefined function if_fun, such that if_fun(true,x,y) = x
and if_fun(false,x,y) = y. - Added transformation move_if_fun.
- Added function option autoSwapIf, which moves an if_fun as argument
of the function to outside the function. - Added diff[.,.] construct, to show indistinguishability between
the process that uses the first argument of diff and the one that
uses the second argument, as in ProVerif. - Allow [onesession] as synonym of [cv_onesession].
- Added command “move up x_1 … x_n to occ” to move random number
generations or assignments upwards in the game. - Added universal one-way hash functions to the library of primitives.
- Allow explicit quantifiers in correspondence queries:
forall xi:Ti; … ==> exists yj:T’j; …
and the existential quantifiers can occur anywhere after ==>.
(This is now the recommended syntax. The old syntax is still
accepted for compatibility.) - Allow _ in patterns.
- Allow proving [unique] after some game transformations.
- As a consequence, removed setting allowUnprovedUnique.
- The command [move] now supports non-expanded games, but
still moves only new and let that occur at the process level. - Removed command “remove_assign all”, useless in practice.
- New command “SArename random”, previously included in “remove_assign”.
- Added option “no_test” to the commands “guess” and “guess_branch”
to assert that we use the guessed value resp. are in the guessed
branch, instead of testing it. - Use program points more often in the collection of true facts,
in addition or instead of defined variables. - Display a warning when correspondence queries do not satisfy a
well-formedness condition (the conclusion of the correspondence must
be uniquely determined given the events in the hypothesis). - Display probability when one-session secrecy is proved.
- No need to double the probabilities in “success” for (one-session) secrecy.
- Fixed bugs related to the fact that terms may abort.
- Fixed bugs in success simplify: minor precision improvement
with query event(e(M)) ==> false; when distinguishing cases in
the proof of correspondences, it may have forgotten some cases;
add the probability for the proved cases; always consider the
proof of independence for secrecy queries, even if one-session
secrecy cannot be proved; fixed internal error when there is
no query. - Fixed bugs in guess transformation: injectivity was proved in the
initial game instead of the current game; use compatibility
information between program points to prove injectivity;
apply guess also to the queries that prove find[unique];
fixed internal error in command “guess x” when x has array indices;
reprove unicity of find in case secrecy queries are present;
allow guessing value of a variable defined in a term;
improved probability when several correspondence queries can be
considered together, in guess variable and guess_branch. - Fixed bug in guess_branch transformation: branches of find were not
computed correctly. - Fixed bug: use only facts independent from x when eliminating
indices in computation of probability of a collision that relies on
the random variable x. - Fixed bug in proof of injectivity when there are several events
before ==>. - Fixed bug: events were not preserved in the initial transformation
of the RHS in equivalence proofs. - Fixed bug in SArename that could cause an internal error.
- Fixed 4 bugs in the pre-treatment of equiv statements.
- Fixed bugs in probability counting: avoid counting spurious
collisions of previous transformations in globaldepanal;
do the proof of secrecy in one step to avoid counting twice the
same collisions. - Fixed internal error with physically equal terms in the left-hand
side of equiv statements.
