| Athena is a new formal verification approach for security protocol analysis. This dissertation makes an analysis of Athena approach and extends it to be enabled to analyze type-flaw attacks and multi-protocols guessing attacks which are two significant problems in the area of security protocol verification. The main results that the author obtained are as follows:(1) This paper introduces Athena's extensions based on strand spaces, analyzes its logic and verification algorithm comprehensively. And the experiment data shows its high efficiency.(2) Athena approach adopts the strong typing abstraction, where all message considered in analysis are assumed to be well-typed. This corresponds to an assumption that all agents can magically tell the true types of message. However, it is not realistic when protocol runs in real environment. So we extend Athena. In this paper, a composite term is added, and an intruder's ability of type-transition is enhanced. We extend the notion of inter-term, goal and goal binding in Athena, and adapt some related notion. Using the extended approach, NSL protocol is analyzed and we found a type-flaw attack, which can not be found in APV tool.(3) Multi-protocols is one of the open issues in security protocol analysis, and multi-protocols guessing attack is a specific problem, which belongs to it. Based on this problem, Athena approach is extended. Considering the secondary protocol's effects on primary ones, we introduce the notion of ideal in strand spaces, and based on which a PPI (protocol-to-protocol influence) relation is presented. Then, in order to relate verifiers in the search process of the next-state function of Athena, two new notions of guessing verifier goal and guessing verifier goal binding are presented. Accordingly, the state expressive way and inference rules are adapted. Finally, using the extended of Athena approach, we find a guessing attack when EKE protocol and another constructed authentication protocol run at the same environment. |
PDF Full Text Request