Dear all,
New releases of both ProVerif and CryptoVerif are available,
numbered 2.00. They can be found at the usual places:
-
ProVerif is available at http://proverif.inria.fr
It is also available via opam. -
CryptoVerif is available at http://cryptoverif.inria.fr
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.
Enjoy!
-Bruno
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.
- Allow
- 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.”
becomes
“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
front-end. - 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
function. - Probabilistic primitives choose random coins internally
(using “letfun”), so the user does not have to choose them
explicitly. - 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
square_GDH_prime_order. - 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.
- Symmetric-key primitives no longer use a key generation
-
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.Usage:
./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
primitives.
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.