Modelling Attacker's Knowledge for Cascade Cryptographic Protocols

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 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.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{Benassa08,
  author       = {Nazim Bena{\"{\i}}ssa},
  editor       = {Egon B{\"{o}}rger and
                  Michael J. Butler and
                  Jonathan P. Bowen and
                  Paul Boca},
  title        = {Modelling Attacker's Knowledge for Cascade Cryptographic Protocols},
  booktitle    = {Abstract State Machines, {B} and Z, First International Conference,
                  {ABZ} 2008, London, UK, September 16-18, 2008. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {5238},
  pages        = {251--264},
  publisher    = {Springer},
  year         = {2008},
  url          = {https://doi.org/10.1007/978-3-540-87603-8\_20},
  doi          = {10.1007/978-3-540-87603-8\_20},
  timestamp    = {Mon, 18 Apr 2022 18:26:24 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/Benassa08.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}