Netinfo Security ›› 2015, Vol. 15 ›› Issue (7): 71-76.doi: 10.3969/j.issn.1671-1122.2015.07.011

• Orginal Article • Previous Articles     Next Articles

Research on Authentication Protocol Security Based on Formal Verification Tool

DUAN Ran, XU Nai-yang, HU Ai-qun()   

  1. School of Information and Engineering, Southeast University, Nanjing Jiangsu 210096, China
  • Received:2015-05-20 Online:2015-07-01 Published:2015-07-28

Abstract:

With the rapid development of the Internet services, the computer network has been the main approach to interchange of information. The Internet brings convenience to people, while also brings about privacy leakage and further more monetary loss. People devotes to themselves to protect information security in which authentication protocol is in major. Formal analysis assists protocol-design and covers the bug of protocol security. Formal analysis includes model checking, theorem proving and belief logic. AVISPA includes model checking and some else formal analysis, and also can be automatic. SPAN makes the function of AVISPA vivid and localization which is described as Message Sequence Charts. Choose SPAN to analyze SSL protocol and Kerberos protocol. It turns out that SSL protocol tends to suffer from falsify certification and the public key system isn’t secure on Kerberos protocol. To improve SSL protocol, make users not believe in SSL certification and provide the intruder from fetching public-key for encrypting certification; to improve Kerberos protocol, public-key replacing symmetric-key keeps other keys safe even if the intruder crack one key.

Key words: authentication protocol, security, SPAN, SSL protocol, Kerberos protocol

CLC Number: