Athena: a novel approach to efficient automatic security protocol analysis

摘要: We propose a new efficient automatic verification technique, Athena, for security protocol analysis. It uses representation - our extension to the Strand Space Model, and utilizes techniques from both model checking theorem proving approaches. Athena is fully able prove correctness of many protocols with arbitrary number concurrent runs. The run time typical literature, like Needham-Schroeder protocol, often fraction second. Athena exploits several different that enable it analyze infinite sets runs achieve such efficiency. Our extended Model natural problem domain. properties are specified in simple logic which permits proof search algorithms has enough expressive power specify interesting properties. procedure borrows some proving. believe right combination compact all actually makes successful fast protocols.