Sciweavers

Share
CSFW
1999
IEEE

Athena: A New Efficient Automatic Checker for Security Protocol Analysis

11 years 4 months ago
Athena: A New Efficient Automatic Checker for Security Protocol Analysis
We 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. We 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 we allow any arbitrary configurations of the protocol execution, (for example, any number of initiatorsand responders), terminationcould be forced by bounding the number of concurrent protocol runs and the length of messages, as is done in most existing model checkers. Athena also exploits several state space reduction techniques. It is based on an extension of the recently proposed Strand Space Model [25] which captures exact causal relation i...
Dawn Xiaodong Song
Added 02 Aug 2010
Updated 02 Aug 2010
Type Conference
Year 1999
Where CSFW
Authors Dawn Xiaodong Song
Comments (0)
books