The automatic protocol screener needs to be sound and efficient. Given a candidate protocol, the protocol screener has to be able to examine the protocol and tell whether it is correct or not. The protocol screener is sound if when it claims that a protocol satisfies certain security properties, it is true that the protocol really does satisfy these properties. Since the protocol generator generates thousands of candidate protocols, the protocol screener needs to be highly efficient to find the optimal protocol in a reasonable amount of time.
There are several existing tools for semi-automatic and automatic protocol analysis, such as the NRL Analyzer [Mea94], the Interrogator Model [Mil95], FDR [Low96], Mur [MMS97], and Brutus [CJM98]. Athena is a recently introduced checker for security protocol analysis [Son99]. Comparing to other existing automatic tools, Athena has the following two main advantages:
For these reasons, we choose to use Athena as the protocol screener. During this project, Athena has verified tens of thousands of protocols and has established itself as a highly efficient and robust tool for automatic protocol analysis.
The following is a brief overview of how Athena works. Athena uses an extension of the recently proposed Strand Space Model [THG98] to represent protocol execution. Athena incorporates a new logic that can express security properties including authentication, secrecy and properties related to electronic commerce. An automatic procedure enables Athena to evaluate well-formed formulae in this logic. For a well-formed formula, if the evaluation procedure terminates, it will generate a counterexample if the formula is false, or provide a proof if the formula is true. Even when the procedure does not terminate when we allow any arbitrary configurations of the protocol execution, (for example, any number of initiators and responders), termination could be forced by bounding the number of concurrent protocol runs and the length of messages, as is done in most existing automatic tools.
Athena also exploits several state space reduction techniques. Powered with techniques such as backward search and symbolic representation, Athena naturally avoids the state space explosion problem commonly caused by asynchronous composition and symmetry redundancy. Athena also has the advantage that it can easily incorporate results from theorem proving through unreachability theorems. By using the unreachability theorems, it can prune the state space at an early stage, hence, further reduce the state space explored and increase the likely-hood of termination. These techniques dramatically reduce the state space that needs to be explored.