IBS协议的形式化分析与验证

IBS agreement formal analysis and verification

安全协议的形式化分析方法有许多,但都普遍存在一些问题,本文介绍了一种在C P N模型基础上改进的形式化方法FOCPN,并且利用该方法对IBS协议进行了实验仿真分析,主要针对其不可否认性和可追究性进行了验证,实验结果显示该方法可以有效验证出I B S协议的特性。

There are many formal methods used in analysis of secure protocol with some problems. This paper introduces a modified formal method called FOCPN based on CPN, and uses this method in the analysis of IBS protocol. It emphasizes on IBS protocol＇s norepudiation and fairness to verify and analyze. The experimental result shows that this method can verify secure protocol＇s features.