A new formal analysis of the Signal PQXDH protocol by Prosecco, Cryspen, and Signal using ProVerif and CryptoVerif
A new formal analysis of the Signal PQXDH protocol by Prosecco, Cryspen, and Signal using ProVerif and CryptoVerif
Internet Defense Prize and Distinguished Paper Awards at USENIX Security’23
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…
Distinguished paper award and test of time award at CSF’23
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…
New release CryptoVerif 2.07
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…
Distinguished paper award at CSF’22
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…
New release ProVerif 2.04
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…
New release ProVerif 2.03
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.…
New release CryptoVerif 2.05
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…
