Analysis of Security Protocol Based on Petri Nets

摘要：

Petri Nets (PNs) have shown to be a formal method to design and model the security protocol. We first apply PNs to model the security protocol. To analyze the security protocol conveniently and efficiently, we present a method to translate PNs into Promela code and discuss in detail the transform rule. We use the LTL to formalize the correct properties of the protocol, and whole PNs of the security protocol is checked by SPIN. Additionally, we employ the Woo-Lam protocol to illustrate the feasibility of our method.

关键词： Security protocol PNs LTL Promela/SPIN Model checking

作者: Fengli Liu Wei Han Mingyue Jiang

作者单位: Center of Math Computing and Software Engineering, Zhejiang Sci-Tech University, Hangzhou, Zhejiang, P. R. China

会议类型: 国际会议

会议名称: 2010 International Conference on Circuit and Signal Processing(2010年电路与信号处理国际会议 ICCSP 2010)

会议地点: 上海

会议语种:英文

页码: 451-454

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