Formal Analysis Model of Security Protocol Based on PCL

摘要：

Formal analysis and verification for security protocol is a difficult and essential problem in network security. In this paper, one important formal analysis tool —protocol composition logic (PCL) is introduced. Its precursor PDS ?, structure and central idea are analyzed. After sketching the environment of security protocol, we develop a framework for formal analysis and verification of security protocols based on PCL, and describe the executing processes in detail. As a case study, the security properties of the amended Helsinki protocol are proved using PCL on the basis of general analysis model.

关键词： formal analysis security protocol PCL helsinki protocol

作者: Laifeng Lu Jianfeng Ma

作者单位: College of Mathematics and Information Science, Shaanxi Normal University, Xian, China Ministry of College of Mathematics and Information Science, Shaanxi Normal University, Xian, China

会议类型: 国际会议

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

会议地点: 太原

会议语种:英文

页码: 658-660

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