关于针对密码协议的形式验证.doc

HR Planning System Integration and Upgrading Research ofA Suzhou Institution密码协议的形式验证摘要：无线通信在设计合适的安全协议方而，设置了一定数量的限制导致了着重于无线应用 的新协议诞生其中的一些协议缺点明显形式验证是是增加安全协议的信赖所必不可少的 部分本文将讨论形式验证的不同方法以一个针对无线通信的安全协议，运用一个逻辑模 型来表示的形式确认作为例子关键词：安全协议，协议确认，确认逻辑，认证，移动安全1.绪论无线通信为安全协议的设计设置了一些限制用于这类通信的移动设备，通常只有限的 计算和储存能力况且，用户和网络Z间的带宽通常是限定的；因此通过无线电接口发送的 信息必须保持最小值由于这些约束，以及其它需要注意的方面如匿名，所以常规的协议不 适于无线通信导致一些着重于无线应用的新协议诞生包括ASK协议[l], ASPeCT协议⑵ 和Wong-Chan协议⑶一些其他的候选的认证协议如最近Park[4]和Yietal提出的协议，□.经 被发现了很多缺点[6][7]O已经发布的协议所存在的缺点，表明了源协议的设计是非常复杂和容易出错的过程。

已 经证明非正式技术在协议验证方面的不足正式的验证技术提供了一种提高协议安全的手段 这种技术强制执行了最初设想的明确规范以及协议的冃标，因此协议范閑的定义而且，由 于这个方法的本质，以系统性的方式发现协议的弱点但是检测弱点的能力与所用技术的限 制相关的本文讨论形式验证的不同方法大概的方法包括状态机，代数项重写技术，定理证明技 术和逻辑模型而且，通过逻辑基础技术证明形式确认的进程是一项安全的协议本文着重 于形式确认的优点，并鼓励推广这项技术2.形式协议确认形式证明是确保密码协议安全的必要步骤一些技术可以用来分析协议的安全性包括 状态机，代数项重写技术，定理证明技术和逻辑模型2.1.状态机状态机运用一项可达性分析技术［8］的方法分析协议运用这项协议，系统的全局状态由 每一个过渡表示然后分析每一个全局状态是否发现有状态协议上的错课导致攻击者获得了 访问保密信息权限一个详细的研究证实了所有可达到状态都是安全的可达性分析适丁判 别一个协议是否匹配其规格，但并不保证被主动袭击时动安全性这项其它的一系列限制是 需耍通过极端的假定来保持较小的状态空间［9］一些状态机并没有明确针对安全协议分析的设计这些工具［10］的一个问题在于不能辨 别安全领域内细微的缺陷，如应对攻击。

特别针对协议分析设计的工具可以应对攻击，但会 受限于所有状态机的影响基于纯状态空间研究的方法可以判别一个协议是否包含了一个已 经定义的缺陷，却不太可能发现协议中不明种类的缺陷由丁有这些缺陷的存在，所以即便 基于状态机的技术可以与其他技术高效率地结合，却是永远也不能取代其他的验证技术状 态机的研究效率低下，经常不确定（由于空间太大而不能分析）和不能找出新的错误；因此 协议设计人员很少使用22代数项盍写技术代数项重写技术与状态机非常和像但是状态机技术由不安全的状态开始，试图表明不 存在从原始状态通向不安全状态的路径与Z相比，代数项重写技术适于初始的状态规格 努力证明不能到达不安全状态尽管代数项重写技术与所有的方法有关，由于可以发现新协 议的缺点，所以还是比常规状态机有所发展但是这项技术始终受一系列的限制一个问题是只考虑已经被系统描述的行为合理地 使用并没有充分代表入侵者发出的信息可以考虑窃听与冋应攻击，但当入侵者采用新信息 时，这项技术便失败了代数项重写的另一个问题就是复杂，这减轻了它对程序设计人员的 吸引2.3.原理证明技术手工生产证明是很难生产的针对原理证明用来协助数学命题的证明的工具已经被开发 出来。

在用户知道每一个阶段的证明下，这些程序允许一步一步地进入和证明数学陈述因 为一个安全协议可以被精确指定，精确无误的公式可以被定义，给定协议的在设定情景是安 全的状态能用精确的数学项解释这种陈述能够进入一个原理证明而证明的研究也可以进行然而，原理的证明方法在展示协议的正确性方面比找出协议被攻击的漏洞方面做得好 况且，一个原理证明要求用户通过证明找出正确合理直观可行的路径因此源程序的验证有 可能由丁操作者缺乏经验而失败尽管有诸多限制，原理证明还是对协议设计人员有利的， 尤其是与其他技术融合的时候2.4.模型逻辑运用逻辑的安全协议形式验证在以前被认为是安全的协议中发现了一些缺陷［HJ|12Jo逻 辑技术涉及演绎推理的进程，在其中所希望的协议冃标是通过对假定应用一些公理和推导规 则来演绎，以及通知协议的交换［12］o接下来的一节以GNY逻辑为例，描述了基于协议验证 的逻辑方法2.4.1. GNY 逻辑Gong, Needham和Yahalom［ll］的逻辑通常称为GNY逻辑GNY逻辑是用作正式的验 证密码协议表一为本文中所用GNY的构成，更多的细节和完全的描述参阅［11］用GNY 逻辑验证一个协议，必须进行一下步骤：1. 协议形式化2. 初始假定说明3 •协议冃标说明4 •应用逻辑假定尽管GNY非常有效，但还是存在限制：不包含短期操作者，仅仅按信条处理而不是按 所知，用依靠人解释的理想化的规则。

