New release CryptoVerif 2.07

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.

Comments are closed.