ProVerif
ProVerif is an automatic cryptographic protocol verifier, in the formal model (so called Dolev-Yao model). This protocol verifier is based on a representation of the protocol by Horn clauses. Its main features are: It can handle many different cryptographic primitives, including shared- and public-key cryptography (encryption and signatures), hash functions, and Diffie-Hellman key agreements, specified both as rewrite rules or as equations. It can handle an unbounded number of sessions of the protocol (even in parallel) and an unbounded message space. This result has been obtained thanks to some well-chosen approximations. This means that the verifier can give false attacks, but if it claims that the protocol satisfies some property, then the property is actually satisfied. With Andreas Podelski, we have shown that the considered resolution algorithm terminates on a large class of protocols (the so-called ”tagged” protocols, FoSSaCS’03 and TCS). With Xavier Allamigeon, we have implemented attack reconstruction: when the tool cannot prove a property, it tries to reconstruct an attack, that is, an execution trace of the protocol that falsifies the desired property (CSFW’05). This verifier can prove the following properties: secrecy (the adversary cannot obtain the secret, CSFW’01), authentication (SAS’02) and more generally correspondence properties (SAS’03, with Martín Abadi), strong secrecy (the adversary does not see the difference when the value of the secret changes, Oakland’04), equivalences between processes that differ only by terms (LICS’05 with Martín Abadi and Cédric Fournet)
Keywords for this software
References in zbMATH (referenced in 19 articles )
Showing results 1 to 19 of 19.
Sorted by year (- Chen, Chen; Jia, Limin; Xu, Hao; Luo, Cheng; Zhou, Wenchao; Loo, Boon Thau: A program logic for verifying secure routing protocols (2015)
- Bansal, Chetan; Bhargavan, Karthikeyan; Delignat-Lavaud, Antoine; Maffeis, Sergio: Keys to the cloud: formal analysis and concrete attacks on encrypted web storage (2013)
- Baudet, Mathieu; Cortier, Véronique; Delaune, Stéphanie: YAPA: a generic tool for computing intruder knowledge (2013)
- Mateescu, Radu; Salaün, Gwen: PIC2LNT: model transformation for model checking an applied pi-calculus (2013)
- Arapinis, Myrto; Bursuc, Sergiu; Ryan, Mark: Privacy supporting cloud computing: ConfiChair, a case study (2012)
- Arapinis, Myrto; Bursuc, Sergiu; Ryan, Mark D.: Reduction of equational theories for verification of trace equivalence: re-encryption, associativity and commutativity (2012)
- Blanchet, Bruno: Security protocol verification: symbolic and computational models (2012)
- Cortier, Véronique; Degrieck, Jan; Delaune, Stéphanie: Analysing routing protocols: four nodes topologies are sufficient (2012)
- Cortier, Véronique; Wiedling, Cyrille: A formal analysis of the Norwegian e-voting protocol (2012)
- Luu, Anh Tuan; Sun, Jun; Liu, Yang; Dong, Jin Song: SeVe: automatic tool for verification of security protocols (2012)
- Paiola, Miriam; Blanchet, Bruno: Verification of security protocols with lists: from length one to unbounded length (2012)
- Canetti, Ran; Herzog, Jonathan: Universally composable symbolic security analysis (2011)
- Küsters, Ralf; Truderung, Tomasz: Reducing protocol analysis with XOR to the XOR-free case in the Horn theory based approach (2011)
- Baudet, Mathieu; Cortier, Véronique; Delaune, Stéphanie: YAPA: a generic tool for computing intruder knowledge (2009)
- Blanchet, Bruno; Abadi, Martín; Fournet, Cédric: Automated verification of selected equivalences for security protocols (2008)
- Bhargavan, Karthikeyan; Fournet, Cédric; Gordon, Andrew D.; Tse, Stephen: Verified interoperable implementations of security protocols (2007)
- Cervesato, Iliano; Stehr, Mark-Oliver: Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types (2007)
- Canetti, Ran; Herzog, Jonathan: Universally composable symbolic analysis of mutual authentication and key-exchange protocols (2006)
- Kremer, Steve; Ryan, Mark: Analysis of an electronic voting protocol in the applied pi calculus (2005)