The Application Of Knowledge Theory Based Secure Protocol Formal Verification Method

Security protocol verification is an important technology of guarding network's security. In this paper, we've discussed a series of typical symmetric Key exchange protocols, and formally verify it using a new knowledge based security protocol verification method which is called SPV logic in this paper. Consequently, we've inspected the correctness of this logic as dealing with the encrypted information of shared key and dynamic key.In this paper, we've presented a detailed formal verification procedure of symmetric key exchanging protocol-Kao Chow and Yahalom, and deliberately analyzed and proved their secure properties such as authentication, and so on. In the process of verifying Kao Chow protocol, we've found the redundance of transmitted information, and then simply the protocol under the precondition of not exerting influence on secure properties. In the process of verifying Yahalom protocol, we've found a failure of (n,l)-secrecy theorem, which is the most important one in relevant axiomatization system, and then revised it through tutor's guides.In order to test the correctness of the verification tool SPV, we've applied it to verify a plenty of symmetric key exchanging protocols. However, we've found SPV's failure owing to the different consequences between auto-verification and manual deduction of Kao Chow protocol.