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