Download on the CryptoVerif page Changes since the last release: Ghost types; computations of ghost types and useless events and tables are removed when generating F* or OCaml implementations. cv2fstar: add an invariant preserved by all oracle functions, to be defined and proved by the user (by default, always True) axiomatize that…
Download on the CryptoVerif page Changes since the last release: cv2fstar: use an effect to make sure the generated code is used correctly. translate the security properties proved in CryptoVerif into F* axioms. fixed bug when the name of the table file is not the same as thename of the table. fixed…
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…
A new formal analysis of the Signal PQXDH protocol by Prosecco, Cryspen, and Signal using ProVerif and CryptoVerif
Our paper “TreeSync: Authenticated Group Management for Messaging Layer Security” by Théophile Wallez, Inria Paris; Jonathan Protzenko, Microsoft Research; Benjamin Beurdouche, Mozilla; Karthikeyan Bhargavan, Inria Paris was awarded an Internet Defense Prize at USENIX Security’23. Our papers also received 3 distinguished paper awards at USENIX Security’23. In addition to the…
The paper Indistinguishability Beyond Diff-Equivalence in ProVerifby Vincent Cheval and Itsaka Rakotonirina received a Distinguished Paper Awardat IEEE CSF 2023. The paper An Efficient Cryptographic Protocol Verifier Based on Prolog Rulesby Bruno Blanchet, published at CSFW 2001, received a Test of Time Award atIEEE CSF 2023. This paper was the…
Download on the CryptoVerif page Changes since the previous release: Translation of CryptoVerif models into F* implementations, byBenjamin Lipp. (More documentation and the translation ofproperties 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…
Recent work by Adrien Koutsos and his co-authors received the Distinguished Paper Award at IEEE CSF 2022 (part of FLOC): Cracking the Stateful Nut: Computational Proofs of Stateful Security Protocols using the SQUIRREL Proof Assistant with D. Baelde, S. Delaune, A. Koutsos and S. Moreau. The pre-print is available on…
Download on the ProVerif page. Changes since the previous release: – Improved optimisation transforming mess facts into attacker facts when the channel is a public term and not only a public name. – Allow nested comments in the input file. All comments must be closed. ProVerif will raise an error…
Download on the ProVerif page. Changes since the previous release: – Events that occur in the conclusion of a lemma and also as an injective event in the main query are not ignored anymore when applying the lemma. – Replace attacker(fail-any,x) or attacker(x,fail-any) with bad in the conclusion of clauses.…
