Formal Analysis Of Provable Network Security Protocol Basesd On Logic Of Events

Formal method is an important approach for analysis of network security protocol,and it is also a hot research topic in the field of information security.Based on strict mathematical concepts and logic method,formal methods describe protocols,and find ambiguous or incomplete aspects in the description of the agreement.Moreover,it can effectively reduce the complexity of the analysis process,and make protocol security analysis simple,specification,practical.Theorem proving is a certain formal method,with the purpose of proving security of an infinitely concurrent network security protocol.The logic of events,a kind of logical method of theorem proving,describes the logic of protocols and algorithms under the concurrent and distributed systems.Based on logic of events,we extended it and put forward strong authentication theory,which aimed at formal description and certification on Needham-Schroeder(NS)protocol and Neuman-Stubblebine protocol.Contents of present paper:1.Based on logic of events,we conducted formal descriptions on seven action of security protocol,generating challenge numbers to security agreement,sending messages,receiving messages,encryption,decryption,signature and verification.The formal descriptions on secret keys,challenges and the protocol messages were given.With strong matching and matching session defined,as well as taking account the axioms of inference rules and logic of events,the strong authentication was concluded.2.NS protocol with two agents was studied.According to protocol vulnerabilities,we added timestamp to avoid replay attack.The logic of events was applied to formally describe the improved protocol.By certificating senders and receivers,strong authentication theory was proved to be applicable to both sides of the network security protocol.Meanwhile,Neuman-Stubblebine protocol with three agents was studied.The logic of events was applied to do legal definition on basal sequence of the protocol,and we found that the sender was safe while the receiver was not.And two-way authentication cannot be achieved.Strong authentication theory is suitable for three-sides network security protocol.3.Finally,we found that the authentication certification of Authentication-Protocol can be conducted merely by action reasoning of its honest body.And it is concluded logic of events is suitable for the safety certification of multi-agent protocol.