Open AccessA Novel Approach to Automatic Security Protocol Analysis Based on Authentication Event Logic
Author(s) -
Xiao Meihua,
Ma Chenglin,
Deng Chunyan,
Zhu Ke
Publication year - 2015
Publication title -
chinese journal of electronics
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.267
H-Index - 25
eISSN - 2075-5597
pISSN - 1022-4653
DOI - 10.1049/cje.2015.01.031
Subject(s) - computer science , authentication protocol , cryptographic protocol , protocol (science) , wide mouth frog protocol , decidability , principal (computer security) , authentication (law) , event (particle physics) , computer security , theoretical computer science , otway–rees protocol , cryptography , challenge handshake authentication protocol , medicine , physics , alternative medicine , pathology , quantum mechanics
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.