Download on the CryptoVerif page

Changes since the previous release:

– Allow comparisons between indices and tables (insert, get)

in the right-hand side of equiv declarations.

– Optimize the right-hand side of equiv declarations by removing

useless assignments.

– Allow new and event_abort in conditions of find and get.

– Allow get[unique] (which is transformed into find[unique]).

– CryptoVerif proves that the get[unique] and find[unique] in the initial

game are really unique.

– Added definitions of Diffie-Hellman properties with a single

family of exponents, in the standard library of cryptographic primitives.

– Allow “min(<probability>, …, <probability>)”, “<probability>^<integer>”,

and “optim-if <condition> then <probability> else <probability>”

in probability formulas.

– Improved the computation of the runtime of the context when

adding a replication on top of an “equiv” declaration (using “optim-if”).

– In a “proba” declaration, allow the user to specify the dimensions of

the arguments of the probability function.

– CryptoVerif now checks that calls to the same probability function

have the same number of arguments and compatible dimensions.

– Added the “letproba” declaration to define probability functions.

– Nicer probability formulas: write A – B instead of A + -B;

group some time formulas.

– Added a macro for DDH with random self reducibility in the standard

library of cryptographic primitives (it is more limited than other DDH

macros).

– Allow multiple command-line options “-lib <file>”.

– Improvement of some error messages (suggestion of Benjamin Lipp).

– Avoid creating duplicate defined conditions in transformation

remove_assign.

– Minor improvement of the precision of the treatment of else

conditions of find.

– Improved test infrastructure: allow setting a timeout on tests.

– Removed option optimizeVars.

– Reimplemented the counting of calls to oracles in the crypto transformation,

to make it more precise and fix two bugs.

– Revised the command “allowed_collisions”: the form

“allowed_collisions <formulas>” applies to both collisions between

terms and collision statements without using the “collision” keyword;

the list of formulas may be empty; formulas may be 1/pest when there is

no factor.

– Fixed bug in query_equiv: undone the optimization of the translation

that avoids creating oracles that just generate random values before

a single oracle; this optimization was not sound in general.

– Fixed several bugs in generation of OCaml implementations:

* a non-existing file is now considered as an empty table (reported

by Benjamin Lipp).

* serialization and deserialization functions were swapped for

types bool and bitstringbot (fixed by Benjamin Lipp).

* the order of evaluation of terms was sometimes incorrect for terms

that contain insert/get/event_abort

* let pat = M in yield else p executed p even when the pattern-matching

succeeded

* fixed syntax error in the translation of get terms

* inside events, do not ignore event_abort as well as insert even when it

appears via a call to a letfun

– Fixed bug in computation of indices in crypto transformation.

– Fixed bug in update of defined conditions following other

rewritings of the game: it supported only expanded games, but

was sometimes called on non-expanded games.

– Fixed bug with negation in extraction of information from terms containing

if/let/find/new/event_abort.

– Fixed internal error: else case of a let term was missing in transformation

of insert/get into find.

– Fixed probabilities in GDH, square GDH and PRF-ODH.

– Fixed bug in probabilities: when a collision statement was applied

together with a crypto transformation, there was confusion between

the time of the adversary against the collision statement and the one

against the crypto transformation.