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

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
Bruno Blanchet
July 2009
CryptoVerif: A Computationally Sound Mechanized Prover for Cryptographic Protocols
´ CNRS,EcoleNormaleSupe´rieure,INRIA,Paris
Security protocols
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; . . .
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
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.
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