网络安全认证协议形式化分析PPT演示文稿

内江师范学院学报J OUR NAL OF N EIJ IAN G NORMAL UN IV ERSI TY第23卷第12期No.12Vol.23一种自动验证网络安全协议的互模拟方法杨　军,孟海涛3(盐城工学院江苏　盐城224051) 摘　要:为了解决进程接收具体信息的输入所带来的无穷种迁移问题,采用一种称为“符号化”的方法,提出了进程符号环境和符号化和格局标号迁移语义,为Spi 演算设计了符号互模拟关系—符号Reded 互模拟.结果表明:该符号互模拟关系对传统的互模拟关系是可靠的,符号化的标号转移语义将进程无穷输入导致的迁移限期为有穷种迁移.因此使得基于该关系的安全协议自动验证算法得以实现.关键词:密文通信协议;进程演算;符号互模拟中图分类号:TP393.08文献标识码:A文章编号:167121785(2008)12-0056-030　引言近十年来,进程演算,如Spi 演算[1]、CSP 和CCS 等,由于能很好地为网络安全协议建立模型、验证其安全属性,因而基于进程演算的安全协议形式化分析方法得到很大的发展.在这些模型中,Abadi 和G or 2don 的Spi 演算尤为引人注目.Spi 演算是在Pi 演算[5]中增加了加解密原语和一些关系扩展而来.协议的安全属性通常用偏序关系∠∠来表示[4].例如,为了说明协议P 具有保密性,可以构造一个与P 并发的攻击者O ,在环境ε里并发执行P 和O.如果所有的运行迹均未泄漏密文消息M ,则说明P 具备保密性,否则不具备.其缺点在于进程O 并不能描述所有的攻击者.1Spi 演算语言Spi 演算为由Pi 演算发展而来的进程代数语言.在增加了对称加解密、哈希原语之后,它能够用来表示复杂消息的传递,从而可以来为安全协议建立模型.在增加了配对(pairi ng )、配对分裂(pair 2split ti ng )、匹配(match )和非匹配(mismatch )等原语后,更进一步地描述安全协议性质.对安全协议的分析基于同样的完美加密假设[2],也即加密和哈希算法是足够强壮的,加密的密钥是原子的.本文所使用的Spi 演算的语法如下:n ∷=a ,c ,….,k ,n …名N ν∷=x ,y ,z …变元VM ∷=n │(M 1;M 2)│E (M;n )│H (M )　消息Mt ∷=x │M │(t 1,t 2)│E (t 1,t 2)│H (t)│πi (t 1,t 2)│D (t 1,t 2)项Tb ∷=tt │b 1　∧b 2│┐b │[t 1=t 2]│[t :N ]│[eν├t]布尔表达式BP ∷=0│c(x).P │c 〈t 〉.p │P │Q │b ∶P ,Q │(νa)P │let x =D (t ,t ′0)in P │case x of πi (t 1,t 2)in P进程项P为了表示非对称加密,假设有关系КΑN ×N ,满足(k ,k ′)ΑК当且仅当用k 加密的消息能被k ′解密;定义I (k )={k ′│(k ,k ′)ΑK};一个替换σ是一个满足条件σ(.)∶V →T 的偏序函数.替换可以作用于进程、项和表达式等.2　符号操作语义与具体语义规则不同的是,当执行符号语义中的进程输入动作时,用给输入变元赋值的消息是用含变元的项来替代的,而这种替代直到环境允许时才进行.此外,语义规则中布尔表达式满足的条件在进程迁移过程中被累积和满足[3].符号操作语义的迁移规则形式是P |→λbP ′,这里,λ∈A s ={c(x),c 〈t 〉},b ∈B ,则记为P |→λttP ′.当b =�,相应的对称规则省略.当布尔表达式条件为真时,符号操作语义传递规则跟具体语义是等价的.S pi 演算的符号操作语义如下:65　收稿日期　作者简介杨军(6),男,江苏盐城人,盐城工学院学生处硕士:2008-09-01:199-.2008年12月杨　军,孟海涛:一种自动验证网络安全协议的互模拟方法(S IN )--c (x )P |→c (y )ttP [y/x ]y =new {T},(S OU T )--c 〈t 〉P |→c 〈t 〉ttP,(S CH S I )P |→λbP ′b ′∶P ,Q |→λb ∧bP ′,(S PARI )P |→λbP ′P |Q |→λbP ′|Q,(S RES )P |→λbP ′(νa )P |→λb(νa )P ′a |{c}∪n (b),(S S PL 1)P[t 1/x 1]|→λbP ′ca se x of π1(t 1,t 2)in P |→λbP ′(S D EC )P[t/x ]|→λbP ′let x =D (E (t ,t ′),t ″)in P |→λb ∧b ′∧b ″P ′b ′ =(I (t ″)=t ′),b ″={t ′,t ″}∶N .引理2.1　PμP ′当且仅当存在赋值ρ和替换σ,且满足P |→λb P ′,这里,P ′=Q σ,μ=λ.σ,ρ(b.σ)=tt.3　格局的LTS 语义在Spi 演算中,密文协议被认为运行在能够攫取、伪造各种消息的环境中.进程P 的具体环境ce ν是由进程P 具体消息的输出和复合规则得到的消息集合,而符号环境eν是进程P 项输出和复合规则的集合.本节主要分析进程的符号环境(为方便起见,后文用“环境”指称“符号环境”).当一个进程输出一个消息时,它的环境将复制一份放入其消息集中.另一方面,当进程需要输入一个消息时,它的环境将试图伪造各种可能的消息给输入进程,这就导致了如引言中所述的难以处理的输入动作迁移后出现的无穷种可能分支问题.从环境e ν产生项t 的过程必须仔细地设计,首先看如下一个例子.P ≡c 〈E (M ,k )〉|c (x ).l et =Dec (x ,I (k ))inc 〈u 〉,eν=Φ.在上述进程的执行中,P 需要从环境中接收一个项=(y ,)由于密钥对环境依然是未知的,项=(y ,)的产生只能受限于替换σ(=[M y ]),且当环境知道消息(M ,)也即,假设(M ,)∈e ν;k |ev ,替换σ(=[M/y ])使得推理e ν|-t 成立,这里t =E (y ,k ).格局C =(eν,P )是进程P 和其符号环境ev 的二元组.格局的迁移对应于进程和其环境之间的交互.现在,定义格局的标号迁移语义(L TS 语义)(F IN )P |→c (x )b P ′[t/x ](e ν,P)|→c (x )b ∧[e ν|-t](e νσ,p ′[t/x ]σσ∶e ν|-t ,(F OUT )P |→c (x)bP ′(e ν,P)|→c(x)b(e ν∪{t},p ′),4　Reefe d 互模拟在Spi 演算中,互模拟等价是两个进程之间十分重要的关系.为了验证进程P 和Q 之间是否互模拟,通常需要在等价环境对中检验P 和Q 是否执行一致的动作.本文中所使用的互模拟关系(取名为Reef ed 互模拟),包含具体和符号互模拟.具体Reef ed 互模拟的定义类似于其他已存在的互模拟[2].定义4.1　一个协调的关系R c 是具体Reefe d 模拟的,当(e ν1,e ν2)|-PR cQ 可推出,无论(ce ν1,P )c(x)(ce ν′1,P ′),存在一个格局(ce ν′2,Q ′)和(ce ν2,Q)c(y)(ce ν′2,Q ′),且对所有的消息M 和N ,(ce ν1,ce ν2)|-(M ∴N ),满足(ce ν′,ce ν′2)|-P ′[M/x ]R cQ ′[N/y ];(ce ν,P )c〈M 1〉(ce ν′1,P ′),这里ce ν′1=ce ν1∪{M 1},存在一个格局(ce ν′2,Q ),且满足(ce ν2,Q )c〈M 2〉(ce ν′2,Q ′)ce ν2=ce ν′2∪{M 2}和(ce ν1,ce ν2)|-P′R C Q ′.一个具体的Reefed 互模拟是关系R c ,且满足R c和R cT都是具体Reefed 模拟的.具体的Reefed 互模拟类(Bi similarit y)(～c r )是所有具体Reefed 互模拟关系的集合.具体Reefed 互模拟即指具体Reef ed互模拟类,用符号～c r 来表示.定义4.2　一个协调的关系R b 是符号Reef ed模拟的,当(ν,ν)|R Q 可推导出,无论何时()　(ν,)|→(x )∧[ν|](ν′,′[x ]σ),这里75t E k .k t E k /ev E k .E k e 1e 2-P b i e 1P c b1e 1-t e P t/1内江师范学院学报第23卷第12期σ1∶eν1|-t且eν′1=eν1σ1,存在一个替换σ2和布尔集B,满足(1)σ2∶eν2|-t和eν′2=eν2σ2;(2)b∧b1]∪B,Πb′∈B,b′]b2满足(eν2,Q)|→c(x)b2∧[eν2|-t](eν′2,Q′[t/y]σ2)和(eν′1,eν′2|-P′[t/x]σ1R b Q′[t/y]σ2.(ii)　(eν1,P)|→c〈t1〉b1(eν′1,P′),这里eν′1=eν1∪t1,存在一个布尔集B,这里b∧b1]∪B,Πb′∈B,b′]b2,满足(eν2,Q)|→c〈t2〉b2(eν′2,Q′),这里eν′2=eν2∪t2,且(eν′1,eν′2)|-P′R b′Q′.定理4.1(可靠性)　如果ε|-P～b r Q,ε= (eν1,eν2),则存在一对合适的替换σ1,σ2和一个赋值函数ρ,满足εcσ1,σ2|-Pσ1～c r Qσ2.5　总结本文首先把Spi演算扩展为能描述所有加密系统的、具有清晰语义的计算模型.为解决进程接收具体信息的输入所带来的无穷种迁移问题,提出了进程符号环境和符号化的格局标号迁移语义.在此基础上,为S pi演算设计了解决此问题的符号互模拟关系———符号Reef ed互模拟,并证明了它是具体互模拟关系的可靠逼近.基于这项工作,显然可以实现基于Spi演算的协议安全属性自动化验证,我们相信这对于应用在软件和电路中的自动检测也有很大的启发作用.参考文献:[1]Abadi M and G or d o n A D.A bisimulation met h od fo rc rypto graphic protocols[J].No rdic Jo ur nal of Compu2ting,1998,5(4):2672303.[2]Boreale M,De Nicola R,and Pugliese R.Proof tech2nique s for cryptographic processes[J].SIAM Journal on Computing,2002,31(3):9472986.[3]Borgst r J om,Briais S a nd Nestmann U Symb olic bisimu2lations in the spi calcul us.Proc.of CONCU R2004,vol2 ume3170of LNCS,2004:1612170.[4]Boreale M Symbolic trace a nalysis of c ryptograp hic p ro2tocols[M].Proc of ICAL P200,2001:6672681.[5]ner,Pa rrow J,Walker D.A calc ulus of mobileproce sses,I a nd II[J].Infor mation a nd Computation, 1992,100(1):1277.A Bisimulation Method for Automatic Conf ir m a tionof N et w or k Secur ity Cr yptogra phic Pr otocolsY ANG jun,ME NG Hai2Tao(Y a ncheng Institute of Tecnology,Y anc heng,Jiangsu224051,China) Abstract:In order to find a solution to the infinite migra tio n p ro ble m caused by a process’s receipt of concrete infor mation input,by use of a sym b olic method,the idea of proce ss symbolic environment and symbolic migration se ma ntic s ar e put for th. The r elation of symbolic bisimulation(symbolic Reef ed bisimulation)is designed f or Spi calculus.The re sult shows:the symbol2 ic bisim ulation is reliable to the tr aditional concrete bisimulation.Since t he symbolic migration semantics i s a ble to confine the migr ation restric tio n,whic h arises f ro m the proce ss’s receipt of infinite input,to finite migration,it help s secure the realiza tio n of t he automatic securit y p ro tocol confirmation that is ba sed on such a relation. K ey w or ds:cr yptographic p rotocols;process calc ulus;symbolic bisimula tionn(责任编辑:胡　蓉　英文审译:阳卓胜) 85。

