基于Spi演算的密码协议自动化分析技术研究

◆江 涛



基于Spi演算的密码协议自动化分析技术研究

◆江 涛

(国务院法制办公室秘书行政司 北京 100000)

密码协议可以维护网络通信和其中的各个分布式系统的安全，为了让恶意攻击者无法获取机密信息或者借安全漏洞进行不公平认证，需要对协议所运行的环境安全性进行提升和技术改进。而通过以前的静态分析测试和人工手动验证，对密码协议的所存在的威胁和漏洞检测不够全面，由此其重要性得以体现。根据这一研究模块，本文将对其演算基础以及实现自动化的分析方式，还有Spi演算方式在密码协议中对其秘密性的验证和认证性的分析演算做基本阐述。

Spi演算；密码协议；自动化；分析技术

0 引言

密码协议是为了针对预防攻击者而以密码体制为基础来建立相互传递信息的协议，运用对密钥进行分配、对身份进行认证等技术，用以加强协议的正确性、安全性和抗变换性这三大要点。可往往在逻辑关系千变万化，会因为当时对协议所运行环境的了解不足而致使遗漏设计细节。如何完善密码协议成为了人们的思考焦点，而在Spi演算基础上的密码协议的自动化分析技术应运而生，并受到了广泛关注。

1 基于Spi演算密码协议的形式化分析

在形式化分析种存在一些不同的验证方法，例如在知识和信念方面实现推理的模态逻辑方法，以定理证明为基础的方法和以进程演算为基础的方法。1997年Abadi和Gordon建立的Sp i演算[1]，除了能够对进程信息、间值和通道名称进行同步传递，还可以用其简单语法和丰富的描述能力，为密码协议进一步提供密码操作原语，在运用Dolev-Yao模型的基础上，面对密码协议所执行的每一个进程分析其与攻击者所执行进程相交替的可能，用以验证其各项性质。

在Spi演算的基础上，我们需要运用相应的操作语义来对已经建模的密码协议验证其所满足的安全属性，通常会用的有程序分析技术、模型检测技术和互模拟等价技术这三种。

首先要说的是模型检测技术，它需要密码协议被实现，也就是被转换成有限的状态转换图，以此同时密码协议所满足的性质也需要被规范，通常是将性质用某种时态逻辑来约束，而模型检测技术也就是通过确定实现的状态转换图是否和被规范的密码协议性质相符，用这个来验证有限状态系统的技术类型。

其次是程序分析技术，其被分为静态分析和动态分析，在现在的发展情况中静态分析要比动态分析更完善，其已经具备自动分析系统性质的方法和工具，动态分析虽然可以有效的保护密码协议执行过程中可能出现的分支，并且具有验证空间小、实现效率高的优势，但是目前还没有合适的自动化验证工具出现。因此，由于动态分析的先天不足，程序分析技术也主要可以从静态分析方面被分为数据流分析和控制流分析[2]。

最后，互模拟关系作为进程演算领域的核心概念之一，使互模拟等价技术的成长促发了进程演算被广为运用在程序的验证和并发系统建模，而目前，互模拟验证技术也主要是以Spi演算为基础的。所以其在利用测试等价关系的形式化分析过程中的应用基本被分为四个方面：

（1）协议整体和协议参与主体要用Spi演算转换成具体描述来进行形式化展示。

（2）在满足密码协议安全目标的基础上运用Spi演算对其规范形式进行判断。

（3）可以用反应关系对被任意第三封闭进程R和Barbβ测试的规范形式进行约简[2]。

（4）对密码协议和其规范协议满足的测试等价关系实施验证，以确认满足的具体安全协议的要求。

2 基于Spi演算的密码协议自动分析器的实现

2.1分析器工作原理

在运用逻辑方法在现有条件下，对扩展Spi演算语法和Spi演算在密码协议安全属性定义的基础上实现的自动分析器，其化简后的工作原理如图1：

图1分析器工作原理图

该分析器基于被广泛采用的Dolev-Yao模型，是根据密码协议自动默认在攻击者是在运行环境中的，而攻击者在环境中可以获取密码协议在信道上拥有的所有信息，并且可产生自己的消息和伪装成一般的用户发送消息。对于密码协议的加密和解密操作，只有拥有相应解密密钥的用户才可以将加密信息解密。

