Evaluating and improving protocol analysis by automatic proof

The paper summarizes the results of Automatic Authentication Protocol Analyzer (AAPA) analyses of 52 protocols from A Survey of Authentication Protocol Literature: Version 1.0 by Clark and Jacob, a continually updated library of protocols analyzed in the protocol-failure literature. The AAPA found no problems in 27 that Clark and Jacob did not identify as having problems, but also found no problems in 16 that Clark and Jacob did identify as having problems, though the attacks on 8 of these would be prevented by type checks that the AAPA assumes are always made. It found problems in 6 that Clark and Jacob also identified as having problems, and found problems in 3 that Clark anal Jacob did not identify as having problems. The paper defines a semantics for the AAPA´s specification language, defines valid inference and protocol failure with respect to this semantics, identifies reasons for each of the AAPA´s “misses”, and sketches ongoing work that should correct all, or all except one, of these “misses”