Date Added: Jan 2011
The authors propose an efficient automatic checking algorithm, Athena, for analyzing security protocols. Athena incorporates a logic that can express security properties including authentication, secrecy and properties related to electronic commerce. They have developed an automatic procedure for evaluating 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 they 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 model checkers.