Strand Space Model of Amended NS Protocol and Its Analysis

A strand is a sequence of events; it represents either an execution by a legitimate party in a security protocol or else a sequence of actions by a penetrator. A strand space is a collection of strands, equipped with a graph structure generated by causal interaction. In this framework, protocol correctness claims may be expressed in terms of the connections between strands of different kinds.It is the first time to prove the Miao-Hepsilas modified version of Needham-Schroeder protocol with the theory of strand space which is a rising formal analysis tool. Firstly, its authentication is analysed, the analysis contains responserpsilas authentication and sponsorpsilas authentication. Then its confidentiality is analysed, and two concepts honest and ideal are used to simplify the process of verification. It indicates that K, N_b, and N_b ⁰ are secret. At last, the result shows that the amended N-S protocol can reach the goal, and it is consistent with the result of Miao-Hepsilas analysis.