Los Angeles, CA
March 31, 2009 to April 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, 2009 WRI World Congress on Computer Science and Information Engineering, CSIE, 2009 WRI World Congress on Computer Science and Information Engineering, CSIE 2009, pp. 439-442, doi:10.1109/CSIE.2009.467