A Novel Approach to Automatic Security Protocol Analysis Based on Authentication Event Logic

Since security protocols form the cornerstones of modern secure networked systems, it is important to develop informative, accurate, and deployable approach for finding errors and proving that protocols meet their security requirements. We propose a novel approach to check security properties of cryptographic protocols using authentication event logic. Compared with logic of algorithm knowledge, authentication event logic guarantees that any well-typed protocol is robustly safe under attack while reasoning only about the actions of honest principals in the protocol. It puts no bound on the size of the principal and requires no state space enumeration and it is decidable. The types for protocol data provide some intuitive explanation of how the protocol works. Our approach has led us to the independent rediscovery of flaws in existing protocols and to the design of improved protocols.