Analyzing and Verifying Petri Net Model of Security Protocol Based on Maria

摘要：

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 PKJMT-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.

关键词： petrl net security protocol Maria analysis and verification

作者: Yan Wang Jiantao Zhou Hua Li Ying Hao

作者单位: Inner Mongolia University College of Computer Science, Huhhot 010021, Inner Mongolia, China Inner Mo Inner Mongolia University College of Computer Science, Huhhot 010021, Inner Mongolia, China

会议类型: 国际会议

会议名称: The 2010 International Conference on Computer Application and System Modeling(2010计算机应用与系统建模国际会议 ICCASM 2010)

会议地点: 太原

会议语种:英文

页码: 400-405

在线出版日期: 2010-10-22（万方平台首次上网日期，不代表论文的发表时间）