安全协议攻击序列重构技术

维普资讯 http://www.cqvip.com 第２９卷　第１３期　计算机工程与设计　２００８年７月　ＶＯ１．２９　ＮＯ．１３　Ｃｏｍｐｕｔｅｒ　Ｅｎｇｉｎｅｅｒｉｎｇ　ａｎｄ　Ｄｅｓｉｇｎ　Ｊｕｌｙ　２００８　安全协议攻击序列重构技术　张超，　韩继红，　王亚弟，　朱玉娜　（解放军信息工程大学电子技术学院，河南郑州４５０００４）　摘要：攻击者攻击序列在安全协议形式化分析技术中用于描述攻击者对安全漏洞的攻击步骤。目前，攻击序列重构技术　是安全协议形式化分析研究的热点与难点。对国际流行的方法进行了介绍和总结，重点分析和比较了基于模型检测的方　法、基于定理证明的方法、基于逻辑程序的方法等能够进行攻击序列重构的各种方法，指出了各自的优缺点及技术手段、技　术特点，最后给出了该领域的进一步研究方向。　关键词：安全协议；形式化分析；攻击序列重构；模型检测；定理证明；逻辑程序　中图法分类号：ＴＰ３０９　文献标识码：Ａ　文章编号：１０００．７０２４（２００８）１３．３３６８．０４　Ｒｅｃｏｎｓｔｒｕｃｔｉｏｎ　ｔｅｃｈｎｏｌｏｇｙ　ｏｆ　ａｔｔａｃｋ　ｓｅｑｕｅｎｃｅ　ａｇａｉｎｓｔ　ｓｅｃｕｒｉｔｙ　ｐｒｏｔｏｃｏｌｓ　ＺＨＡＮＧ　Ｃｈａｏ，ＨＡＮ　Ｊｉ．ｈｏｎｇ，Ⅵ　ＮＧ　Ｙａ—ｄｉ，　ＺＨＵ　Ｙｕ—ｎａ　（Ｉｎｓｔｉｔｕｔｅ　ｏｆ　Ｅｌｅｃｔｒｏｎｉｃ　Ｔｅｃｈｎｏｌｏｇｙ，ＰＬＡ　Ｉｎｆｏｒｍａｔｉｏｎ　Ｅｎｇｉｎｅｅｒｉｎｇ　Ｕｎｉｖｅｒｓｉｔｙ，Ｚｈｅｎｇｚｈｏｕ　４５０００４，Ｃｈｉｎａ）　Ａｂｓｔｒａｃｔ：ＡＲａｃｋ　ｓｅｑｕｅｎｃｅ　ｄｅｓｃｒｉｂｅｓ　ａｔｔａｃｋｅｒ’Ｓ　ａｃｔｉｏｎ　ｔｏｗａｒｄｓ　ｔｈｅ　ｓｅｃｕｒｉｔｙ　ｐｒｏｐｅｒｔｙ　ｏｆａ　ｐｒｏｔｏｃｏ１．Ｔｈｅ　ｒｅｃｏｎｓｔｒｕｃｔｉｏｎ　ｏｆａａａｃｋ　ｓｅｑｕｅｎｃｅ　ｔｅｃｈｎｏｌｏｇｙ　ｉｓ　ａ　ｎｅｗ　ｃｈａｌｌｅｎｇｅ　ｔｏ　ｆｏｒｍａｌ　ａｎａｌｙｓｉｓ　ｏｆｓｅｃｕｒｉｔｙ　ｐｒｏｔｏｃｏｌｓ．Ｔｈｅ　ｐｏｐｕｌａｒ　ａｐｐｒｏａｃｈｅｓ　ａｒｅ　ｉｎｔｒｏｄｕｃｅｄ　ａｎｄ　ｓｕｍｍａｒｉｚｅｄ．ｅｓｐｅｃｉａｌｌｙ　ｍｏｄｅｌ　ｃｈｅｃｋｉｎｇ　ｂａｓｅｄ　ｍｅｔｈｏｄ，ｔｈｅｏｒｅｍ　ｐｒｏｖｉｎｇ　ｂａｓｅｄ　ｍｅｔｈｏｄ，ｌｏｇｉｃ　ｐｒｏｇｒａｍｍｉｎｇ　ｂａｓｅｄ　ｍｅｔｈｏｄ　ｎａｄ　ＳＯ　ｏｎ．Ａｄｖａｎｔａｇｅｓ　ａｎｄ　ｓｈｏｒｔａｇｅｓ　ｆｏｒ　ｅａｃｈ　ｍｅｔｈｏｄ　ｒａｅ　ｐｒｅｓｅｎｔｅｄ．Ｆｉｎａｌｌｙ　ｓｔｕｄｙ　ｆｏｒ　ｆｕｔｕｒｅ　ｄｅｖｅｌｏｐｍｅｎｔ　ｉｓ　ｓｕｇｇｅｓｔｅｄ．　Ｋｅｙ　ｗｏｒｄｓ：ｓｅｃｕｒｉｔｙ　ｐｒｏｔｏｃｏｌｓ；ｆｏｒｍａｌ　ａｎａｌｙｓｉｓ；ａｔｔａｃｋ　ｓｅｑｕｅｎｃｅ；ｍｏｄｅｌ　ｃｈｅｃｋｉｎｇ；ｔｈｅｏｒｅｍ　ｐｒｏｖｉｎｇ；ｌｏｇｉｃ　ｐｒｏｇｒａｍｍｉｎｇ　０　引　言　安全性质进行验证，该验证工具能够对不安全状态构建一条　路径，该条路径就能够描述攻击序列。Ｍｉｌｌｅｎ的这种思想被后　在安全协议形式化验证技术的发展中，人们往往只注重　来的许多系统所采用。　分析安全协议的安全性质是否满足，而对有安全缺陷的协议　随着自动化验证技术的发展，攻击序列构造技术也不断　进行攻击重构并不关注。但是，在各种形式化验证方法中，分　完善，能够描述的攻击也更加简捷精确，根据攻击序列构造技　析理论往往存在缺陷，当对一个协议的安全性质得到非期望　术的实现方式目前能够对攻击序列进行构造的方法有：基于　结果时，很难分辩是协议的安全问题还是分析理论的缺陷问　模型检测的方法、基于定理证明的方法、基于逻辑程序的方法　题，而如果能够重构攻击序列，那么就能为协议的安全性质缺　以及其它方法。　陷提供充足证据。同时，根据攻击序列能够发现协议缺陷的　所在之处，从而可以对协议进行有针对性的改进。因此在安　１基于模型检测的方法　全协议形式化分析中加入攻击序列构造技术是十分必要的。　基于模型检测的安全协议分析方法是从攻击的角度对协　当安全协议的安全性质没有满足时，攻击者能通过一系列的　议进行分析，其分析过程就是攻击序列构造的过程。　动作参与到协议运行过程中达到破坏协议安全性质的目的，　模型检测方法就是对状态集的一种搜索。它首先要将协　这一系列的动作就是攻击者的攻击序列。　议系统抽象为一组有限状态集合，然后对状态集的所有状态　一般认为Ｎｅｅｄｈａｍ和Ｓｃｈｒｏｅｄｅｒ首次提出了使用形式化　进行搜索，看是否存在从初始状态到不安全状态的路径，若　的方法对协议进行分析，Ｄｏｌｅｖ和Ｙａｏ则首次使用形式化方法　有，该条路径就可以看成对协议的攻击过程。搜索的策略分　对协议进行了分析并提出了Ｄｏｌｅｖ．Ｙａｏ攻击者模型，成为以后　为前向搜索和后向搜索，前向搜索是从初始状态出发，穷尽搜　形式化分析的基础。攻击序列重构技术中的攻击者大多是基　索所有可能的转移，判断是否存在到达不安全状态的路径；后　于该攻击者模型。最早能够构造攻击序列的安全协议验证工　向搜索是从不安全状态出发，进行逆向搜索，判断是否可以回　具是由Ｍｉｌｌｅｎ开发的Ｉｎｔｅｒｒｏｇａｔｏｒ，基于状态空间搜索对协议的　溯到初始状态。　收稿日期　２００７・０７．２９　Ｅ－ｍａｉｌ：ｚｈａｎｇｃｈａｏｘｘｇｃ＠１６３．ｃｏｍ　作者简介：张超（１９８３一），男，山东德州人，硕士研究生，研究方向为计算机网络安全、安全协议自动化验证技术：　韩继红（１９６６～），女，山　西定襄人，副教授，硕士生导师，研究方向为计算机网络安全、信息系统安全：　王亚弟（１９５３一），男，甘肃兰州人，教授，博士生导师，研究方　向为计算机网络安全、信息系统安全；　朱玉娜（１９８５一），女，山东菏泽人，硕士研究生，研究方向为计算机网络安全、安全协议自动化验证技术。　・——３３６８・——　维普资讯 http://www.cqvip.com 模型检测方法要保证对协议的验证在有限时间内完成，　则需要对协议系统进行抽象限制，如限制会话方，或并行会话　数量等。但是，这种抽象限制会影响协议验证的正确性，目前　以上问题主要有两种方法解决，一种是英国学者ＧａｖｉｎＬｏｗｅ…　的研究，即构造一个小系统模型，同时证明若协议的完整系统　扩展的串空间模型不仅能够证明协议的正确性，而且可以对　有缺陷的协议进行攻击序列构造　２．２基于逻辑推理证明的方法　在该类方法中协议的描述一般采用逻辑规则，对安全性　质的证明则采用通用的定理证明器。此类方法中较有代表性　的工作有Ｗｅｉｄｅｎｂａｃｈ逻辑方法　和Ｃｏｒａｌ逻辑系统。　２．２．１　Ｗｅｉｄｅｎｂａｃｈ逻辑系统　Ｗｅｉｄｅｎｂａｃｈ首先使用逻辑规则对协议进行了形式化描　述，他以Ｎｅｕｍａｎ—Ｓｔｕｂｂｌｅｂｉｎｅ协议为例将协议原型中的参与角　模型存在攻击，则小系统模型也存在攻击，只要对小系统进行　验证即可得到结果；另一种方法则是采用状态缩减技术，剪除　不必要的搜索路径。　由于模型检测技术是通过搜索到达不安全状态的路径进　行协议验证，因此当验证出协议不安全时则协议不安全，而当　验证出协议是安全的，则不能保证对所有路径进行了完全搜　索，即无法保证协议是安全的。　基于模型检测的安全协议分析方法在自动化验证及攻击　序列构造方面有指导意义，但是存在状态空间爆炸的问题，对　协议的分析只能提供辅助性意见，而无法保证分析的完备性。　基于模型检测的方法中能够重构攻击序列的安全协议自　动化验证工具主要有：Ｉｎｔｅｒｒｏｇａｔｏｒ，ＳＰＡ　等。　２基于定理证明的分析方法　与模型检测方法相反，基于定理证明的分析方法是对安　全性质进行正面证明。　基于定理证明的分析方法主要有归纳法、阶函数分析法　和串空间分析方法及基于逻辑推理证明的方法等。归纳法和　串空间方法等是基于数学方法进行理论证明，而基于逻辑推　理证明的方法是使用定理证明器进行安全性质的证明。目前　为止能够对攻击序列进行描述和重构的则有串空间方法和基　于逻辑推理证明的方法。　２．１串空间分析方法　串空间方法是一种将图论的直观与定理证明的完备性结　合在一起的形式化分析方法。串空间是由协议参与者（诚实　主体和攻击者主体）的串组成的集合。串集合之间可以穿插　组合，使一个串的发送消息对应于另一个串的接收消息。协　议的实例用一个串空间的丛表示，对一个协议进行正确性证　明就是对协议可能形成的所有丛进行判断，看协议安全属性　是否满足。最初的串空间理论，只能够从代数方法上对协议　进行证明，而对存在代数缺陷的协议无法进行攻击序列的重　构。国内学者沈海峰Ⅲ等在串空间的代数理论基础上提出了　４条启发式规则：　（１）束的约束下，按代数结论分别确定代数结果的前提和　后件串轨迹；　（２）如果代数结果的前提和后件有不同的主体名，则认为　这个不同的主体为入侵者，更改对应的消息交换图；　（３）构造协议合法主体之间入侵者的串轨迹，使合法主体　认为自己执行了一次完整的协议；　（４）如果两个主体的束高在串轨迹中和正确束高不匹配，　则认为其中插入了入侵者。　通过以上４条规则，可以将验证出有代数缺陷的协议串　转化为有攻击者交互的攻击序列图。　此外，国内学者周永彬　等对串空间模型进行了扩展，提　出了通用串空间模型，引入了ｏｒａｃｌｅ　ｓｔｒａｎｄｓ等新的ｓｔｒａｎｄ类型。　色动作及攻击者能力抽象为一组逻辑语句，并将要验证的安　全性质抽象为逻辑结论，然后使用定理证明器ＳＰＡＳＳ对逻辑　结论进行验证。Ｗｅｉｄｅｎｂａｃｈ的逻辑系统在验证过程中存在不　可终结情况，通过对不可终结情况的分析可以得到对协议的　一种攻击情况。Ｗｅｉｄｅｎｂａｃｈ逻辑系统没有提供攻击序列重构　机制，对安全协议缺陷的查找是基于逻辑系统验证结果的，通　过对不可终结情况以及安全性质的逻辑结论验证结果进行静　态分析找出一个协议的缺陷。　２．２．２　Ｃｏｒａｌ逻辑系统　２００３年Ｇｒａｈａｍ　Ｊ．Ｓｔｅｅｌ结合Ｐａｕｌｓｏｎ的归纳法中的迹概念　与Ｃｏｍｏｎ和Ｎｉｅｕｗｅｎｈｕｉｓ的逻辑反证理论形成一套能够自动　生成攻击迹序列的系统，并基于ＳＰＡＳＳ开发出相应的自动化　验证工具Ｃｏｒａｌ『６】。　Ｓｔｅｅｌ的主要思想在于对不正确定理的证明，即通过将需　证明的安全性质形式化为一条定理，用协议本身和攻击者的　能力形成的知识库去证明定理的不正确性，证明过程就是一　种对该安全性质的攻击过程。　Ｓｔｅｅｌ对攻击序列进行重构的方法是在逻辑推导的过程中　加入了迹的概念，将所有可能的消息收发都加入到迹中，协议　的运行就形成了一条有效迹，当证明出表示安全性质的命题　不成立时对有效迹进行搜索就可以得到攻击序列。　３基于逻辑程序的方法　基于逻辑程序的形式化分析方法是将对安全协议安全性　质的验证转换为逻辑系统中对逻辑规则的可推导判定问题。　基于逻辑程序的分析方法易于自动化实现，而且每条逻辑规　则能够对应到相应的协议步骤或攻击者能力，因此在推导过　程中记录必要的信息可以对攻击序列进行重构。在基于逻辑　程序的分析方法中比较有代表性的工作有，Ｂｌａｎｃｈｅｔ的ＰｒｏＶｅｒｉｆ　验证器　“　和我国学者李梦君开发的ＳＰＶＴ“　。　３．１　ＰｒｏＶｅｒｉｆ逻辑系统　２００２年Ｂｌａｎｃｈｅｔ基于一阶Ｈｏｒｎ逻辑提出一套安全协议　分析理论，并开发出协议验证器ＰｒｏＶｅｒｉＬ与Ｗｅｉｄｅｎｂａｃｈ逻辑　系统所不同的是Ｂｌａｎｃｈｅｔ逻辑系统对协议本身的建模是从攻　击者的角度进行的，并且系统对每条消息的交互进行了更严　格的限制，攻击者要发出一条消息必须收到协议规范中该条　消息之前的所有消息。　Ｂｌａｎｃｈｅｔ使用扩展的ｐｉ演算对协议系统进行描述，通过　一组转换规则将协议的扩展ｐｉ描述转换为一组Ｈｏｒｎ逻辑，　并在验证中使用基于归结的验证算法对安全性质进行推理。　Ｂｌａｎｃｈｅｔ在规则归结过程中通过权重对规则的推理进行限　－——３３６９－——　维普资讯 http://www.cqvip.com