第28卷　第3期2005年3月计 算 机 学 报CH IN ESE J OU RNAL OF COM PU TERSVol.28No.3Mar.2005SPA :新的高效安全协议分析系统李建欣　李先贤　卓继亮　怀进鹏(北京航空航天大学计算机学院　北京　100083)收稿日期:2003201209;修改稿收到日期:2004212230.本课题得到国家自然科学基金(90412011)和国家“八六三”高技术研究发展计划项目基金(2003AA144150)资助.李建欣,男,1979年生,博士研究生,主要研究方向为网络安全、信任协商.E 2mail :lijx @ ;myjianxin @.李先贤,男,1969年生,博士,副教授,主要研究方向为信息安全、计算机科学理论.卓继亮,男,1976年生,硕士研究生,主要研究方向为网络安全.怀进鹏,男,1962年生,博士,教授,博士生导师,主要研究方向为计算机软件与理论、中间件与网格技术、网络安全.摘　要　研制高效的自动分析系统是密码协议安全性分析的一项关键任务,然而由于密码协议的分析非常复杂,存在大量未解决的问题,使得很多现有分析系统在可靠性和效率方面仍存在许多局限性.该文基于一种新提出的密码协议代数模型和安全性分析技术,设计并实现了一个高效的安全协议安全性自动分析系统(Security ProtocolAnalyzer ,SPA ).首先对协议安全目标进行规范,然后从初始状态出发,采用有效的搜索算法进行分析证明,试图发现针对协议的安全漏洞.使用该系统分析了10多个密码协议的安全性,发现了一个未见公开的密码协议攻击实例.实验数据显示,该系统与现有分析工具相比,具有较高的分析可靠性和效率,可作为网络系统安全性评测以及密码协议设计的有效辅助工具.关键词　信息安全;密码协议;形式化分析;搜索算法;攻击序列中图法分类号TP309SPA :A N e w E ff icient System for Security Protocol AnalysisL I Jian 2Xin L I Xian 2Xian ZHUO Ji 2Liang HUA I Jin 2Peng(S chool of Com puter Science ,Bei hang Universit y ,Bei j i ng 100083)Abstract Cryptograp hic protocols are communication p rotocols of dist ributed systems t hat use cryptograp hy to achieve various goals such as aut hentication and key dist ribution in t he open net 2work environment.Developing efficient automatic system is a crucial task in t he area of security analysis for cryptograp hic p rotocols.However ,t he security analysis for cryptograp hic protocols is very co mplex and difficult and a lot of unresolved p roblems still p resent in it ,which causes some limitations on reliability and efficiency of previously available automatic systems.An effi 2cient automatic analysis system (Security Protocol Analyzer ,SPA )for cryptograp hic p rotocols is designed and implemented based on t he CPA (Cryptograp hic Protocol Algebra )model and new a 2nalysis techniques.In t his system ,security p roperties of t he cryptograp hic protocols are specified firstly ,and t hen an effective p roof search algorit hm starting wit h t he initial state is applied and t ries to find all possible attack sequences on t hem.More t han ten cryptograp hic protocols are ana 2lyzed successf ully wit h t his system ,and moreover ,a new attack instance is also found.The anal 2ysis result s show t hat SPA has imp roved t he analysis reliability and efficiency compared wit h ot h 2er existing tools.It can be used as an efficient tool for t he evaluation of t he network security and t he design of cryptograp hic p rotocols.K eyw ords information security ;cryptograp hic protocol ;formal analysis ;search algorit hm ;at 2tack sequence1　引　言随着互联网技术及应用的飞速发展,如何保护网络传送信息的安全成为一项重要的任务.密码协议(也称为安全协议)是采用密码学技术来达到密钥分配、主体身份认证等目的的通信协议,在很大程度上为网络通信提供了安全性保证.这些密码协议都是经过精心设计的,角色间消息的交互存在着复杂的关系和制约,而且大部分的密码协议是运行在分布式网络环境中.分布式网络具有多主体参与、大规模并发和运行动态性等特点,正是由于这种运行环境的复杂性使得设计出的密码协议难免出现缺陷.大量的事例表明,许多密码协议在使用多年后才发现存在很严重的安全漏洞,例如著名的Needham2 Schroeder公开密钥协议在公开17年后,它存在的中间人攻击漏洞才被Lowe发现[1].由于密码协议的漏洞一般都很隐蔽,使用手工分析非常困难,易于出错,所以研制高效、可靠的自动分析工具成为密码协议安全性分析的一项关键任务.目前国际上推出了许多自动分析工具,然而它们大都仍然存在搜索状态数太多的问题,而且这些工具往往只面向研究人员,一般的技术人员难以使用.本文在文献[2]提出的密码协议形式模型———CPA (Cryptograp hic Protocol Algebra)模型的基础上,设计并实现了一个高效的安全协议分析系统SPA (Security Protocol Analyzer),能够有效分析多种类型的密码协议.2　相关工作采用形式化方法分析密码协议已有20多年的历史,一直属于国际上研究的热点[3].目前,对密码协议进行形式化分析广泛采用模型检测和定理证明的技术.针对密码协议进行形式化分析的特定模型检测工具包括Interrogator[4]、Brut us[5]等.其中Interro2 gator是比较早的基于状态空间搜索思想来发现协议安全缺陷的模型检测工具,它使用通信状态机描述协议的参与者,并赋予了攻击者对信息自动处理的能力;Brut us是采用一阶逻辑描述密码协议的属性,从协议运行的初始状态开始搜索所有合法主体和攻击模型的活动序列来检测是否存在协议的攻击序列,并使用偏序和对称的消减方式来限制状态搜索空间.通用模型检测工具包括FDR[1]、Murφ[6]等,其中FDR是基于进程代数理论CSP的自动模型检测工具,牛津大学的Lowe首先将其用于密码协议安全性的分析,方法是将协议参与主体视为CSP进程,攻击者的进程则描述多种攻击行为,协议的安全性目标被描述为主体的事件序列;Murφ是由斯坦福大学的Mitchell应用于密码协议的分析,它在许多方面的描述类似于FDR,但它是使用共享变量来描述协议主体事件,使用不变量描述协议的安全属性,同时采用对称消减、可逆规则等技术来提高系统效率.模型检测工具更有利于通过自动推理生成攻击实例的方法来检测协议的不正确性,但在证明协议正确性时,往往很难做到将无限状态空间映射为一个有限状态空间,从而容易出现无限搜索状态空间的问题.相对于模型检测,定理证明的技术可以处理无限状态空间,因而可以提供协议的正确性证明.采用定理证明技术的NRL协议分析器[7]是比较著名的密码协议分析工具,能够分析任意数量参与主体密码协议的安全性,它是以不安全的状态为开始进行回溯搜索,如果不安全状态不能够从初始状态达到,协议就是安全的,否则就是不安全的,同时搜索的过程就是一个攻击的过程.NRL分析器的缺点是自动化程度较低,往往需要人工干预,相对效率也比较低.At hena[8,9]是Dawn Song和Sergey Berezin等结合模型检测和定理证明的方法新开发的密码协议分析工具,它使用扩展的SSM模型[8,9]描述协议的运行,采用更为紧致的状态表示方法、变量替换和消减规则来减小状态的搜索空间.At hena的证明过程类似N RL分析器,都是以不安全状态为开始进行状态搜索的,但是它对攻击者的能力做了约束,且变量替换没有类型匹配的限制,在处理复杂密码协议时,容易产生搜索状态空间爆炸问题.3　密码协议的代数模型本文采用文献[2]提出的密码协议代数(CPA)模型规范密码协议,并运用了相应的安全性分析理论.为便于理解,这里对CPA模型只作简单介绍,关于本节内容的详细论述可参见文献[2],本文未特别说明的符号和术语均与文献[2]一致.3.1　密码协议代数原子消息.　PR I M=I D∪K E Y∪GEN.其中I D表示协议中主体的名称集合;K E Y表示密钥集,013计 算 机 学 报2005年包括非对称密钥中的公私钥和对称密钥;GEN =∪a ∈ID G a ,G a 对应协议中由标识名为a 的主体生成的所有消息集.消息项可如下递归定义:(i )若t 是原子消息,则t 是消息项;(ii )若t 1,t 2是消息项,则t 1・t 2是消息项;(iii )若t 是消息项,k ∈K E Y ,则{t}k ,M A C (t ,k )和H ash (t )是消息项.其中运算符・称为联接运算;{m}k 称为加密运算,满足:{{m}k }k -1=m 和{{m}k -1}k =m , 若k =k -1则称为对称密码运算;若k ≠k -1则称为公钥密码运算;H as h (m )称为哈希函数运算,M A C (m ,k )称为消息认证码函数,满足Has h (m 1)=Has h (m 2)Ζm 1=m 2和M A C (m 1,k 1)=M A C (m 2,k 2)Ζm 1=m 2∧k 1=k 2.消息项集M 与消息运算构成一个代数系统,称为密码协议代数CPA .迁移函数.　设A 是一个CPA 代数,σ是M n ∪{Δ}到M ∪{Δ}的一个映射,若对任何b =(b 1,b 2,…,b n )∈M n ,满足σ(b )∈A [b 1,b 2,…,b n ],则称σ为A 上的一个迁移函数.这里引入一个特殊符号“Δ”,表示空的消息项.变量替换.　一个变量替换<(t )=t{t 1/x 1,t 2/x 2,…,t n /x n }表示使用项t i 替换变量x i 在t 中的所有出现项.若变量替换满足<(t )=<(t ′),则称<是项t 和t ′的合一.3.2　密码协议的形式描述以下叙述中,均假设P 是一个N 方密码协议.基本事件.基本事件可表示为三元组〈σi j (α,l ),t ,t ′〉,其中σi j (α,l )为事件函数,l 为协议的会话轮数,α=(a 1,a 2,…,a N )为参与协议会话主体集,下标i 用于标识该事件主体在α中的位置,下标j 用于标识该事件所在事件序列的序号.t 和t ′分别表示接收到和发送出的消息项,满足映射关系t ′=σi j (α,l )(t ).事件函数偏序关系ΜP ,满足σi 1j 1(α1,l 1)ΜPσi 2j 2(α2,l 2)当且仅当i 1=i 2∧α1=α2∧(l 1<l 2∨(l 1=l 2∧j 1Φj 2)).设协议P 的有限序列Γ=τ1τ2…τn ,其中τi 表示事件函数,若满足:(1)对于任何1Φi <j Φn,不存在τi ,τj 使得τj ΜP τi ;(2)当σi j (α,l )∈Γ,对于1Φk Φj ,σik (α,l )∈Γ;则称Γ是协议P 的长度为n 的一条迹.当x =(x 1,x 2,…,x n )∈M n,则称序列Γ(x )为协议P 的迹序列.密码协议的形式定义.　一个N (Ε2)方密码协议是二元组,其中,(1)M 是基本消息代数空间;(2)P =〈P 1,P 2,…,P N 〉,其中P i 是N 方协议P 的第i 个角色,对Πα=(a 1,a 2,…,a N )∈I D (N ),l ∈N ,可以导出相应事件函数序列:Σi (α,l )=σi ,1(α,l )…σi ,s i (α,l ),其中σi ,j (α,l )为协议的原子事件函数.在这里,迹Σi (α,l )称为角色P i 的正则迹.当x =(x 1,x 2,…,x n )∈M n,则称迹序列Σi (α,l )(x )为角色P i 的正则迹序列.正合序列.　设Γ=σ1σ2…σn 是迁移函数序列,对于a i ∈M ∪{Δ},可得到消息迁移序列Γ(a )=〈σ1,a 1,σ1(a 1)〉〈σ2,a 2,σ2(a 2)〉…〈σn ,a n ,σn (a n )〉,D 0是攻击者初始知识,若满足a 1∈D 0,a i ∈D i -1,D i =D i -1[σi (a i )],i =1,2,…,n ,则称Γ(a )是一个正合的D 0序列.正合序列描述了攻击者的一个攻击过程.3.3　密码协议形式分析模型3.3.1　语法1133期李建欣等:SPA :新的高效安全协议分析系统Φ(X )∈Ex t (Φ(Σ)),即X 是正合的Σ2序列.(iv )M P 4a ∈ΣX 当且仅当Φ(Σ)∈R P 且Φ(a )∈Φ(Σ)Φ(X )(a ∈ΣX 为(a ,Σ)∈X 的简记,表示a ∈D 0[X ],其中D 0是关于正则迹Σ的攻击者初始知识).对含逻辑联接词?,∧和量词Π的公式语义解释是自然的.3.3.3　密码协议安全性描述秘密性安全目标.　协议的秘密安全性是建立共享秘密协议的安全要求,目的是保护某些数据(即会话目标消息)不被攻击者获取,表示为公式其中Σ是正则迹序列,t 是秘密消息项.对应性安全目标.　认证性是鉴别传输数据来源的真实性或新鲜性.CPA 模型将数据的源认证解释为一种对应性,即当认证方的正则迹序列属于一个正合迹序列,协议预先规定的角色正则迹序列(或部分)也属于这个正合序列.表示为公式ΠX.(EX T (Σ,X )∧ΣΑX )]ΛΑX(简略形式为ΣCorresp Λ),其中Λ是某个正则迹Σj (α,l )的部分或全部(简称子迹).密码协议的安全性定义.　设M P 是协议P 的一个模型,G P 是安全目标集,若G P 中的每个公式在模型M P 中都为真,则称P 是一个安全的密码协议.4　新的安全协议分析系统(SPA )基于文献[2]中的密码协议代数(CPA )模型,我们设计并实现了一个高效的密码协议自动分析系统(Security Protocol Analyzer ,SPA ),并应用该系统成功分析了一些密码协议的安全性.本节首先简要介绍系统的总体结构,然后介绍系统中的核心算法与技术.4.1　SPA 系统的总体结构SPA 系统的整体结构框架如图1所示,下面简要介绍各个模块的主要功能.(1)协议输入及其解析模块目前的公开密码协议大多使用半自然语言描述,这种描述不太严谨,容易产生二义性.由于SPA 系统仅能处理规范好的密码协议,我们采用EBN F (Extended Backus 2Naur Form )定义了一种与CPA 模型描述语言配套的协议规范描述语言,能够准确图1　SPA 系统结构框架描述密码协议组成要素.该模块提供了协议规范文本编辑器和协议辅助生成向导两种方式生成协议规范描述文本,以满足不同用户的需求.通过对生成的协议规范描述文本进行词法和语法解析,如果符合协议描述规范语法,则执行相应的语义动作,生成描述协议的静态数据.(2)分析过程控制及其管理模块这部分的主要功能是控制整个协议的分析过程,根据用户指令启动或停止分析进程.在实际运行过程中,还需要对数据的动态交换、存储进行管理,协调各个具体功能模块,保证以最优效率完成协议的分析.(3)协议数据预处理及其初始化模块该模块主要负责协议的预处理和初始化.首先,由于在协议会话过程中引入攻击者角色,所以需要构造扮演攻击者角色主体参与的会话组,生成各会话主体新的迹序列.同时,由于密码协议大多运行在开放的网络环境中,网络数据都是公开的,所以需要确定攻击者的初始知识集合,并根据其运算能力作相应的约简操作.最后,完成协议分析的初始化工作,包括为各个角色的安全目标定理证明分配独立的运行空间,建立对应的初始状态和证明树根节点,加载可能存在的用户预设策略(用户可对分析过程的证明树的深度、宽度以及状态迹序列长度等条件进行约束).(4)角色安全目标定理证明模块在CPA 模型中,密码协议P 的安全性被规范为安全目标定理集G P ,这里关键的问题就是通过一种有效的算法来证明G P 中的每条定理.本模块主要应用状态搜索算法S earchA l g 在有限的状态空间中对角色的安全目标定理进行严格的推理证明.在状态搜索过程中,需要判定各状态的安全性,其中攻击者不可达状态、攻击者可达但不违背安全目标状态都属于安全状态,攻击者可达而且违背安全目标状态属于不安全状态,对不能判定其安全性的状态,应用分裂算法S plit 扩张迹序列并生213计 算 机 学 报2005年成新的状态集(需要保证新状态的有效性和新鲜性).(5)协议分析结果输出模块为了便于分析人员了解协议分析的过程及结果,该模块既可显示协议分析结果的信息摘要(如搜索时间、搜索状态数目、攻击序列数目等),也可以通过Tree 结构图直观显示每个角色的证明状态树.这样,对于存在安全漏洞的协议,协议分析人员就能够直观、方便地了解它的攻击过程.SPA 系统的各模块间是一种松藕合关系,其总体结构框架具有良好的可扩展性,能够方便插入针对特殊协议的附加处理模块.4.2　SPA 系统的核心算法与技术我们使用Java 语言实现了SPA 系统,下面分别介绍系统三个组成部分中的一些关键算法及技术.4.2.1　输入部分在SPA 系统的输入部分,使用递归下降子程序解析协议规范描述文本,如果解析通过,将分离出它的三个主体描述类(如图2所示),其中特定迹序列是附带参数的迹序列,用于辅助表示安全目标定理中的正则迹序列Σ或其子迹Λ.对于角色P i 的迹序列Σi (α,l )中的消息项,按照其递归定义形式表示为消息树结构,其中叶节点为原子消息项.根据这些原子消息项来源和属性(在协议规范描述文本中,各角色中的原子消息属性由对应的参数表指定)的不同,采用唯一标识索引,存入Hash 表中统一管理,以提高核心算法频繁访问这些信息的效率.图2　协议P 的三个主体描述类4.2.2　协议分析核心部分在密码协议分析核心部分,首先需要完成协议的预处理和初始化,然后启用状态搜索算法从初始状态出发对协议描述的各个角色安全目标定理证明,在状态搜索过程中所采用的分裂算法则是SPA 系统能够快速构造出攻击序列的一个关键部分.协议的预处理过程.1.在确定的会话轮数l 下,对具有s 个可信服务器角色(该角色不可由非诚实主体扮演,如证书权威机构CA 等)的n 方密码协议P ,生成(n -s )!种除可信角色外诚实主体的会话组合,在具有攻击者协同参与情形下,引入p =n -s -1个可扮演各个诚实主体角色的攻击者(p 1,p 2,…,p n -s -1),生成(n -s )种主体会话组合,最后对(n -s )!+(n -s )种组合进行对称约简.例如对于双方密码协议P =〈a ,b 〉且l =1,会话组合为(a ,b ),(b,a ),(a ,p )和(p ,b ).2.对步1中的每种主体会话组合,主要应用变量替换等算法,生成各主体新的会话迹序列.进而求得所有诚实主体的规范序列空间N or Σ=∪(N orΣi (α,l )).3.设置攻击者本身知识集合D 0,D 0包括所有诚实主体I D 及其公钥,攻击者的密钥K E Y (私钥和共享密钥)及其生成的消息GEN ,也可是协议规范预设的其它公开信息.4.构造攻击者可以通过公开网络获取协议会话的知识集合D P ={t |〈σ,s ,t 〉∈N or Σ}.5.由步3和4生成攻击者的初始知识集合D =D 0∪D p .Πd ∈D ,若d ∈D 0,则记录d 的起源d →D 0;若d ∈D p ,则根据攻击者知识集D,对d 不断进行解密、分解等约简操作,直到D 集合中不再存在可约简的消息子项,对于d 的不可约简项d 1,d 2,…,d k ,分别记录d i 的起源节点d i →〈σs ,t s ,t ′s 〉.协议的初始化过程.在SPA 中,采用三元组(A ,B ,E )表示协议的运行迹状态(简称状态),其中A 为非空迹序列,B 为安全目标节点集,E 为正合节点集.针对CPA 模型描述的两类安全目标,分别采用如下方法来构造它的初始状态:(1)对于秘密性安全目标ΣSecret t ,构建一个新节点〈σ,t ,Δ〉,相应的初始状态为s 0=(Σ∪〈σ,t ,Δ〉, , ).(2)对于对应性安全目标ΣCorresp Λ,相应的初始状态为s 0=(Σ,Λ, ).建立初始状态后,SPA 采用宽度优先的原则进行状态搜索,主要包括状态搜索算法S earchA l g 和状态分裂算法S plit.算法1.　状态搜索算法.SearchA l g (){//建立初始状态StateS et ={(A 0,B 0,E 0)};while (S tateSet != ){//选取一个待分析状态(A i ,B i ,E i )=S elect (S tateS et );//用户预设处理策略处理该状态User Policy ((A i ,B i ,E i ));//判断迹序列A i 是否包含安全目标节点if (B i ΑA i ){//状态(A i ,B i ,E i )为安全状态S tateSet.Remove (A i ,B i ,E i );continue ;}//判断迹序列A i 中节点是否已全部正合if ((B i ⁄A i )&&(A i ΑE i ))//(A i ,B i ,E i )为不安全状态,3133期李建欣等:SPA :新的高效安全协议分析系统//正合序列A i描述了协议的一个攻击return FAL SE;//应用状态分裂算法,得到子状态集LL=S plit((A i,B i,E i));for each(A l,B l,E l)∈L{//状态有效性检查if(V ali date((A l,B l,E l))//将新状态并入集合S tateSetS tateS et=S tateSet∪{(A l,B l,E l)};}//状态(A i,B i,E i)分析完毕S tateSet.Remove(A i,B i,E i);}return TRU E;//协议无攻击}对于不能判定安全性的状态s=(A,B,E),其中A=〈σ1,t1,t′1〉,〈σ2,t2,t′2〉,…,〈σn,t n,t′n〉.是一个迹序列,SPA系统依据迹序列扩张方式,应用状态分裂算法S plit(算法3)求其子状态集,能够有效扩展状态搜索空间,避免大量冗余状态的产生.在状态分裂算法中首先需要应用算法Uni f y(算法2)求解出非正合节点的接收项t与攻击者初始知识集合D 的合一变量替换集合.变量替换合并运算Ψ.令集合A={a1,a2,…,a m},B={b1,b2,…, b n},其中a i=(<,d l,a,…,d j,a),b i=(δ,d l,b,…, d j,b),<,δ为变量替换,d l,…,d j∈D.变量替换合并运算Ψ的计算规则如下:(1)若集合A={(λ,d l,a,…,d j,a)},B={(δ,d l,b,…,d j,b)},则C=Ψ(A,B)定义为如果变量替换λ,δ不矛盾,则C={(λ∪δ,d l,a,…,d j,a,d l,b,…,d j,b)}, 否则C= ;(2)若集合A或B中的元素不只一项,则C=Ψ(A,B)定义为{Ψ(a,b)|a∈A,b∈B}. 特殊情况,当A= ,Ψ(A,B)=B;当B= ,Ψ(A,B)=A.算法从略.算法2.　U ni f y.输入:消息项t,攻击者初始知识集合D输出:t的子项组合与D中项可以合一的变量替换集合S Unif yUni f y(D,t){//初始化S Unif y为空集S Uni f y= ;//按照消息项递归定义方式求项t的子项组合集T={(t1,t2,…,t m)|u(t1,t2,…,t m)=t,u为代数式}for(each t的子项组合(t1,t2,…,t m)∈T){U= ;//U初始为空集//由合一算法M GU求项t i和d i的变量替换集合for(each t i∈{t1,t2,…,t m}){U i={(λi,d i)|λi(t i)=λi(d i),λi是变量替换,为项d i和t i最一般合一,d i∈D};//应用Ψ运算规则合并变量替换集合U=Ψ(U,U i);}//所有完全子项的合一集合求并集S Uni f y=S Unif y∪U;}}算法3.　状态分裂算法.输入:待分裂的状态s=(A,B,E)输出:分裂得到的子状态集合S′S plit(s){//从A中选取第一个非正合节点〈τ,t,t′〉=Sel N oEx t N ode(A);//标识〈τ,t,t′〉的前驱节点〈ω,p,p′〉=Prev N ode(A,〈τ,t,t′〉);//初始化子状态集为空集S′= ;//通过算法2求项t与D中元素的可合一变量替换集合Uni f y(D,t)={(<,m1,…,m k)|<(t)=u{<(m1)/x1,…,<(m k)/x k},u是代数式,m i∈D,i=1,2,…,k};for(each(<,m1,m2,…,m k)∈Uni f y(D,t)){//依据迹序关系,分为如下几类情形生成新的迹序状态if(Πm i,满足m i∈D0,1ΦiΦk){//添加一个新状态S′=S′∪{(<(A),<(B),<(E)∪{<(〈τ,t,t′〉)};continue;//处理下一个(<,m1,m2,…,m k)组}//集合M R包含所有不属于D0的m iM R={m1,m2,…,m k}-{m i|m i∈D0且1ΦiΦk};对于任一个m r∈M R,根据m r→〈σs,t s,t′s〉关系表可查询到其起源节点n s=〈σs,t s,t′s〉;if(ϖm r∈M R,其起源节点n s的变量替换满足<(〈σs,t s,t′s〉)∈<(A)且〈τ,t,t′〉ΜP n s){S′=S′∪ ;//不添加新状态continue;//处理下一个(<,m1,m2,…,m k)组}if(Πm r∈M R,其起源节点n s的变量替换满足<(〈σs,t s,t′s〉)∈<(A)且n sΜP〈τ,t,t′〉){S′=S′∪{(<(A),<(B),<(E)∪{<(〈τ,t,t′〉)};//添加一个新状态continue;//处理下一个(<,m1,m2,…,m k)组}413计 算 机 学 报2005年for(每个m r∈M R){if(m r起源节点n s的变量替换满足<(〈σs,t s,t′s〉)|<(A)){//正则迹中起源节点前的节点集G(m r)={<(〈σr1(α,l),t r1,t′r1〉),…,<(〈σrj(α,l),t rj,t′rj〉)};G=∪i G(m i)-<(A); //去除在A中已存在的节点for(G中节点每个满足偏序关系ΜP的有效排列Πi){A′=<(〈σ1,t1,t′1〉)…<(〈ω,p,p′〉)+Πi+<(〈τ,t,t′〉)…<(〈σn,t n,t′n〉);//添加一个新状态S′=S′∪{(A′,<(B),<(E)∪<(〈τ,t,t′〉))};}}}}//结束所有Uni f y(D,t)中项的遍历return(S′);//返回新生成的子状态集合}值得一提的是,由于SPA系统在协议预处理期间限制了攻击者角色数量和会话轮数,依据迹序关系,可匹配的节点将逐渐减少,从而保证了分裂算法收敛.除此外,算法中的变量替换都遵循类型匹配一致原则等方法都有效减小了状态搜索空间.与Athena系统的几点比较.　卡内基・梅隆大学的Song等[8,9]基于Strand空间研制的At hena系统是一种高效的密码协议自动分析工具.SPA与At hena、NRL协议分析器等分析工具共同之处是均采用构造攻击过程的方法分析协议的安全性;然而, SPA系统与At hena等其它系统相比采用了更有效的新模型和新的算法,主要体现在如下4个方面:(1)CPA模型中对密码协议的描述方式通常比Strand空间更为简洁.例如,用CPA模型描述Needham2Schroeder公钥协议[1]仅用4个节点(迁移函数),而在Strand空间中需要6个角色节点.(2)At hena基于的St rand空间模型属于图论方法,SPA基于的CPA模型侧重的是代数方法.在Strand空间中通过攻击者St rand处理消息运算,难以解决由运算产生的消息集无限性问题,因此,需要人为限制加密深度,并且消息项运算量大;而SPA 采用具有代数等式和自由生成元(基)的CPA代数方法解决消息运算无限生成问题,不需要限制运算方式(如加密深度),即解决了消息集无限性问题,因而分析结果更可靠.(3)协议的攻击序列表示方式不同,SPA采用算法更直接有效:At hena算法中St rand节点间属于一种消息绑定关系,搜索过程中状态图(bundles)无预期地生长;而SPA中迹序列是通过攻击者知识的递增过程表示.这些区别使基于CPA的SPA系统在序列生成过程中,收敛更集中,对于一些协议会显著提高其分析效率.(4)基于St rand的At hena系统在状态搜索中主体存在变量类型,从而变量替换中可能重复替换,出现冗余.基于CPA理论的SPA中,由于已有关于主体的约简理论,在预处理阶段对不同主体扮演各个角色已做了替换,状态搜索中迹序列中的主体都为常量类型.4.2.3　输出部分在SPA系统的输出部分,协议分析人员可以获得协议分析的结果信息以及各角色安全目标定理的证明树(结构如图3所示),其中每个节点除记录该状态的自身信息外,还包括分析过程中对该状态属性的判定结果等.图3　证明树结构对于证明树中的节点P i,如果其中存储的状态s=(A,B,E)属于不安全状态,则迹序列A是一个正合序列,描述了协议的具体攻击过程.一般来说,迹序列A中的节点是经过不断扩张生成的,它的来源可能是任意一个主体的迹序列,其中的消息项也都经过了多次的变量替换、等价变换,具体形式可以在下一节的应用实例分析中了解到.对于SPA系统的实现,我们在充分考虑协议分析算法实现效率的同时,提供了友好的人机交互界面和自动处理功能,以方便协议分析人员的使用.5　SPA系统的应用SPA系统是一个有效的网络系统安全性评测以及密码协议设计辅助工具.我们借助SPA系统分析了一些典型的密码协议,得到了较理想的结果,鉴于篇幅有限,这里仅给出BAN2Yahalom协议[10]的一个新攻击过程分析.5.1　BAN2Yahalom协议分析5133期李建欣等:SPA:新的高效安全协议分析系统。