next up previous
Next: Assumptions Up: A First Step towards Previous: The Protocol Screener

Case Study: Automatic Generation of Authentication Protocols

 

In order to gain preliminary experience with APG, we perform a case study with automatic generation of two-party mutual authentication protocols. Authentication protocols are among the most widely used and intensely studied security protocols. Their complexity is suitable for an initial case study, and they are known to be notoriously difficult to design correctly and hence a good challenge [BAN89, Low96].

We use the agreement properties proposed by Gavin Lowe for authentication protocols as the formal definition of the authentication property [Low97]. A protocol guarantees a participant B agreement for a certain binding x if each time a principal B completes a run of the protocol as a responder using x, supposedly with A, then there is a unique run of the protocol with the principal A as initiator using x, supposedly with B.

In this section, we first discuss the assumptions we make in the case study. Then, we explain the difficulties we encountered in the case study and describe our enhancement techniques to overcome the difficulties. Finally, we summarize the experiment results and our findings.




next up previous
Next: Assumptions Up: A First Step towards Previous: The Protocol Screener

Adrian Perrig
Fri Sep 1 21:14:38 PDT 2000