The Application Of Instantiation Space Logic In Formal Analysis Of Public Key Authentication Protocols

The prevalence of network has brought in huge convenience to social life, but its vulnerability will lead to disaster. How to ensure the security of network has been a heat issue. Security protocols are efficient means to protect the network, and the security of security protocols has been the focus.The formal analysis approaches of security protocols have been rapidly developed in the past 30 years. Prof. Kaile Su has presented a new model of security protocol logic called Instantiation Space which applies knowledge reasoning in analysis of security protocols, and the corresponding automatic tool SPV has been designed and implemented. But as the freshness and immaturity of this logic, it calls for a mount of instances to check the correctness and efficiency of it.This paper applied precise, correct deduction and proof on 2 typical protocols SPLICE/AS and Denning-Sacco using the Instantiation Space logic system and revealed the efficiency of this logic in detecting impersonation attack but deficiency of multiple sessions attack in public key authentication protocols.On the ground of deduction , the paper chose a more serials of public key authentication protocols to use the tool SPV for automatic verification, and got expected results. It draws the conclusion that Instantiation Space logic and it's automatic tool SPV is correct and efficient in public key authentication protocols.