Our protocol generator generates candidate protocols that satisfy the specified system specification and discards obviously flawed protocols at an early stage. Intuitively, the protocol space is infinite. To solve this problem is to use iterative deepening, a standard search technique. In each iteration, we set a cost threshold of protocols. We then search through the protocol space to generate all the protocols below the given cost threshold. After sorting the protocols, the protocol screener tests them in the order of increasing cost. If one protocol satisfies the desired properties, it is minimal with respect to the cost metric function given by the user and the generation process stops. Otherwise, we increase the cost threshold and generate more protocols.
A simple three-party authentication and key distribution protocol has a protocol space of order . Our protocol generator generates and analyzes protocols per second, which would take over three years to explore the entire space. We have developed powerful protocol space reduction techniques to prune the search tree at an early stage. With these pruning techniques, it only takes the protocol generator a few hours to scan through the protocol space of order . More details are included in [PS00a, PS00b].