Download on the CryptoVerif page
Changes since the last release:
– Library of primitives:
– added macros for primitives without security assumption (useful to model broken primitives; e.g., classical schemes in the presence of a quantum adversary).
– added macros for IND-CPA public key encryption, KEMs (Key Encapsulation Mechanisms), fixed-generator GDH, strong DH, and fixed-hash collision-resistant hash functions. (The latter make sense only against a fixed adversary.)
– replaced the PRF-ODH macros with more parametric macros.
– built a separate library for assumptions valid against a quantum adversary (pq.cvl, pq.ocvl).
– cv2fstar:
– run in proof mode before generating F* code, to collect the proved queries.
– for indistinguishability and diff-indistinguishability, generate 2 implementations, one for each process.
– fixed bug that happened when no return has following oracles.
– made the filter type explicit in the translation of get, because F* cannot always infer it.
– cv2OCaml: for indistinguishability and diff-indistinguishability, generate code for the first process (assumed to be the protocol, while the second one is assumed to be a specification).
– Allow naming equations and collisions, added option [manual] for equations and collisions to deactivate them at the beginning, and added command “use” to activate or deactivate equations, collisions, and “equiv” statements.
– Allow functions defined by letfun in equations, collisions, and queries.
– When a query is encoded as another query (reachability secrecy, diff-indistinguishability), remember the original query and display it on the RESULT line.
– Fixed bug that occurred when several branches of find use the same indices.
– Fixed bug in encoding of query secret x [reachability], which made x public for other queries.
– When the diff[.,.] construct is used, for all queries except the indistinguishability between the first and second argument of diff, we assume that the adversary knows whether the first or the second argument of diff is used.
