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.