然而，阻碍GNY普及的更严重的问题是它的复 杂x,y)两个公式级联{x}k 和对称加密和解密{x}k+公共密钥加密和解密{x}k-个人密钥加密和解密#{X}公式x是新的，在运行协议Z前没有被发送过①{x}公式X是可识别的P

U用户鉴别V服务提供者鉴别S证书核查鉴别KK一个关键的加密密钥SK会议密钥rx一个由X生成的随机数表二协议术语3.1. ASK 协议ASK协议［1］首先使用椭圆曲线加密以达到“认证和密钥确认”因为在不同通信端的计 算负担是不对称的，所以这项技术尤其适合于无线通信VtU: Kv+U computes KK={Kv+}Ku・UtV: Ku+V computes KK={Ku+}Kv・ and SK=KK + rvVtU: {CertV, rv}KKU computes SK = KK + rvUtV: (CertU.rv'KKFig. 1. The ASK Protocol所以在移动设备上的计算要求很低椭圆曲线加密的更大的优点是密钥尺寸小与基于 常规公共密钥加密系统的协议相比，减小了带宽要求ASK协议的信息交换如图一所示ASK 协议的前两个步骤，主要是主体交换公共密钥在这个阶段用个人密钥通过加密其它主体的 公共密钥，每个主体可以计算关键的加密密钥KK,即进行了 Diffie・Hellman密钥交换然后 服务提供者V生成随机数w，可以用KK加密來生产会议密钥SK接着V给用户U发一条 信息，包含了随机数w和它的用KK加密的证书。

用户U在收到wZ后，可以算出会议密钥 U也可以通过测试证书，验证Z前收到属于V的公共密钥协议以一条从用户发送给服务提 供者的信息结束，其中包含了用户的证书和由前些时候V生成的随机数这条信息要求实现 用户认证尽管协议明显简单，可是ASK协议的缺点也已经被发现［6］本文中ASK协议的 形式验证表明了 GNY逻辑检测弱点的能力，因此在释放它们进入公共域Z前丿应强调安全协 议的形式验证的重要性32 ASK协议的验证这一节将应用GNY逻辑验证ASK协议321.协议公式化ASK1:U< ・Kv+ASK2: VV »Ku+心+ 、ASK3:UV 小CertV〜〉S|= V,，rv}KKK“+ 、ASK4: V< ・{・CertU~> S |= U,rv}KK3.2.2. 初始设想的规格U 3 Ku-;U 3 Ks+;UI三Ks+ 、 S；U 9 CertU;U |= 0CertV;U |三 SnU |= S => S |= *;V ? Ks+;V|三 S；V a CertV;V |= 0CertU;》U;323•协议目标的规格UaSK;U|三#SK;V?SK;V|三# SK;v |三 #rv；V 1= S S 1= *;U |三V夕SK;crU|三 u > V;V|= U 9 SK;V I三 u <~: > V;U$ #(CertV, rv)V^(CertV,rv)#(CertU, rv)V|三U 〜(CertU, rv)3.2.4.逻辑假设的应用・公理T1推断U

为了继续证明，有以下假定：关键加密密钥KK由Diffie-Hellman密钥交换所建立因 此可以考虑分享预计和主体Z间的机密只有这些主体可以生成会议密钥，因为关键 SK加密密钥是不可缺少的先决条件因此我们能假定V\^U^V也就是说V相信SK适 合分享机密ASK3: U < CertV S\=U <^V*rv }kK- 原理 T1 推断 U < *{* CertV ~〉S\=U t 卩,*口 j>KK・ 因为U mKK ,通过公理T3,可以解密信息和告知信息内容公理T2和P1推断U 拥有每个部分的信息・ 因此，U 3 ryo因为ASK1有U 3 KK ,公理P2推断U 3 SK = KK + rv・ 因为Diffie-Hellman密钥交换依赖丁•底层加密系统，所以GNY逻辑不能驱动SK SKU\^U<^V o为了继续证明，由ASK2,可以假定u^u'^v .也就是U相信SK适 丁•分享机密・ 因此，实现了 U的密钥承认但是U不能建立新密钥・ 因为证书认证签署了 CertV,可以应用公理14,推出U- CertV .通过公理T6,T2和Pl, U可以通过CertV得到V的公共密钥・U相信S。