Provable Implementations of Security Protocols

  • Andy Gordon

Twenty First Annual IEEE Symposium on Logic in Computer Science (LICS 2006) |

Proving cryptographic security protocols has been a challenge ever since Needham and Schroeder threw down the gauntlet in their pioneering 1978 paper on authentication protocols: “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.” By now, there is a wide range of informal and formal methods that can catch most design errors. Still, as in other areas of software, the trouble is that while practitioners are typically happy for researchers to write formal models of their natural language specifications and to apply design principles, they are reluctant to do so themselves. In practice, specifications tend to be partial and ambiguous, and the implementation code is the closest we get to a formal description of most protocols. This motivates the subject of my talk: the relatively new enterprise of adapting formal methods for security protocols to work on code instead of abstract models. The goal is to lower the practical cost of security protocol verification by eliminating the need to write a separate formal model. I will describe current tools that partially address the problem, and discuss what remains to be done.