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.