摘要
为了将密码协议的非否认性和公平性统一在一个框架之下更好地进行分析,提出了一套适用于分析非否认性和公平性的一阶逻辑语法和语义。在此基础上建立了一个用于分析非否认性和公平性的一阶逻辑模型,并以FairZG非否认协议为例进行了分析,发现了该协议的一个已知攻击,证明了模型的有效性和正确性。
In order to analyze the non-repudiation and fairness properties under one frame, a set of first-order logic syntax and semantics for non-repudiation protocols was proposed, and a model was built. The Zhou-Gollmann fair non-repudiation protocol was analyzed with the model and a known attack to the protocol was found. The results show that our model is valid and correct.
出处
《计算机应用》
CSCD
北大核心
2007年第9期2189-2193,共5页
journal of Computer Applications
关键词
非否认性
公平性
一阶逻辑
形式化分析
non-repudiation
fairness
first-order logic
formal analysis
