New releases: ProVerif version 2.00 and CryptoVerif version 2.00

Dear all,

New releases of both ProVerif and CryptoVerif are available,
numbered 2.00. They can be found at the usual places:

The main novelty in these releases is that a lot of effort
has been made so that the tools are compatible: a large subset of
the language is accepted by both tools, which allows you
to use the same or very similar files as input to both tools.
More details can be found in Section 6.4 of the ProVerif manual.

Common examples are found in the ProVerif distribution
in directory examples/cryptoverif. You can run them by
./proverif -lib cryptoverif.pvl examples/cryptoverif/.pcv
in the main ProVerif directory. (If you install ProVerif via opam,
the examples are in .opam//doc/proverif/examples/cryptoverif
and the cryptographic library cryptoverif.pvl is in
.opam//share/proverif/cryptoverif.pvl )

These examples can also be found in the CryptoVerif distribution
in directory examples/basic. You can run them by
./cryptoverif examples/basic/.pcv
in the main CryptoVerif directory.

For ProVerif, the changes are extensions; they preserve
compatibility with previous versions, except for a few
additional keywords and other very minor changes.
For CryptoVerif, there are major incompatible changes. A converter
from CryptoVerif 1.28 is provided in the CryptoVerif distribution.
Major improvements have also been made to the library of
cryptographic primitives.


Full list of changes in ProVerif:

  • New keywords in the typed pi calculus front-end:
    do, foreach, implementation, public_vars, secret
    These keywords cannot be used as identifiers.
  • Identifiers of processes (in declarations "let P(…) = ")
    must be distinct from other identifiers.
  • Allow the conjunction of several events or facts before the
    arrow ==> in queries.
  • Interactive simulator:
    • Display events and public terms in order of addition.
    • Show the recipe used to compute a term in the list of public terms,
      when terms are added to public terms.
    • Allow zooming in the graphical trace display.
    • Show fresh names created by the adversary and public terms
      computed by the adversary in the graphical trace display.
    • When the user needs to enter a recipe, display the list of terms,
      so that he has enough information.
    • Button “Forward” to redo a step undone by the “Backward” button.
  • Compatibility with CryptoVerif
    • Allow
      a <-R T; P as a synonym of new a: T; P
      x[:T] <- M; P as a synonym of let x[:T] = M in P
      foreach i <= N do P as a synonym of ! i <= N P and of ! P
    • Allow and ignore CryptoVerif implementation annotations
    • Allow disequations “equation forall x1:T1, …, xn:Tn; M1 <> M2.”
      and just check that they are valid.
    • Support for event, get, insert in terms (by expansion into processes)
    • New queries:
      query secret x.
      query secret x [real_or_random].
      to test the secrecy of a bound variable or name x.
    • Allow public variables in correspondence and secrecy queries, e.g.:
      query event(e1) ==> event(e2) public_vars x1,…,xn.
      query secret x public_vars x1,…,xn.
  • Fixed bug that could cause the addition of a spurious edge,
    when a replication is executed just after a box in the graphical
    display of traces.
  • Fixed bug: trace reconstruction failed abnormally in the absence
    of free names.
  • Display an error message instead of looping when there is a recursive
    macro in the pi calculus front-end without types.

Full list of changes in CryptoVerif:

  • Improved simplification of terms, in particular in the presence
    of boolean variables.

  • Exploit the information of complex conditions of find
    (themselves containing let, if, or find).

  • During the crypto transformation, do not transform a random variable
    that appears in an event and that is marked [unchanged] in the
    transformation using an oracle with priority > priorityEventUnchangedRand
    (default: 5), prefer leaving it unchanged.

  • New front-end, for improved compatibility with ProVerif.
    The main syntax changes are as follows:

    • “define” becomes “def”
    • “[compos]” becomes “[data]”
    • “[decompos]” becomes “[projection]”
    • “equation structure(id1, …, idn).” becomes
      “equation builtin structure(id1, …, idn).”
    • “forall x1:t1, …, xn:tn; M.” becomes
      “equation forall x1:t1, …, xn:tn; M.”
    • “query secret1 x.” becomes “query secret x [cv_onesession].”
    • The syntax of correspondences is now the ProVerif syntax:
      For instance, “query event e1(…) ==> e2(…).”
      becomes “query event(e1(…)) ==> event(e2(…)).”
      and “query event inj:e1(…) ==> inj:e2(…).”
      becomes “query inj-event(e1(…)) ==> inj-event(e2(…)).”
      If there are public variables, they must be explicitly indicated
      in the correspondences, by adding “pub_vars x1,…,xn” at the
      end of the query. (In previous versions, CryptoVerif
      implicitly considered as public variables in correspondences
      the variables on which secrecy queries were present.)
    • Equivalences use the syntax of the oracles front-end,
      even in the channels front-end.
      (Oracles must always be named; oracles must conclude with
      return(M) instead of just M; oracles are separated by
      parallel compositions, not by commas.)
      The names of equivalences must be between parentheses:
      “equiv(name) …” or “equiv(name(f)) …”
    • Collisions use the syntax of the oracles front-end,
      even in the channels front-end:
      “collision new x1:T1; … new xn:Tn; forall y1:T1’, …, ym:Tm’; M1 <=§=> M2.”
      “collision new x1:T1; … new xn:Tn; forall y1:T1’, …, ym:Tm’; return(M1) <=§=> return(M2).”
    • Processes are parametric: if a process macro P, defined by
      “let P = …” uses variables defined before the usage of P,
      then these variables must now be passed as argument to P:
      “let P(x1:T1,…,xn:Tn) = …”, used by “P(M1,…,Mn)” in the
      channels front-end and by “run P(M1,…,Mn)” in the oracles
    • Both front-ends allow the synonym constructs
      “! i<=N” and “forall i <= N do” for replication,
      “new x:T” and “x <-R T” for random-number generation, and
      “let x = M in N” and “x <-M; N” for assignment.
      The oracle front-end now uses “yield” instead of “end”
      (like the channels front-end).
  • The library of cryptographic primitives has been revised:

    • Symmetric-key primitives no longer use a key generation
    • Probabilistic primitives choose random coins internally
      (using “letfun”), so the user does not have to choose them
    • IND-CCA2 public-key encryption may leak the length of the cleartext.
    • Added equivalences that allow to transform manually only some
      occurrences of encryption for IND-CCA2 encryption,
      of decryption for INT-PTXT encryption,
      of MAC verification for MACs,
      of signature verification for signatures.
    • Added probabilistic MACs, deterministic signatures,
      and renamed the macros as a consequence.
    • Added AEAD, possibly with a nonce (e.g. AES-GCM).
    • Added square_CDH, square_DDH, square_GDH, and
    • Added macros for combinations of primitives,
      building authenticated encryption from encrypt-then-MAC,
      from AEAD, or from AEAD_nonce, and AEAD from encrypt-then-MAC
      or from AEAD_nonce.
  • An automatic converter from CryptoVerif 1.28 to CryptoVerif 2.00
    is provided. It converts the front-end changes, but not the changes
    in the cryptographic library. As a consequence, converted
    examples need to be run using a converted version of the old
    cryptographic library.

    ./convert [-lib <lib_filename>] [-in channels|-in oracles] [-olib <lib_output_filename>] -o <output_filename>
    This command converts the into <output_filename>.
    (This command should be run in the main CryptoVerif directory.)
    The setting “-in channels” or “-in oracles” chooses the front-end to
    use. It allows the user to override the default (“channels” when
    ends in .cv and “oracles” when ends in .ocv).
    If “-lib <lib_filename>” is present, it uses <lib_filename> as
    CryptoVerif 1.28 library of cryptographic primitives. Otherwise, it
    uses the default CryptoVerif 1.28 library of cryptographic
    If “-olib <lib_output_filename>” is present, it outputs the
    converted library of primitives into <lib_output_filename>.
    The suffix “.cvl” or “.ocvl” is automatically added to all library
    filenames (depending on the front-end in use), the user should not
    include it.

    The converted examples can be run by
    ./cryptoverif -lib converter/default-converted <converted_filename>
    when they use the default CryptoVerif 1.28 library.
    (This command should be run in the main CryptoVerif directory.)
    Otherwise, use the converted library built by ./convert.

  • Option -oproof to output the proof in
    instead of displaying it on the standard output.

1 Like