Modelling Attacker's Knowledge for Cascade Cryptographic Protocols

Nazim Benaissa 1
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We address the proof-based development of cryptographic protocols satisfying security properties. Communication channels are supposed to be unsafe. Analysing cryptographic protocols requires precise modelling of the attacker's knowledge. In this paper we use the event B modelling language to model the knowledge of the attacker for a class of cryptographic protocols called \textit{cascade protocols}. The attacker's behaviour conforms to the Dolev-Yao model. In the Dolev-Yao model, the attacker has full control of the communication channel, and the cryptographic primitives are supposed to be perfect.
Type de document :
Communication dans un congrès
Egon Börger and Michael Butler and Jonathan P. Bowen and Paul Boca. First International Conference on Abstract State Machines, B and Z - ABZ 2008, Sep 2008, London, United Kingdom. Springer, 5238, pp.251-264, 2008, Lecture Notes in Computer Science. 〈10.1007/978-3-540-87603-8_20〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00336641
Contributeur : Nazim Benaissa <>
Soumis le : mardi 4 novembre 2008 - 16:20:33
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52
Document(s) archivé(s) le : mardi 9 octobre 2012 - 15:00:57

Fichier

ABZ2008benaissa.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Nazim Benaissa. Modelling Attacker's Knowledge for Cascade Cryptographic Protocols. Egon Börger and Michael Butler and Jonathan P. Bowen and Paul Boca. First International Conference on Abstract State Machines, B and Z - ABZ 2008, Sep 2008, London, United Kingdom. Springer, 5238, pp.251-264, 2008, Lecture Notes in Computer Science. 〈10.1007/978-3-540-87603-8_20〉. 〈inria-00336641〉

Partager

Métriques

Consultations de la notice

145

Téléchargements de fichiers

128