制，有效地避免了不可终结情况。Ｂｌａｎｃｈｅｔ逻辑系统体系如　图１所示。　动验证器ＳＰＶＴ。ＳＰＶＴ的系统体系同ＰｒｏＶｅｒｉｆ系统体系相同，　只是在推理策略中的不动点计算和攻击序列重构处理机制方　面不同。　与Ｂｌａｎｃｈｅｔ的理论相比李梦君提出的逻辑系统更具高效　性。对避免不可终结情况提供了更完善的措施，并且对攻击　序列的重构更加有效，生成的反例规则更加形象。　李梦君对扩展的ｐｉ演算的改进基于下面的输入进程和输　出进程　图１　Ｂｌａｎｃｈｅｔ逻辑系统体系　Ｃ（ｒｏｌｅ（＜Ｍ，Ｎ，ｔａｇ＞，ｘ））．Ｐ　输入进程　ｃ．（ｒｆＪｚＰ（＜　Ⅳ’姐ｇ＞　，）．Ｐ　输出进程　Ｂｌａｎｃｈｅｔ在ｐｉ语法中加入了构造器和析构器用于描述加　在输入进程中　ⅡⅣ分别标识消息　的理想发送者和实际　解密操作，并在一阶Ｈｏｍ逻辑语法中使用合一来表示消息的　收发。在ｐｉ语法中加入了构造器和析构器　Ｍ，…，　）　构造器　ｌｅｔｘ＝　Ｍ，…，　）ｉｎＰ　析构器　Ｈｏｍ逻辑语法中的蕴含关系　：：＝　规则　Ａ…Ａ　一Ｆ　蕴含　Ｂｌａｎｃｈｅｔ工作的主要贡献在于：　（１）给出一个经典的基于逻辑程序的框架，扩展了易于表　达和理解的ｐｉ语法，加入了用于描述加解密操作的原语，并使　用扩展的ｐｉ语法进行协议描述，并基于归结提出高效的算法　进行逻辑推理；　（２）对协议分布式的系统进行了更深入的研究，改进了逻　辑规则对消息收发的表达，在一定程度上保证了消息在协议　原型中的收发顺序，从而保证了攻击序列重构时消息出现的　先后次序；　（３）研究了逻辑推理中的不可终结情况，并引入了权重的　思想，在很大程度上保证了推理的可终结性，并且大大减少了　攻击序列重构时对冗余推导过程的搜索；　（４）将协议原型形式化为一组规则，规则的归结过程代表　了协议消息的交互，突破了对并行会话数量的限制。　２００５年Ｂｌａｎｃｈｅｔ对ＰｒｏＶｅｆｉｆ理论进行改进““，加入了用于　记录推理过程的信息，使得验证器能够对不满足安全性质的　协议重构攻击序列。在扩展的ｐｉ演算中对复制进程和输入进　程进行了扩展，加入了标识。　！　Ｐ　复制进程　ｘ　．Ｐ　输入进程　在复制进程中　用于标识进程的不同副本，输入进程中的　用于标识进程的哪个副本发出了消息　。　相应的，在逻辑系统中对蕴含规则也加入了标识　Ａ…Ａ，＾一Ｆ，其中　为运行标识，表示一条消息的实际发出　者，，表示当前的会话标识符。二元组（　用来记录会话标识　为朋ｑ会话主体收到运行标识为　的消息后发出一条消息。　ＰｒｏＶｅｒ／ｆ通过记录推理过程中的运行标识和会话标识来　对攻击序列进行重构，但是其输入的序列是以进程的方式进　行描述，并没有说明该进程的类型，不利于理解。　３．２　ＳＰＶＴ逻辑系统　我国学者李梦君对逻辑程序验证方法也进行了深入研　究，提出了一套与Ｂｌａｎｃｈｅｔ相似的推理分析方法，并开发出自　－——３３７０———　接收者，ｔａｇ取值为ｔｒｕｅ表明消息Ｘ被安全协议的诚实参与者接　收。在输出进程中　和Ⅳ分别标识消息　的发送者和理想接收　者，ｔａｇ取值为ｔｒｕｅ表明消息　由安全协议的诚实参与者发送。　相应的，在一阶逻辑系统中对ａｔｔａｃｋｅｒ谓词也进行了扩展，　ａｔｔａｃｋｅｒ（ｒｏｌｅ＜Ｍ￣，ｔａｇ＞，ｘ），ａｔｔａｃｋｅｒ谓词表示攻击者获得Ｍ发出　的消息　，并且Ｍ认为Ⅳ为合法的消息接收者，ｔａｇ值取真表示Ｍ　为诚实角色。这样通过对ａｔｔａｃｋｅｒ￥￣词进行扩展，就可以在推　理过程中保留消息发送和接收的信息，为攻击序列构造提供　了充分的条件。在逻辑推理中为了对攻击序列进行构造，李　梦君提出了反例规则反例树的概念。在构造反例树的基础上，　通过对反例树的深度优先搜索来自动生成反例规则。　４其它方法　除了以上所述的各种方法外，还有一类协议分析器将多　种技术结合到一起用于自动化验证并生成攻击序列。　Ｓｏｎｇ结合串空间、模型检测技术和定理证明的方法开发　出Ａｔｈｅｎａ系统ｆｔ２］，Ｓｏｎｇ提出了一种用于推理串空间和束的逻　辑方法，在该逻辑中，安全性质被描述为正规式。给定一个协　议和安全性质，系统将采用一个自动化的算法来验证安全性　质。在验证时，系统从初始状态开始，依据ｉｎｉｔ、ｉｆｎａｌ和ｓｐｌｉｔ规　则，进行状态转化，并对新状态进行验证，当发现状态不满足　所要求的性质时算法终止。　Ａｔｈｅｎａ系统使用状态来表示协议主体交替执行的顺序。　另外，系统中的规则也与一般的定理证明器的规则不同，系统　中的规则是可逆的，因而，当验证出协议有漏洞时不需要对证　明过程进行回溯就可以得到攻击序列，而一般的定理证明器　的要得到具体的推导过程必须对证明过程进行记录以便回　溯。Ａｔｈｅｎａ系统所采用的策略保证了攻击序列重构时的快捷　和有效。虽然Ａｔｈｅｎａ系统在状态搜索中采用了定理证明的策　略，并且通过限制并行会话数量来避免“状态空间爆炸”问题，　但是验证过程并不能保证一定可以终止。　５结束语　各种方法的比较如表１所示。　综上所述，在攻击序列重构技术方面仍存在诸多问题亟　待解决：①攻击序列构造效率不高，各种方法中只有基于模型　检测的方法和Ａｔｈｅｎａ系统中的验证过程与攻击序列构造过程　是一致的，其它方法都是验证完闭后对验证过程进行逆推导　来实现攻击序列重构：②攻击序列的表现形式易读性差，需要　维普资讯 http://www.cqvip.com

