Cet ouvrage fait partie de la bibliothèque YouScribe
Obtenez un accès à la bibliothèque pour le lire en ligne
En savoir plus

Introduction Calculus Proof technique Example proof Conclusion

De
42 pages
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

  • cryptographic primitives

  • errors can

  • protocols has

  • fully automatic

  • security protocols

  • protocols

  • active research area


Voir plus Voir moins
IntroductionCaluculPsorfoethcineEqumpxaprlefCoolcnooisunteC(nahconlBBurA)CrINRIENS,NRS,002yluJfireVotpy
Bruno Blanchet
July 2009
CryptoVerif: A Computationally Sound Mechanized Prover for Cryptographic Protocols
´ CNRS,EcoleNormaleSupe´rieure,INRIA,Paris
1/491
IortntcudethcinuqEeaxpmelionCalculusProofonfCooprniousclreVouJfiC)AItpyr
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
I,SNAIRNNC(tE,SRlaoBhencunBr
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,manyprotocolveriersdothat.To name a few: FDR AVISPA (in fact, 4 protocol verifiers) Scyther ProVerif
0290/314erifJuly)CryptoVnolcsuoinqueExampleproofCulucorPsetfoinhcntIduroioctalnC
lucurosPteofnichtnIudoroitclaCnonclusionuqEeaxpmelrpooCf14
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
Un pour Un
Permettre à tous d'accéder à la lecture
Pour chaque accès à la bibliothèque, YouScribe donne un accès à une personne dans le besoin