精编基于SPIN的安全协议形式化验证方法

基于SPIN的安全协议形式化验证方法1引言 随着计算机技术的发展，人类进入了信息时代，信息技术已经渗透到了人们日常生活的方方面面，然而信息在开放的网络环境中传输会遭到各种各样的攻击，如偷听攻击、

基于SPIN的安全协议形式化验证方法 1引言 随着计算机技术的发展，人类进入了信息时代，信息技术已经渗透到了人们 日常生活的方方面面，然而信息在开放的网络环境中传输会遭到各种各样的攻击， 如偷听攻击、截取攻击、伪造攻击、篡改攻击等。这些攻击的存在在不同程度上 损害了网络用户的利益。因此为了确保信息安全，人们设计出了安全协议来保证 通信过程的安全可靠。安全协议是一个分布式算法，它规定了两个或两个以上的 协议主体在一次通信过程中必须要执行的一系列步骤。利用安全协议人们来实现 在开发网络中的安全通信。可以说安全协议是信息安全的基础，其自身的安全问 题已成为安全研究的重要内容。目前，在安全协议验证领域存在多种验证方法如 模拟、形式化等，模拟的方法存在不能100%覆盖的缺陷，而形式化能够达到覆盖 率100%而且具有严密的数学基础，因而越来越受到业内人士的信赖。形式化验证 主要有两种验证方法定理证明和模型检测两种方法。定理证明的基本思想是将安 全协议描述为公理系统，安全协议的安全目标则表示成需要证明的定理，安全协 议是否符合安全目标则对应于公理系统中的目标定理是否成立。定理证明的最大 优势是协议运行期间不会出现状态爆炸的问题。缺点是，对使用者的技术要求较 高，需专业人士才能驾驭，而且自动化程度不高，需要人工干预。模型检测的基 本思想是，把安全协议看成一个分布式系统，单个协议实体涉及的协议执行部分 为局部状态，所有局部状态构成了分布式系统的全局状态。在安全协议的全局状 态上定义安全属性，安全协议是否满足安全属性等价于系统可达的每个全局状态 上安全属性都能够得到满足。模型检测可实现全自动的执行，人的干预较少操作 简单易实行，但模型检测会出现状态空间爆炸的情况，这种情况制约了模型检测 技术的发展。SPIN这种模型检测工具利用on-the-fly技术可以有效的缓解状态 空间爆炸问题，SPIN模型检测工具的基本思想是将协议表示成一自动机的形式， 并且将待验证属性表示为另一自动机，然后求这两个自动机的同步积。通过遍历 求同步积后产生的新的状态机的整个状态空间，检查协议是否满足我们期望的性 质描述。如果不满足则返回错误并提供导致错误的状态迁移路径，我们将通过错 误路径来定位错误。本文详细介绍了模型检测工具SPIN的工作原理，并给出了 1