欢迎来到天天文库
浏览记录
ID:34095513
大小:1021.52 KB
页数:4页
时间:2019-03-03
《基于 spi 演算的安全协议验证》由会员上传分享,免费在线阅读,更多相关内容在教育资源-天天文库。
1、第28卷第3期计算机应用与软件Vol28No.32011年3月ComputerApplicationsandSoftwareMar.2011基于Spi演算的安全协议验证郑清雄(上海交通大学计算机科学与工程系上海200240)摘要在安全协议的各种验证方法中,进程代数方法依托完善的进程演算理论得到了很好的应用。Spi演算在PI演算的基础上扩充了密码操作原语来刻画安全协议,并使用测试等价验证安全属性。讨论了利用Spi演算进行验证的过程,并对经典NSSK协议进行分析。关键词安全协议 Spi演算测试等价 NSSK协议VERIFYINGSECURI
2、TYPROTOCOLSBASEDONSPICALCULUSZhengQingxiong(DepartmentofComputerScienceandEngineering,ShanghaiJiaotongUniversity,Shanghai200240,China)Abstract Amongseveralauthenticationmethodsforsecurityprotocols,processalgebraapproachwhichreliesonasoundtheoryofconcurrentprocesscalculu
3、shasbeenwellapplied.TheSpicalculusdepictssecurityprotocolsasanextensionofthepicalculusbyenrichingitscryptographicprimitives,andusestestingequivalencetoverifysecurityproperties.TheprocessofauthenticationwithSpicalculusisdiscussedinthepaper,theanalysisonclassicalNSSKprotoc
4、oliscarriedoutusingthisapproachaswell.Keywords Securityprotocols Spicalculus Testingequivalence NSSKprotocolL,M,N terms0 引言nname(M,N)pair安全协议是信息安全的基础,然而设计一个符合安全目标 0zero的协议十分困难。因此,必须借助形式化方法,对安全协议进行suc(M)successor分析和验证[1]。基于进程代数的安全协议验证能够精确地描xvariable述协议中不同主体之间的交互过程
5、,得到了广泛的应用。Abadi{M}nsharedkeyencryption和Gordon在pi演算[2,3]的基础上,增加密码学描述原语,建立在pi演算中,名是唯一的项。Spi演算增加了描述对(pair)和数字(zero,successor)的项结构是为了便于在安全协议中描了用来描述和验证安全协议的Spi演算。Spi演算保持了pi演述它们。而将变量从名中区分开来则是为了简化一些等式的描算简单的语法和强大的描述能力,采用互模拟等价理论对安全述。另外,Spi演算增加了基于共享密钥加密的项结构,项{M}N协议进行验证。表示在共享密钥系统(如
6、DES)中用密钥N对项M加密所得到本文以Spi演算为工具对安全协议验证的过程进行描述,的密文。并且在Spi演算框架内验证对经典NSSK协议的一种攻击方法。1.2 Spi演算的进程进一步,定义Spi演算中的进程(process)集合:1 Spi演算的语法P,Q,Rprocessesm〈N〉.P output[4,5]pi演算是RobinMilner在CSS等进程演算的基础上提M(x).P input出的,已经成为并发计算的基础模型。pi演算能够表示通信拓P|Q composition[6]扑结构可以动态变化的系统(既移动进程)。Spi演算是
7、对pi(vn)P restriction演算的增强和扩充,增加了支持密码系统的原语。利用Spi演!P replication算,我们能够对协议进行详细的抽象和分析。[MisN]P match1.1 Spi演算的项 0 nillet(x,y)=MinP pairsplitting假设有名(name)所组成的无限集合,这是安全协议中用来通讯的通道集合;以及有变量(variable)所组成的无限变量收稿日期:2009-12-28。郑清雄,硕士生,主研领域:远程演算,安集合。定义Spi演算的项(term)集合如下:全协议。第3期郑清雄:基于Spi
8、演算的安全协议验证263caseMof0:Psuc(x):QintegercasecaseLof{x}NinPsharedkeydecryption3 Spi演算的语义进程的基本语义可以做如
此文档下载收益归作者所有