Analyzing and verifying Petri net model of security protocol based on Maria

作者：Wang Yan^*; Zhou Jiantao; Li Hua; Hao Ying

来源：2010 International Conference on Computer Application and System Modeling, ICCASM 2010, 2010-10-22 to 2010-10-24.

DOI：10.1109/ICCASM.2010.5620733

• Analysis and verification
• Authentication services
• Automated analysis
• Formal specification and analysis
• Hot spot
• Improved models
• Kerberos protocol
• Maria
• Paper models
• Petri net models
• Public keys
• Security flaws
• Security protocols

Formal specification and analysis of security protocol is a research hotspot in network security at present. This paper models authentication service exchange of Public-Key Kerberos Protocol and an attack against this protocol with Petri nets. The Maria Tool automates analysis and verification of the model and finds that PKINIT -26 protocol has a security flaw. So we improve the model according to PKINIT -27 specification and verify authenticity of the improved model. It argues that Maria has the ability to analyze and verify sophisticated security protocols. Furthermore, it can be widely applied for automated analysis and verification of security protocol.

• 出版日期2010
• 单位内蒙古大学