多方不可否认协议的增广CSP建模与分析

基于逆向工程的思想，使用前期工作中提出的面向两方不可否认协议分析的增广CSP方法，对典型的Kremer-Markowitch多方不可否认协议的安全性进行了探索性建模与分析。借助该分析成功发现此协议在满足不可否认性和公平性的同时却不具备时限性。这表明在适用于两方不可否认协议安全性验证的同时，增广CSP方法也可作为多方不可否认协议安全性验证的新方法。

Modeling and analysis of multi-party non-repudiation protocols with extended-CSP approach

Follow with the methodology of reverse engineering,an exploratory modeling and analysis of security of the typical Kremer-Markowitch multi-party non-repudiation protocol were carried out with a novel method named extended-CSP approach which had been proposed for two-party non-repudiation protocol in preliminary work.With the analysis,the inherent fact that this protocol statisfies not timeliness but non-repudiality and fairness was found successfully.The result of the analysis indicates that,as applying to two-party non-repudiation protocols,the extended-CSP approach can also be a new method for security verification of multi-repudiation protocols.