Study On Analysis Of Security Protocols Of Computer Communication Network

This dissertation mainly discusses using formal methods for analysis of cryptographic protocols, the main results that the author obtained are as follows: (1) The limitations of the BAN logic are studied which are in assumptions, protocol idealisation, semantics, and attacks. (2) The model checker SMV are firstly used for analysis of cryptographic protocols and the method using SMV is proposed and has proved to be a very successful approach to analyzing cryptographic protocols. (3) The Helsinki cryptographic protocol is analyzed and a new modified Helsinki protocol is proposed which is secure and improved. (4) TMN cryptographic protocol is analyzed successfully and a new type of attack is proposed. (5) A general method (running modes), which can be used to verify the two-party cryptographic protocols, is proposed. Based on this method, the verification of the protocols becomes independent of model checking tools. (6) TW cryptographic protocol is analyzed by running modes and the result of analysis shows that using running modes to analyzing the two-party cryptographic protocols is a very successful approach. (7) The general SMV software which can be used to analyzing the two-party cryptographic protocols is designed.