spi演算证明协议非可否认性

《spi演算证明协议非可否认性》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、第5期李援等：spi演算证明协议非可否认性·97·spi演算证明协议非可否认性李援1，蒋建国1，王焕宝2（1.合肥工业大学计算机与信息学院，安徽合肥230009；2.安徽建筑工业学院数理系，安徽合肥230022）摘要：spi演算以进程代数理论作为基础，适合多轮并发条件下安全协议的证明。通过在spi系统中引入消息起源测试成功表示了签名消息的安全语义，并在此基础上验证了ZG协议的非可否认性，扩展了spi演算在安全协议证明中的应用范围。关键词：spi演算；非可否认；公平性；消息起源测试中图分类号：TP

2、309文献标识码：B文章编号：1000-436X(2009)05-0094-05Formalanalysisofnon-repudiationprotocolbyspiLIYuan1,JIANGJian-guo1,WANGHuan-bao2(1.CollegeofComputerandInformation,HefeiUniversityofTechnology,Hefei230009,China;2.DepartmentofMathematicsandPhysics,AnhuiInstitut

3、eofArchitectureIndustry,Hefei,230022,China)Abstract:spicalculus,whichwasbasedonthetheoremsofprocessalgebra,wasfitfortheproofofconcurrentprotocolexecution.Messageoriginationtestwasputupandthesemanticsofmessagesignoperationwassuccessfullyexpressedbaseo

4、nthetest,atlast,thenon-repudiationprotocolZGwasprovedsoastoprovethevalidityofthemethod.Keywords:spicalculus;non-repudiation;fairness;messageoriginationtest第5期李援等：spi演算证明协议非可否认性·97·1引言1.1spi演算收稿日期：2007-06-26；修回日期：2009-03-08基金项目：国家自然科学基金资助项目（60474035）；

5、国家教育部博士点基金资助项目（20060359004）FoundationItems:TheNationalNaturalScienceFoundationofChina(60474035);ThePh.D.ProgramsFoundationofMinistryofEducationofChina(20060359004)Abadi等在1997年提出以进程代数理论为基础的spi演算[1,2]，利用进程间的互模拟等价关系证明安全协议的秘密性，其理论清晰，特别适合于多轮并发协议的安全性验证。虽然A

6、badi此后进一步增强spi演算，提出应用pi演算并利用其成功证明了JKF等协议的公平性、匿名性以及抗DOS攻击性[3,4]，但由于Abadi等在使用spi进行协议建模时忽略了密码签名操作的安全语义，从而限制了spi在安全协议证明中的应用范围。另一方面，为了完成对认证性、秘密性外安全属性的证明，人们不得不借助于原有的逻辑证明系统或其他的定理证明方法。因此，扩展代数证明方法在安全协议分析中的应用范围，在演算系统中添加安全操作的语义表达是亟待解决的问题。1.2非可否认协议第5期李援等：spi演算证明

7、协议非可否认性·97·非可否认协议允许参与协议主体发送和接收信息，并在协议的运行过程中提供相应的证据给参与协议双方，使任一方在之后都不能够对自己曾经发送或接收信息的行为进行否认的一类协议。非可否认性的实现与主体间交换的证据消息密切相关，一般而言，证据是带有签名的消息，这样就保证了消息来源的正确性。与认证协议和密钥交换协议不同，非可否认协议通常不考虑主体间通信时存在攻击者的情况，而是协议两方并不相互信任，因此希望能够相互保护，以确保各自利益的情况下使用。因此，非可否认协议必须保证作为证据的消息正确

8、性，同时保证此消息足够强壮，使得拥有它的主体能够实现其安全目标。非可否认协议的典型应用情况是：两方主体在一个被动通信环境中进行交互，此环境并不被任何一方主体或者其他主体操纵，但是这两方主体却都可能为牟取自身利益而进行一些非法行为。2非对称密钥系统的spi演算项和进程是pi演算[5]的基本概念，其中项用L、M、N表示，而用P、Q、R…表示进程。非对称密码系统包括公钥和私钥，其中公钥公开而私钥保密，任何主体都可以使用公钥进行数据加密，但只有持有对应私钥的主体才能解密此消息；同时，主体的私钥也可以用于