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
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.…
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…