Los Angeles, California USA
Mar. 31, 2009 to Apr. 2, 2009
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/CSIE.2009.467
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-He’s 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 responser’s authentication and sponsor’s authentication. Then its confidentiality is analysed, and two concepts honest and ideal are used to simplify the process of verification. It indicates that K, Nb, and Nb0 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-He’s analysis.
security protocol analysis, Strand space, the Needham-Schroeder protocol with shared keys
Shimin Wei, Yuyan Guo, "Strand Space Model of Amended NS Protocol and Its Analysis", CSIE, 2009, Computer Science and Information Engineering, World Congress on, Computer Science and Information Engineering, World Congress on 2009, pp. 439-442, doi:10.1109/CSIE.2009.467