next up previous
Next: Impersonation attempt Up: Case Study: Automatic Generation Previous: Assumptions

Adding the Pruning Algorithm to the Protocol Generator

As we mentioned before, a naïve approach generates a large number of uninteresting candidate protocols. In Table 1 we show that the naïve approach generates tens of thousands of candidate protocols in the real experiments. Generating a large number of flawed candidate protocols risks to render APG impractical, since the running time of the protocol screener would be prohibitive. To deal with this problem, we define a pruning algorithm for each security property, which efficiently prunes the majority of the flawed protocols. This pruning algorithm can either operate on the message level or on the protocol level. A secrecy property, for instance, can be verified on the message level, since the secret value cannot be disclosed publically in any message. In the case of the authentication property, however, the pruning algorithm works on the protocol level, since it is difficult to define a message-level pruning algorithm which does not violate completeness (i.e. preserves correct protocols). To quickly discard flawed authentication protocols, we use an intruder module which checks for impersonation and simple replay attacks. As Table 1 shows, these two mechanisms reduce 98 percent of the candidate protocols in real experiments.


next up previous
Next: Impersonation attempt Up: Case Study: Automatic Generation Previous: Assumptions

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