…　表１　形式化方法攻击序列重构技术比较　类别　方法（自动化验证器）　攻击序列构造方法　’　优点　局限性　基于模型检测方法　Ｉｎｔｅｒｒｏｇａｔｏｒ，ＳＰＡ　自动构造　自动化程度较高，验证过程即攻击序列　重构过程１．存在状态空间爆炸问题；　。　２．不能满足完备性。　扩展串空间方法　静态分析　与图论结合；分析直观；满足完备性。　自动化程度不高，还没有完全基于　串空间的自动化工具　定理证明方法　Ｗｅｉｄｅｎｂａｃｈ逻辑系统　根据验证过程或结果进行　静态分析　验证过程自动化程度较高。　１无法自动构造攻击序列；２　．存在不可终结情况。　Ｃ结合了归纳法、定理证明与逻辑程序，在攻击　验证器基于ＳＰＡＳＳ开发，没有形成　ｏｒａｌ逻辑系统　自动构造　序列构造方面有较高效率。　专用验证器，效率有待提高　ＰｒｏＶｅｒｉｆ逻辑系统　自动构造　１．不可终结情况较少；２．规则表达消息收发的　１、攻击序列的表现形式可读性不　基于逻辑程序的方法　方式易于攻击序列重构。　强：２．会产生错误报告。　ＳＰＶＴ逻辑系统　自动构造　与ＰｒｏＶｅｒｉｆ逻辑系统相比，不可终止情况更少。　攻击序列可读性不强。　其它　Ａｔｈｅｔ１ａ系统　自动构造　１．规则较少，推理过程简单；序列重构时无须对推理过程回溯２．规则可逆，攻击　１存在状态空间爆炸问题；　；　２．不能满足完备性。　相关知识的支持。应加入攻击序列到自然描述的转化机　ｏｆＥｄｉｎｂｕｒｇｈ，２００２．　制；③目前大多数研究集中在认证性和秘密性的验证方面，对　［７】　Ｂｌａｎｃｈｅｔ　Ｂ．Ａｎ　ｅｆｉｆｃｉｅｎｔ　ｃｒｙｐｔｏｇｒａｐｈｉｃ　ｐｒｏｔｏｃｏｌ　ｖｅｒｆｉｅｒ　ｂａｓｅｄ　其它安全性质的攻击序列重构技术研究较少。下一步研究应　ｏｎ　ｐｒｏｌｏｇ　ｒｕｌｅｓ［Ｃ］．Ｃａｐｅ　Ｂｒｅｔｏｎ，Ｎｏｖａ　Ｓｃｏｔｉａ，Ｃａｎａｄａ：Ｐｒｏｃ　ｏｆ　扩大攻击序列重构技术的应用范围。　１４ｔｈ　ＩＥＥＥ　Ｃｏｍｐｕｔｅｒ　Ｓｅｃｕｒｉｙｔ　Ｆｏｕｎｄａｔｉｏｎｓ　Ｗｏｒｋｓｈｏｐ，２００　ｌ：　参考文献　８２．９６．　［８】　Ａｂａｄｉ　Ｍ，Ｂｌａｎｃｈｅｔ　Ｂ．Ａｎａｌｙｚｉｎｇ　ｓｅｃｕｒｉｔｙ　ｐｒｏｔｏｃｏｌｓ　ｗｉｔｈ　ｓｅｃｒｅｃｙ　Ｌｏｗｅ　Ｇ．Ｔｏｗａｒｄｓ　ａ　ｃｏｍｐｌｅｔｅｎｅｓｓ　ｒｅｓｕｌｔ　ｆｏｒ　ｍｏｄｅｌ　ｃｈｅｃｋｉｎｇ　ｏｆ　ｔｙｐｅｓ　ａｎｄ　ｌｏｇｉｃ　ｐｒｏｇｒａｍｓ［Ｃ］．Ｊｏｎｅｓ　ＮＤ，Ｌｅｒｏｙ　Ｘ．Ｐｒｏｃ　ｏｆ　ｔｈｅ　ｓｅｃｕｒｉｔｙｐｒｏｔｏｃｏｌｓ［Ｊ］．Ｊｏｕｒｎａｌ　ｏｆＣｏｍｐｕｔｅｒ　Ｓｅｃｕｒｉｔ￣１９９９，７（２，３）：　２９ｔｈ　ＡＣＭ　ＳＩＧＰＬＡＮ—ＳＩＧＡＣＴ　Ｓｙｍｐ　ｏｎ　Ｐｒｉｎｃｉｐｌｅｓ　ｏｆＰｒｏｇｒａｍ．　８９．１４６．　ｍｉｎｇ　Ｌａｎｇｕａｇｅｓ．Ｐｏｒｔｌａｎｄ：ＡＣＭ　Ｐｒｅｓｓ．２００２：３３－４４．　李建欣，李先贤，卓继亮，等．ＳＰＡ：新的高效安全协议分析系统　［９】　Ｂｌａｎｃｈｅｔ　Ｂ．Ｆｒｏｍ　ｓｅｃｒｅｃｙ　ｔｏ　ａｕｔｈｅｎｔｉｃｉｙｔ　ｉｎ　ｓｅｃｕｒｉｙｔ　ｐｒｏｔｏｃｏｌｓ　［Ｊ］．计算机学报，２００５，２８（３）：３０９．３　ｌ　８．　［Ｃ】．Ｃｏｕｓｏｔ　Ｐ．Ｐｒｏｃ　ｏｆｔｈｅ　９ｔｈ　Ｉｎｔ’ｌ　Ｓｔａｔｉｃ　Ａｎａｌｙｓｉｓ　Ｓｙｒｕｐ．ＬＮＣＳ　沈海峰，黄河燕，陈肇熊．串空间代数缺陷到实际攻击的转换［Ｊ］．　２４７７，Ｍａｄｒｉｄ：Ｓｐｒｉｎｇｅｒ－Ｖｅｒｌａｇ，２００２：２４２—２５９．　计算机科学，２００５，３２（７）：９０．９２．　［１０】　李梦君，李舟军，陈火旺．ｓＰＶＴ：一个有效的安全协议验证工具　周永彬，冯登国，季庆光，等．Ｓｔｕｄｙ　ｏｎ　ｓ￣ａｎｄ　ｓｐａｃｅ　ｍｏｄｅｌ　ｔｈｅｏｒｙ　［Ｊ］．软件学报，２００６，１　７（４）：８９８．９０６．　［Ｊ］．计算机科学与技术学报（英文版），２００３，ｌ　８（５）：５５３．５７０．　Ｘａｖｉｅｒ　Ａｌｌａｍｉｇｅｏｎ，Ｂｒｕｎｏ　Ｂｌａｎｃｈｅｔ．Ｒｅｃｏｎｓｔｒｕｃｔｉｏｎ　ｏｆ　ａｔｔａｃｋｓ　Ｃｈｒｉｓｔｏｐｈ　Ｗｅｉｄｅｎｂａｃｈ．Ｔｏｗａｒｄｓ　ａｎ　ａｕｔｏｍａｔｉｃ　ａｎａｌｙｓｉｓ　ｏｆ　ｓｅｃｕ—　ａｇａｉｎｓｔ　ｃｒｙｐｔｏｇｒａｐｈｙ　ｐｒｏｔｏｃｏｌｓ［Ｃ】．Ａｉｘｅｎ—Ｐｒｏｖｅｎｃｅ，Ｆｒａｎｃｅ：　ｒｉｙｔ　ｐｒｏｔｏｃｏｌｓ　ｉｎ　Ｆｉｒｓｔ—ｏｒｄｅｒ　ｌｏｇｉｃ［Ｃ】．Ｔｈｅ　１６ｔｈ　Ｉｎｔ’ｌ　Ｃｏｎｆ　ｏｎ　Ｐｒｏｃｅｅｄｉｎｇｓ　ｏｆ　ｔｈｅ　ｌ　８ｔｈ　ＩＥＥＥ　Ｃｏｍｐｕｔｅｒ　Ｓｅｃｕｒｉｔｙ　Ｆｏｕｎｄａｔｉｏｎｓ　Ａｕｔｏｍａｔｅｄ　Ｄｅｄｕｃｔｉｏｎ，Ｕ　ＡＩ　１　６３２．Ｔｒｅｎｔｏ，Ｉｔａｌｙ：Ｓｐｒｉｎｇｅｒ—Ｖｅｒｌａｇ，　Ｗｏｒｋｓｈｏｐ，２００５：１４０—１　５４．　ｌ　９９９：３　１４．３２８．　［１２】　Ｓｏｎｇ　Ａ　Ｐ　Ｄ，Ｂｅｒｅｚｉｎ　Ｓ．Ａｔｈｅｎａ：ａ　ｎｏｖｅｌ　ａｐｐｒｏａｃｈ　ｔｏ　ｅｆｉｆｃｉｅｎｔ　ａｕ—　Ｇｒａｈａｍ　Ｊ　Ｓｔｅｅ１．Ｄｉｓｃｏｖｅｒｉｎｇ　ａ￣ａｃｋｓ　ｏｎ　ｓｅｃｕｒｉｙｔ　ｐｒｏｔｏｃｏｌｓ　ｂｙ　ｒｅ—　ｔｏｍａｔｉｃ　ｓｅｃｕｒｉｙｔ　ｐｒｏｔｏｃｏ　１［Ｊ］＿Ｊｏｕｒｎａｌ　ｏｆ　Ｃｏｍｐｕｔｅｒ　Ｓｅｃｕｒｉｙｔ，　ｆｕｔｉｎｇ　ｉｎｃｏｒｒｅｃｔ　ｉｎｄｕｃｔｉｖｅ　ｃｏｎｊｅｃｔｕｒｅｓ［Ｄ】．Ｓｃｏｔｌａｎｄ：Ｕｎｉｖｅｒｓｉｔｙ　２００　ｌ（９）：４７．７４．　（上接第３３６７页）　［２】　Ｄｉｌｉｇｅｎｔｉ　Ｍ，Ｃｏｅｔｚｅｅ　Ｆ　Ｍ，Ｌａｗｒｅｎｃｅ　Ｓ，ｅｔ　ａ１．Ｆｏｃｕｓｅｄ　ｃｒａｗｌｉｎｇ　ｂａｓｅｄ　ｗｅｂ　ｃｒａｗｌｅｒ［Ｃ］．Ｐｒｏｃｅｅｄｉｎｇｓ　ｏｆ　Ｉｎｆｏｒｍａｔｉｏｎ　Ｔｅｃｈｎｏｌｏｇｙ：　ｕｓｉｎｇ　ｃｏｎｔｅｘｔ　ｇｒａｐｈｓ［Ｃ】．Ｐｒｏｃｅｅｄｉｎｇｓ　ｏｆ　ｔｈｅ　２６ｔｈ　Ｉｎｔｅｎｒａｔｉｏｎａｌ　Ｃｏｄｉｎｇ　ａｎｄ　Ｃｏｍｐｕｔｉｎｇ．Ｗａｓｈｉｎｇｔｏｎ，ＤＣ：ＩＥＥＥ　Ｃｏｍｐｕｔｅｒ　Ｓｏ—　Ｃｏｎｆｅｒｅｎｃｅ　ｏｎ　Ｖｅｒｙ　Ｌａｒｇｅ　Ｄａｔａ　Ｂａｓｅｓ．Ｃａｉｒｏ：Ｍｏｒｇａｎ　Ｋａｕｆ－　ｃｉｅｔｙ，２００４：３３７—３４１．　ｍａｎｎ　Ｐｕｂｌｉｓｈｅｒｓ，２０００：５２７—５３４．　［６】　曾义聪，杨贯中，刘柯．基于概念树的主题爬取技术研究【Ｊ］．科学　［３］　Ｂｅｒｇｍａｒｋ　Ｄ，Ｌａｇｏｚｅ　Ｃ，Ｓｂｉｔｙａｋｏｖ　Ａ．Ｆｏｃｕｓｅｄ　ｃｒａｗｌｓ，ｔｕｎｎｅｌｉｎｇ，　技术与工程，２００５，５（１２）：７８５．７９０．　ａｎｄ　ｄｉｇｉａｔｌ　ｌｉｂｒａｒｉｅｓ［Ｃ］．Ｐｒｏｃｅｅｄｉｎｇｓ　ｏｆｔｈｅ　６ｔｈ　Ｅｕｒｏｐｅａｎ　Ｃｏｎｆｅ—　［７】　Ｅｄｇｉｎｇｔｏｎ　Ｃｈｏｉ　Ｂ，Ｋａｔｈｅｒｉｎｅ　Ｈｅｎｓｏｎ，ｅｔ　ａ１．Ａｄｏｐｔｉｎｇ　ｏｎｔｏ—　ｒｅｎｃｅ　ｏｎ　Ｒｅｓｅａｒｃｈ　ａｎｄ　Ａｄｖａｎｃｅｄ　Ｔｅｃｈｎｏｌｏｇｙ　ｆｏｒ　Ｄｉｇｉｔａｌ　Ｌｉｂｒａ—　ｌｏｇｙ　ｔｏ　ｆａｃｉｌｉｔａｔｅ　ｋｎｏｗｌｅｄｇｅ　ｓｈａｒｉｎｇ［Ｃ］．Ｎｅｗ　Ｙｏｒｋ：ＡＣＭ　Ｐｒｅｓｓ，　ｒｉｅｓ．Ｌｏｎｄｏｎ：Ｓｐｒｉｎｇｅｒ－Ｖｅｒｌａｇ，２００２：９１—１０６．　２００４：８５．９０．　［４】　Ｅｈｒｉｇ　Ｍ，Ｍａｅｄｃｈｅ　Ａ．Ｏｎｔｏｌｏｇｙ—ｆｏｃｕｓｅｄ　ｃｒａｗｌｉｎｇ　ｏｆｗｅｂ　ｄｏｃｕ—　［８］　Ｃｈｅｎｇ　Ｊｉｎｇ，Ｌｉ　Ｑｉｎｇ，Ｗａｎｇ　Ｌｉｐｉｎｇ，ｅｔ　ａ１．Ａｕｔｏｍａｔｉｃａｌｌｙ　ｍｅｎｔｓ［Ｃ］．Ｐｒｏｃｅｅｄｉｎｇｓ　ｏｆｔｈｅ　ＡＣＭ　ｓｙｍｐｏｓｉｕｍ　ｏｎ　Ａｐｐｌｉｅｄ　ｃｏｍ—　ｇｅｎｅｒａｔｉｎｇ　ａｎ　ｅ－ｔｅｘｔｂｏｏｋ　ｏｎ　ｔｈｅ　ｗｅｂ［Ｃ】．Ｌｅｃｔｕｒｅ　Ｎｏｔｅｓ　ｉｎ　ｐｕｔｉｎｇ．Ｎｅｗ　Ｙｏｒｋ：ＡＣＭ　Ｐｒｅｓｓ，２００３：１１７４—１１７８．　Ｃｏｍｐｕｔｅｒ　Ｓｃｉｅｎｃｅ　３　１４３．Ｂｅｒｌｉｎ：Ｓｐｒｉｎｇｅｒ—Ｖｅｒｌａｇ　Ｈｅｉｄｅｌｂｅｒｇ，　［５］　Ｇａｎｅｓｈ　Ｓ，Ｊａｙａｒａｊ　Ｍ，ＳｒｉｎｉｖａｓａＭｕｒｔｈｙ　Ｖ　Ｋ，ｅｔ　ａ１．Ｏｎｔｏｌｏｇｙ一　２００４：３５．４２．　３３７１