7 jours d'essai offerts
Cet ouvrage et des milliers d'autres sont disponibles en abonnement pour 8,99€/mois
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