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 agreement for a certain binding if each time a principal completes a run of the protocol as a responder using , supposedly with , then there is a unique run of the protocol with the principal as initiator using , supposedly with .
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.