The purpose of the protocol generator is to generate candidate protocols that satisfy the specified system requirements. Intuitively, the protocol space is infinite. Hence, we need a way to limit the number of candidate protocols generated while not omitting any potential optimal protocols.
Our primary method to solve this problem is to use iterative deepening, a standard search technique [RN95]. 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 and the generation process can stop. Otherwise, we increase the cost threshold and generate more protocols.
It is intuitive and our experiments confirmed that the number of protocols generated is exponential in the value of the cost threshold. Hence, the protocol generator can easily generate millions of protocols. Since elaborate protocol verification takes on the order of 1 second per protocol, it would be impractical for the protocol screener to analyze all of these protocols. To make APG practical we use efficient reduction techniques and heuristics to prune invalid candidate protocols early to reduce the number of candidate protocols passed to the protocol screener. Most of the generated protocols contain severe security flaws which can be detected with a simple and more efficient verification algorithm. Each security property that is supported by the system is therefore accompanied by a pruning algorithm (which efficiently discards most severely flawed protocols) and a verification condition for the screener. We give more detail about the pruning algorithms in the case study in Section 3.