非否认协议公平性分析的扩展串空间方法  

An Extended Strand Space Method for Fairness Analysis of Non-Repudiation Protocols

作　　者：李磊[1] 陈静[2] 王育民[1] 

机构地区：[1]西安电子科技大学综合业务网国家重点实验室,西安710071 [2]西安交通大学电子与信息工程学院,西安710049

出　　处：《西安交通大学学报》2010年第6期16-20,共5页Journal of Xi'an Jiaotong University

基　　金：国家自然科学基金资助项目(60473027);国家自然科学基金委员会-广东联合基金重点资助项目(U0835004)

摘　　要：针对在非否认协议公平性的形式化分析中,如何弱化初始假定和避免状态空间爆炸等问题,提出了扩展串空间方法.通过将签名运算引入串空间理论,从而对串空间理论的项集合进行重新定义,进一步通过对子项关系、攻击者迹和自由加密假定的扩展,并结合丛概念,构成了扩展串空间.分析非否认协议的公平性,首先将协议行为归纳为攻击者串、发送者串、接收者串和可信第3方串,以此构造协议的扩展串空间模型,然后结合协议迹和定理证明验证丛中存在发送者串等价于丛中存在接收者串,从而证明非否认协议公平性.通过扩展串空间方法对Zhou-Gollmann协议公平性的分析,得到了与Kailar逻辑和Lanotte自动验证方法相同的结果.与Kailar逻辑相比,扩展串空间方法仅使用自由加密假定,弱化了初始假定;与Lanotte自动验证方法相比,扩展串空间方法无需使用状态空间搜索,避免了状态空间爆炸问题.A new formal analysis method using extended strand space is presented to weaken initial assumptions and to avoid state space explosion in analyzing the fairness of non-repudiation protocols.Signature operations are introduced into the strand space theory,so that the set of terms and sub-term relations are redefined in the strand space theory.Then,an extended strand space model is constructed by inducing the action of protocols to the penetrating strand,the origin strand,the receiver strand,and the trusted third party strand.The fairness of non-repudiation protocols is analyzed by verifying that the existence of the origin strand in the bundle is equivalent to the existence of the receiver strand in the bundle depending on the measure of theorem proving.Analyzing results on Zhou-Gollmann protocol show that the proposed method can weaken initial assumptions compared with the logic method,and can avoid state space explosion compared with the state space method.

关 键 词：非否认协议 扩展串空间 协议验证 公平性 

分 类 号：TN918[电子电信—通信与信息系统]