Invited Paper: Provable Implementations of Security Protocols (at LICS 2006)

Authors: Andrew D. Gordon

Abstract

Proving security protocols has been a challenge ever since Needham and Schroeder threw down the gauntlet in their pioneering 1978 paper: Protocols such as those developed here are prone to extremely subtle errors that are unlikely to be detected in normal operation. The need for techniques to verify the correctness of such protocols is great, and we encourage those interested in such problems to consider this area. [12] This may not seem such a grand challenge, at first, as most cryptographic protocols can be written in half a dozen lines and involve even fewer players; the twist is the intruder, who actively interferes with proceedings: We assume that an intruder can interpose a computer on all communication paths, and thus can alter or copy parts of messages, replay messages, or emit false material. [12]

BibTeX

  @InProceedings{Gordon-ProvableImplementat,
    author = 	 {Andrew D. Gordon},
    title = 	 {Provable Implementations of Security Protocols},
    booktitle =  {Proceedings of the Twenty-First Annual IEEE Symposium on Logic in Computer Science (LICS 2006)},
    year =	 {2006},
    month =	 {August}, 
    pages =      {345--346},
    location =   {Seattle, Washington, USA}, 
    note =       {Invited Talk},
    publisher =	 {IEEE Computer Society Press}
  }