在密码协议自动化分析器中对密码协议及其协议参与主体的形式化描述、用户对协议运行的设置条件还有验证所要达到的安全目标是用户需要输入的三个部分，也就是分析器所需的输入语法。而自动翻译模块是对用户所输入的文件和语句部分进行解析和处理，逻辑推导模块则是被用以判断每位用户提供的信息是否可以从相关的事实和规则中导出。下面根据上述内容对基于Spi演算下的密码协议自动化分析器的分析过程主要步骤进行简要介绍：

第一，将之前被验证的协议整体和协议参与主体受Spi演算的形式化描述输入到系统中，根据系统参数和协议所运行的环境安排设定，主要是针对攻击者属性、信道属性还有密钥威胁等来确定验证目标。第二，分析器会根据用户的环境参数自动验证内容，将协议的形式化描述转为特定的语言，例如霍恩字句等，对协议进行抽象描述。第三，分析器在进行一番逻辑推理算法之后，它会在已有的事实和规则的基础上自动搜索既定的验证目标，根据最后的具体情况来分别处理，如果在目前环境下协议不存在潜在的漏洞，则对协议分析给出正确的结果，反之，则向协议分析提供导致攻击或者漏洞产生的路径。

2.2密码协议分析相关内容

在以事实和规则为基础的逻辑程序设计技术中，事实既是逻辑推理的前提假设，又是规则的依据。在分析器中真正完整的协议分析首先需要攻击者初始知识以及符合其条件的事实，其次是对攻击者计算能力的规则还有对协议本身的规则描述这两个部分。

2.3分析器对密码协议安全属性的分析

首先是密码协议秘密性验证的问题，要对事实和规则定义的基础上证明基于Spi演算的类型系统和分析器在安全属性的分析方法方面的一致性，然后再由此去根据对应事件进程的定义去解决模型中对单射一致性和非单射一致性的证明问题。而在分析密码协议安全属性的方法上除了逻辑方法，其实还有密码学方法，其分析结果比起逻辑方法的可信度要更高一些，而逻辑方法的优势在于，如果是在加密算法完善的情况下，分析效率比密码学更高且直接简洁，则更加有利于自动化分析技术的进行[3]。

另外，在现有的逻辑程序设计技术基础上引进新的认证逻辑系统，对分析器的分析能力其实是一种很有效的完善方式，通过罗列一些常用的定理并引进多种符号和公式和增加新的消息源公理以及改进原本的消息生成、身份认证、消息接收公理，令基于Spi演算的密码协议的自动化分析器能够对更多类型的密码协议进行严谨的分析判断。而且这种方式能够更好的让公钥密码体制在密码协议中发挥效用，例如能够证明一些协议的安全性、可以找出更多协议的安全漏洞以及让分析器不止适用于单一类型的协议。

这些都为我们后期针对密码协议的安全漏洞提出并进行相关的改进方案，保证用户的身份不被泄露的网络安全性问题提供了保障[4]。密码协议的自动化技术发展现在来说尚未达到一个较为平稳的状态，频现的网络安全性问题的解决需要不断地将理论融合于实践中去，并针对其在整个密码协议中的应用优势和缺点进行分析和扬长避短。逻辑方法拥有的优势是采用进程演算的分析效率，短处却是现有的简单逻辑被实际应用后的分析结果可信度有待加强。如何完善语句，如何在加强安全性的同时提高分析效率等等一系列的问题都有待我们进一步思考。现今对基于Spi演算的密码协议自动化分析器还只是初步的对单一逻辑进程的演算，今后的研究中则需要进一步深入了解复合逻辑，以实现同时验证多个安全目标的复合密码协议的安全性。

3 结束语

与之前所研究的密码协议所不同的是，其对密码协议的两项属性，即认证性和秘密性进行分析，首先在信道上输出的信息可以作为秘密性的依据，其次事件发生的先后顺序和次数又可以用来验证协议是否满足密码协议的认证性，并利用Spi演算的扩展语法构造类型系统与密码协议进行匹配，假设其中的进程被密码协议佐证出是无误的，则认定该进程不存在泄露秘密级别数据的可能性，最终在以上原理基础上实现密码协议的自动分析技术。通过详细的Spi演算过程对各主体间的精准把握，恰好可以提升密码协议的安全性。

[1]杨芳.基于模型检测的安全协议自动验证方法研究[D].湖南大学，2015.

[2]郑清雄.基于Spi演算的安全协议形式化分析[D].上海交通大学，2010.

[3]程华清.密码协议安全性分析的逻辑方法及其哲学意蕴[D].华东师范大学，2015.

[4]袁亚飞.逻辑化方法的改进及若干密码协议安全性分析[D].中国人民解放军信息工程大学，2005.