资源描述：
《安全协议形式化分析的不变式生成技术》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。
1、第19卷第1期中国科学院研究生院学报Vol119No112002年3月JournaloftheGraduateSchooloftheChineseAcademyofSciencesMarch2002简报3安全协议形式化分析的不变式生成技术112范红冯登国郭金庚(1中国科学院研究生院信息安全国家重点实验室,北京100039;2解放军信息工程大学安全学院计算机系,郑州450004)(2001年9月19日收稿;2001年10月19日收修改稿)摘要给出了应用于不同系统的不变式的概述,分析了彼此之间的关系,进
2、行了分类,并探讨了其未来发展趋势.密码协议的形式化分析日渐引起人们的广泛关注.这导致了不变式生成与描述技术的发展.不变式是对入侵者可知和不可知消息的定义,可用于协议认证和秘密性的证明,从而成为许多协议形式化分析工具和技术的核心.关键词协议,形式化分析,不变式中图分类号TP3091引言近年来,围绕着安全协议形式化分析工作主要集中于开发推证的归纳技术,即对协议执行数目不限,并且在一个入侵者可对数据进行任意操作的环境下产生的无限消息集合的推证归纳技术.这一技术是通过构造一个不会随协议执行而改变的不变式来加
3、以实现的.如:NRL分析器使用的语言,Schneider在其[1]基于CSP分析中用的秩函数,strandspace的理想,Paulson的analyzt和synth函数,以及Cohen的秘密不变式.所有这些技术的共性是:描述不为协议的合法参与者和入侵者的行为改变的消息集合的属性.这种属性分为两大类,一类为入侵者不可知术语的属性,或只在特定条件下可知术语的属性,诸如前面提到的strandspace的理想,NRL分析器语言和Schneider的秩函数.另一类为入侵者可知术语的属性,如Paulson的a
4、nalyzt和synth函数.本文将主要介绍不同系统中所使用的不变式的类型,这七个系统是:NRL分析器,strandspace模型,新旧版本的Schneider的秩模型,Paulson的归纳模型,strandspace模型与归纳模型相结合的用于推证秘密的模型和Cohen的TAPS.从而系统地分析这些系统中不变式的分类及其共性与个性.2模型与技术211协议模型[2]一般而言,协议模型包括一些发送和接收消息的诚实的主体,以及用于管理消息发送和接收的规则.这些消息可被入侵者截取、重放和篡改.入侵者将所有已
5、知的消息放入其知识集合KS(knowledgeset)中.诚实主体发送的任何消息将被加入到入侵者的KS中.而且,入侵者可对KS中的消息进行操作,所得消息也将[3]加入到KS中.可进行的操作至少包括级联、分离、加密和解密.协议模型抽象如图1所示.以下我们给出几个相关的定义.3973资助项目(G1999035802)和国家杰出青年科学基金资助项目(60025205)范红,女,1969年7月生,博士生;E2mail:pkfanhong@sina1com92中国科学院研究生院学报第19卷图1协议模型Fig1
6、1Protocalmodel定义211协议的执行由主体发送和接收消息的序列构成.如果一个主体接收的每一个消息都对应于某个主体发送的一个消息,则称此协议执行为可完全倒推的.如果一个主体发送的每一个消息都对应某个主体接收的一个消息,则称此协议执行为可完全前推的.定义212状态包括入侵者的KS和诚实主体在某一给定时间点的局部变量值.状态迁移是指发送和接收消息或局部变量值的变化引起的从一个状态到另一个状态的移动.协议执行深度是指协议状态迁移的次数.212形式化分析技术[4]目前安全协议形式化分析技术分为3类
7、.一类是以BAN逻辑为代表的逻辑证明技术.由于其不涉[5]及不变式的生成,故在此不作进一步的讨论.二是定理推证技术,通常涉及证明不变式在状态迁移中保持不变的属性.三是状态探测技术,它往往与定理推证相结合使用.如NRL分析器自动生成和证明不变式以限定搜索空间,并对有限空间进行穷尽搜索.所有状态探测和不变式生成都可使用前推和倒推搜索.当不变式生成和验证时,可作以下证明:若不变式在某一状态下成立,则在任一状态迁移后亦成立.或者,若不变式在某一状态下不成立,则在紧接其前的状态下亦不成立.使用前推搜索时,对所
8、有目前未与接收消息匹配的发送消息与规则中包含的接收消息进行匹配.一旦匹配成功,规则中的任何接受消息则以适当的暂时顺序加入到执行中.此过程持续进行,直到实现完全前推,或中止于某些停止规则上.倒推搜索是极其类似的.假设最终的状态是不安全的,即协议运行中违反正确说明的状态.如秘密已被入侵者获知,本应共享密钥的一对主体却持有不同的密钥等.对不安全状态给出说明后,则搜索其输出与不安全状态匹配的规则.若这些规则中包含未匹配的接收消息,则搜索包含与接收消息相匹配的发送消息的规则,并
