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…
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.…
Download on the CryptoVerif page Changes since the previous release: – Allow comparisons between indices and tables (insert, get) in the right-hand side of equiv declarations. – Optimize the right-hand side of equiv declarations by removing useless assignments. – Allow new and event_abort in conditions of find and get. – Allow…
