Introduction Calculus Proof technique Example proof Conclusion
42
pages
English
Documents
Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus
Découvre YouScribe en t'inscrivant gratuitement
Découvre YouScribe en t'inscrivant gratuitement
42
pages
English
Documents
Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus
Introduction Calculus Proof technique Example proof Conclusion CryptoVerif: A Computationally Sound Mechanized Prover for Cryptographic Protocols Bruno Blanchet CNRS, Ecole Normale Superieure, INRIA, Paris July 2009 Bruno Blanchet (CNRS, ENS, INRIA) CryptoVerif July 2009 1 / 41
Voir
- cryptographic primitives
- errors can
- protocols has
- fully automatic
- security protocols
- protocols
- active research area
Bruno Blanchet
July 2009
CryptoVerif: A Computationally Sound Mechanized Prover for Cryptographic Protocols
´ CNRS,EcoleNormaleSupe´rieure,INRIA,Paris
1/491
Security protocols
41
The verification of security protocols has been and is still a very active research area. Their design iserror prone. Security errors arenot detectedby testing: they appear only in the presence of an adversary. Errors can haveserious consequences.
Security protocols are used for secure communications over an insecure network, such as Internet.
Examples: SSH, SSL/TLS, IPsec; wifi; mobile phone; e-voting protocols; . . .
20ly2/09nuBoalcnrB,ENS,INRhet(CNRS
Models of protocols: the formal model
Two models for security protocols: theformal modeland the computational model.
Formal model(so-called “Dolev-Yao model”): cryptographic primitives are ideal blackboxes messages are terms built from the cryptographic primitives the adversary is restricted to use only the primitives Proofscanbedoneautomatically,manyprotocolverifiersdothat.To name a few: FDR AVISPA (in fact, 4 protocol verifiers) Scyther ProVerif
0290/314erifJuly)CryptoVnolcsuoinqueExampleproofCulucorPsetfoinhcntIduroioctalnC
Features of ProVerif
Fully automatic. Works forunboundednumber of sessions and message space. Handles awide rangeof cryptographic primitives, defined by rewrite rules or equations. Handles varioussecurity properties authentication, some: secrecy, equivalences. Very precise: no false attack in our tests for secrecy and authentication. Relies on an abstract representation of protocols byHorn clausesand on a resolution algorithm on these clauses.
ly20094/oVerifJuC)AItpyrSNE,RNI,t(heRSCNoBunnclarB
