文档介绍：肅密码协议的形式验证蚅摘要:膁无线通信在设计合适的安全协议方面,设置了一定数量的限制。导致了着重于无线应用的新协议诞生。其中的一些协议缺点明显。形式验证是是增加安全协议的信赖所必不可少的部分。本文将讨论形式验证的不同方法。以一个针对无线通信的安全协议,运用一个逻辑模型来表示的形式确认作为例子。b5E2RGbCAP肈关键词:膅安全协议,协议确认,确认逻辑,认证,移动安全肆绪论蕿无线通信为安全协议的设计设置了一些限制。用于这类通信的移动设备,通常只有限的计算和储存能力。况且,用户和网络之间的带宽通常是限定的;因此通过无线电接口发送的信息必须保持最小值。由于这些约束,以及其它需要注意的方面如匿名,所以常规的协议不适于无线通信。导致一些着重于无线应用的新协议诞生。包括ASK协议[1],ASPeCT协议[2]和Wong-Chan协议[3]。一些其他的候选的认证协议如最近Park[4]和Yietal提出的协议,已经被发现了很多缺点[6][7]。p1EanqFDPw膀已经发布的协议所存在的缺点,表明了源协议的设计是非常复杂和容易出错的过程。已经证明非正式技术在协议验证方面的不足。正式的验证技术提供了一种提高协议安全的手段。这种技术强制执行了最初设想的明确规范以及协议的目标,因此协议范围的定义。而且,由于这个方法的本质,以系统性的方式发现协议的弱点。但是检测弱点的能力与所用技术的限制相关的。DXDiTa9E3d芅本文讨论形式验证的不同方法。大概的方法包括状态机,代数项重写技术,定理证明技术和逻辑模型。而且,通过逻辑基础技术证明形式确认的进程是一项安全的协议。本文着重于形式确认的优点,并鼓励推广这项技术。。一些技术可以用来分析协议的安全性。包括状态机,代数项重写技术,定理证明技术和逻辑模型。[8]的方法分析协议。运用这项协议,系统的全局状态由每一个过渡表示。然后分析每一个全局状态是否发现有状态协议上的错误导致攻击者获得了访问保密信息权限。一个详细的研究证实了所有可达到状态都是安全的。可达性分析适于判别一个协议是否匹配其规格,但并不保证被主动袭击时动安全性。这项其它的一系列限制是需要通过极端的假定来保持较小的状态空间[9]。jLBHrnAILg蚃一些状态机并没有明确针对安全协议分析的设计。这些工具[10]的一个问题在于不能辨别安全领域内细微的缺陷,如应对攻击。特别针对协议分析设计的工具可以应对攻击,但会受限于所有状态机的影响。基于纯状态空间研究的方法可以判别一个协议是否包含了一个已经定义的缺陷,却不太可能发现协议中不明种类的缺陷。由于有这些缺陷的存在,所以即便基于状态机的技术可以与其他技术高效率地结合,却是永远也不能取代其他的验证技术。状态机的研究效率低下,经常不确定<由于空间太大而不能分析)和不能找出新的错误;因此协议设计人员很少使用。。但是状态机技术由不安全的状态开始,试图表明不存在从原始状态通向不安全状态的路径。与之相比,代数项重写技术适于初始的状态规格。努力证明不能到达不安全状态。尽管代数项重写技术与所有的方法有关,由于可以发现新协议的缺点,所以还是比常规状态机有所发展。LDAYtRyKfE蒅但是这项技术始终受一系列的限制。一个问题是只考虑已经被系统描述的行为。合理地使用并没有充分代表入侵者发出的信息。可以考虑窃听与回应攻击,但当入侵者采用新信息时,这项技术便失败了。代数项重写的另一个问题就是复杂,这减轻了它对程序设计人员的吸引。。针对原理证明用来协助数学命题的证明的工具已经被开发出来。在用户知道每一个阶段的证明下,这些程序允许一步一步地进入和证明数学陈述。因为一个安全协议可以被精确指定,精确无误的公式可以被定义,给定协议的在设定情景是安全的状态能用精确的数学项解释。这种陈述能够进入一个原理证明而证明的研究也可以进行。dvzfvkwMI1蒇然而,原理的证明方法在展示协议的正确性方面比找出协议被攻击的漏洞方面做得好。况且,一个原理证明要求用户通过证明找出正确合理直观可行的路径。因此源程序的验证有可能由于操作者缺乏经验而失败。尽管有诸多限制,原理证明还是对协议设计人员有利的,尤其是与其他技术融合的时候。[11][12]。逻辑技术涉及演绎推理的进程,在其中所希望的协议目标是通过对假定应用一些公理和推导规则来演绎,以及通知协议的交换[12]。接下来的一节以GNY