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 Symbolic Model Computational Model Implementations Conclusion

De
53 pages
Introduction Symbolic Model Computational Model Implementations Conclusion Security Protocol Verification: Symbolic and Computational Models Bruno Blanchet INRIA, Ecole Normale Superieure, CNRS March 2012 Bruno Blanchet (INRIA, ENS, CNRS) ETAPS March 2012 1 / 48

  • cryptographic primitives

  • computational models

  • verifying protocol

  • security protocols

  • model computational

  • basic cryptographic

  • model implementations

  • ecole normale


Voir plus Voir moins
Introduction
Bruno Blanchet
Symbolic Model
Security mbolic a
Sy
Computational Model
Implementations
Protocol Verification: nd Computational Mod
Bruno Blanchet
els
´ INRIA,EcoleNormaleSupe´rieure,CNRS Bruno.Blanchet@ens.fr
(INRIA, ENS, CNRS)
March 2012
ETAPS
March 2012
Conclusion
1 / 48
Introduction
Outline
1
2
3
4
5
Symbolic Model
Computational Model
Implementations
Introduction to security protocols Verifying protocols in the symbolic model Verifying protocols in the computational model Verifying protocol implementations Conclusion and future challenges
Bruno Blanchet (INRIA, ENS, CNRS)
ETAPS
March 2012
Conclusion
2 / 48
Introduction
Symbolic Model
Communications
A(Alice)
Bruno Blanchet
over
(INRIA, ENS, CNRS)
a
Computational Model
secure
network
secure network
ETAPS
Implementations
B
(Bob)
March 2012
Conclusion
3 / 48
Introduction
Symbolic Model
Computational Model
Implementations
Communications over anniesrecukortwne
A(Alice)
insecure network
B(Bob)
C(attacker) Atalks toBon an insecure network need for cryptography in order to make communications secure for instance, encrypt messages to preserve secrets.
Bruno Blanchet (INRIA, ENS, CNRS)
ETAPS
March 2012
Conclusion
4 / 48
Introduction
Symbolic Model
Cryptographic primitives
Computational Model
Implementations
Conclusion
Definition (Cryptographic primitives) Basic cryptographic algorithms, used as building blocks for protocols, e.g.encryptionandsignatures.
Bruno Blanchet (INRIA, ENS, CNRS)
ETAPS
March 2012
5 / 48