形式化1|概述

1. 什么是形式化

20世纪70年代末80年代初，Needham和Sehrieder将形式化方法应用于安全协议分析。Dolev和Yao在此领域开始了真正的实际工作，并且Dolev，Even和Karp为验证一些有限种类的协议安全性开发了一套算法。直到20世纪90年代初，形式化方法在密码协议中的应用才变得非常流行。在密码协议中运用形式化的分析技术时，研究者发现了以前未能发现的安全缺陷，随之许多安全协议分析工具开发出来了，如Miller的询问器、Meadow的NRL协议分析仪以及Longley-Rigby工具等等。

一句话概括，形式化验证是用形式化的数学方法，来证明或者反证系统满足需求规范。

2. 为什么要用形式化

安全协议的形式化分析需要对外部环境进行评价并在此基础上模拟运行，当网络中存在的攻击者时，要提出具体化的模型。假设安全协议外部环境中包括消息的发送方，消息的接受方和协议的攻击方，还包括各种规则，参与协议的各方使用规则来参与其中。攻击者可能会进行级联、拆分、加密和解密消息（根据DY模型）。具体的表现有以下几种形式：

猜测协议中传递的消息；
转发消息到其指定的接收者处；
使消息到达目的地的时间推迟；

因此，确保安全协议的安全运行十分重要，因为在实际运行过程中，安全协议产生缺陷的原因多种多样，且对安全协议的攻击方式变化无穷，所以安全协议的安全性是一个很难解决的问题，许多广泛应用的安全协议后来都被发现存在缺陷。

最初，人们是基于经验和单纯的软件测试采用攻击检验的方法来分析协议安全性。但由于安全协议运行的外部环境十分复杂多变，对安全协议新的攻击方法越来越多。所以，仅用人工的方法很难识别产生的错误。因此，必须采用形式化的方法和攻击来对密码协议的安全性进行分析。形式化分析就是采用数学或逻辑模型，通过有效的程序来分析系统及其条件，以此来确定一种在系统满足条件情况下所得的证明是否正确的数学理论和方法。

因为形式化的数学理论基础，所以其能更精确规范密码协议的安全特性，且没有歧义。因此采用形式化方法分析密码协议，验证密码协议的正确性。形式化方法包含的内容有：

安全协议分析的形式化模型；
用规范的语言表述密码协议的安全特性；
用形式化语义来解释密码协议及其安全特性；
通过验证技术来确定密码协议是否具备所需的安全特性。

3. 形式化方法构成

《形式化方法导论》，张广泉

形式化方法主要由三方面构成，包括对系统进行描述的系统建模，定义系统需要满足的属性的形式规约和证明系统模型满足相应属性的形式验证。

  flowchart LR
    A(系统建模) -->B(形式规约)
    B --> C(形式验证)

3.1 系统建模

系统建模是对所需要进行验证的系统进行抽象描述的过程。

计算机系统最初是串行的，它具有封闭性、顺序性、可再现性的特征，可以通过输入输出关系来对系统进行描绘。而随着具有不确定性和并发性的系统出现，之前的方法就不要再适用。

合理的抽象模型可以帮助人们更好地抓住系统的本质并加以理解，方便之后对系统进行规约和验证。因此，系统模型的抽象粒度很关键，模型过于抽象不能体现其安全属性，过于具体又可能产生冗余。

目前有许多方法来描述并发系统的形式化建模方法。

Petri网

Petri网是一种既能用来分析系统性质，又能运用图形直观地描绘系统结构的工具。

各种状态迁移系统

由于并发系统的不确定性，为了能更好地表示并发，这个模型的各个迁移过程之间采用交错执行，并且这种交错执行的顺序也具有不确定性。

比较著名的有基于进程演算的CSP模型和CCS模型等。

自动机（状态机）

自动机也是一种常见的抽象模型，其中有限自动机是这一领域中的基础。有限自动机通常也被称作有限状态机，它在软件设计中的应用非常广泛，主要用来说明一个对象在它的生命周期内所能经历的一系列状态以及它能够对外界的事件产生的反应。状态图是状态机最为常见的描绘方式。

3.2 形式规约

在软件开发的过程中，第一步就是确定需求，并且需求需要是清晰的、明确的、没有歧义的。进行软件的实现必须是按照需求来完成的，判断开发得到的系统是否合适，首先就是需要验证它是否满足一开始所确定的需求。形式规约就是使用精确的形式化语言对系统需要满足的属性进行准确定义的过程。

形式规约同样也存在从面向串行系统到面向并发系统的发展历程。在串行程序中，从系统的初始状态到系统最终状态的过程是相对固定的，采用 Floyd 前后断言法、一阶逻辑等方法来进行形式规约在当时是比较好的选择。

对于并发系统而言，它存在着不确定性，其状态的改变更为复杂，时序逻辑能够更好地对它进行规约。除了包含常见的与或非等表现逻辑关系的联结词外，时序逻辑还包含了一些用来表示时间上的关系的时序算子。并发系统最常见的属性有表示坏的事情永远不会发生的安全性和表示好的事情最终会发生的活性，这些属性中出现的“永不”和“最终”这种与时间存在关系的表述方法都可以很好地用时序逻辑来进行表达。

3.3 形式验证

形式验证就是检验根据系统所建立的模型 $S$ 是否满足针对这个系统所提出的需求 $\phi$ ，即验证 $S \mid=\phi$ 。

形式验证的方法主要分为根据逻辑公理进行推理的演绎类方法和进行穷尽搜索的模型检测类方法。

  graph LR
    A(形式化验证) -->B(演绎类)
    A -->MC
    subgraph 方法
    B
    MC(模型检测)
    end

    subgraph 适用范围
    YX(有限状态并发系统)
    JH(几乎所有系统)
    end
    
    B -->YX
    MC(模型检测) -->JH
    
    subgraph 优点
    GD(高度抽象表达能力强大)
    YZ(验证自动进行)
    end
    
    YX-->GD
    JH-->YZ
    
    subgraph 缺点
    XY(需要验证者有良好的数学训练和经验)
    BZ(需要解决状态爆炸问题)
    end
    
    GD-->XY
    YZ-->BZ

演绎类

演绎类的方法将需要验证的性质看成是一个数学定理来进行证明，既可以验证状态有限的系统，也可以通过归纳的方法来应对状态数量庞大甚至是无限状态空间的情况。但是这类方法难以实现完全自动化，当需要验证的系统比较复杂时，这类方法就显得效率低下了。而且人工验证除了费时费力以外，还存在着使用方法是否恰当的疑问，当使用的方法不当时可能导致无法正确进行推理。

模型检测

模型检测类方法则是会对状态空间内所有可能的路径进行搜索，来判断系统所有可能的行为和预期的属性是否都能够达成一致，如果一致的话则返回正确的结论，如果不一致则返回一个反例。这类方法由于它的自动化程度高，目前被运用于许多领域，比如安全协议的研究和软硬件系统设计的验证。然而，正是因为传统模型检测的方法会覆盖到所有可能的状态，所以由于数量太多而产生的状态空间爆炸的问题一直是这类方法使用过程中容易遇到的关键性问题。研究人员也针对这个问题提出了一些解决方案，比如使用二叉决策图来表示状态空间以此增加对可验证状态数量的支持的符号模型检测、限定检验范围的有界模型检测等方法，通过这些方法可以简化整体的状态空间或者有针对性地检测部分状态空间。

4. 攻击者模型

4.1 Dolve-Yao模型

DOLEV D, YAO A. On the security of public key protocols[J]. IEEE Transactions on information theory, 1983, 29(2): 198-208.

这是如今最常见的攻击者模型，它假设攻击者不具备破解密码算法的能力。如果攻击者想要获得加密的秘密，他必须使用正确的密钥来对它进行解密，同时假设在初始阶段，攻击者并不知道任何合法参与者所拥有的秘密消息。并且攻击者还拥有以下能力：

攻击者可以窃听网络消息，在不被发现的情况下阻止并截取所有网络中的消息；
攻击者可以储存自己获得的或者创造的消息；
攻击者可以伪造消息，发送消息；
攻击者可以作为合法的协议参与者参与协议。

也就是说，攻击者可以拥有控制整个网络的能力。

目前大多数的形式化分析工具都是基于 Dolve-Yao 模型设计的。

4.2 eCK模型

SCHMIDT B. Formal analysis of key exchange protocols and physical protocols[J]. Analytical Chemistry, 2013, 64(13): 665A-671A.

倪亮, 陈恭亮, 李建华. eCK 模型的安全性分析[J]. 山东大学学报:理学版, 2013

eCK 模型是针对密钥协商过程被提出的，它提供了一个比 Dolve-Yao 模型更强大的攻击模型。在 eCK 模型中，合法参与者和攻击者被描述为概率多项式时间图灵机。

在计算复杂理论内，机率图灵机是一个非决定型图灵机，在每个转折点根据某种概率分布随机选择某种可行的转变

除了拥有 Dolve-Yao 模型下的能力外，敌手在与挑战者进行游戏时，还被允许拥有以下能力：

攻击者可以获取参与者的长期密钥；
攻击者可以获取会话中参与者的临时秘密；
攻击者可以获取会话中计算得到的会话密钥。

在一个双方的密钥协商中，一般涉及到双方的长期密钥和临时秘密这四块秘密信息，只要每个参与者仍有至少一个秘密未被泄露，则称这个密钥协商过程在 eCK 模型下是安全的。而 eCK 模型下的安全应该满足以下性质：

当敌手未获取到参与协议的合法实体的长期私钥时，它无法仿冒这个实体的身份。
协议进行一次运行则只会产生唯一一个独立的会话密钥。即使敌手掌握了在其它会话中产生的密钥，也无法得知当前会话产生的密钥。
即使所有代理的长期私钥都被敌手获知，至少还能保证前几次会话的密钥是安全的。
当敌手得知了某个合法参与者的长期私钥，它便可以假冒这个参与者和其它合法参与者进行通信。
当协商得到会话密钥后，实体并不会错认与之生成会话密钥的对象。
即使敌手获取到会话中传递的临时秘密，它仍然无法得到会话时使用的密钥，也无法得到其它会话中使用的密钥。

5. 常见形式化方法及工具

形式化工具	模型	证明	安全属性	分析能力
形式化工具	模型	证明	安全属性	无限状态空间	代数运算	自动化	可视化
BAN逻辑	逻辑公式	基于推理的信念	认证性
Paulson归纳法	“trace”集合	归纳法	机密性、认证性	√		√
FDR	CSP	状态机	机密性、认证性			√
AVISPA	HLPSL	状态机	机密性、认证性	√	exp，xor（作为函数）	√	消息序列图和攻击图
Scyther	线性角色脚本	状态机	机密性、认证性	√		√	攻击图
ProVerif	应用PI演算	Horn子句	机密性、认证性	√		√	攻击图
Tamarin	多重集重写规则	状态机	可执行性、存活性、弱一致性、非单射一致性、单射一致性、机密性、前向安全性	√	结合律、交换律、 DH 指数、 xor、双线性对等	√
UPPAAL	时间自动机	状态机	状态可达性			√	消息序列图和攻击图
SPIN	Promela	状态机	状态可达性			√	消息序列图和攻击图

基于逻辑的形式化方法最典型的例子是BAN逻辑。它关注协议中可信参与者的信念，通过推导可信参与者在协议执行过程中能够正确执行协议的信念来分析协议。但是它仅能用来进行认证性上的验证，也不适用与太过复杂的方案，并且由于其语义过于简单不够完善，并不能全面地检查到问题。但是正因为它是最简单的逻辑证明方法，即便没有自动化和可视化的工具存在也足够方便使用，尽管它的局限性是众所周知的，而且许多其他基于逻辑的方法如 GNY、SVO被开发出来弥补它的缺点，但人们仍然喜欢选择它作为在许多工作中分析安全协议的形式化方法。

GONG L, NEEDHAM R M, YAHALOM R. Reasoning about Belief in Cryptographic Protocols[C]//Proceedings of IEEE Symposium on Security and Privacy. 1990: 234-248.

Syverson P F, Van Oorschot P C. On unifying some cryptographic protocol logics[C]//Proceedings of 1994 IEEE Computer Society Symposium on Research in Security and Privacy. IEEE, 1994: 14-28.

Paulson归纳法同样是基于逻辑的方法，但是它进行了无限状态空间方面的扩展，可以用来分析一些更加复杂的问题。不过因此它的证明过程也会显得更加复杂，虽然可以使用 Isabelle 定理证明器实现部分自动化，但是自动化的程度并不高，在处理复杂问题的时候依然会带来不小的开销。

PAULSON L C. The inductive approach to verifying cryptographic protocols[J]. Journal of computer security, 1998, 6(1-2): 85-128.

CSP 模型是比较早出现的用来描述并发系统中通过消息交换实现的交互通信实体行为的建模方式，它属于进程演算，但是它的自动化工具失败分歧细化（Failure Divergence Refinement，FDR）则采用了基于操作语义的状态搜索思想。不过虽然它能够实现高度的自动化但是却缺少能够直观体现结果的可视化功能。

PROCESSES C S. Communicating sequential processes[J]. Communications of the Acm, 1978, 21(1): 666-677.

应用PI演算也是进程演算的一种，它是PI演算的扩展，可以用直观的进程语法详细描述参与者（包括它们的交互）的行为。它可以用于无限数量的会话和无限的消息空间，不存在状态空间爆炸的问题，但是它的证明过程非常复杂，如果使用它进行人工地推导，将是一项非常耗时和费力的工作。所幸它可以使用基于 Dolve-Yao 模型的 ProVerif 工具实现对认证性和机密性的自动化分析。同时它还具有可视化的功能，当发现存在攻击时它可以生成相应的路径。

AVISPA 是一种高度自动化的验证工具，它提供了一种模块化的、表现力强的、基于角色的形式化语言高级协议规范语言（High Level Protocol Specification Language，HLPSL）来描述协议和它的安全特性，还整合了四种不同的分析终端来进行多种自动化分析。这个工具可以根据输入的模型看到模拟出来的消息序列图。如果分析的结果是不安全的，分析终端会输出相应的攻击轨迹，用户可以依据给出的反例找到协议的安全漏洞，并采用相应措施进行改进。

ARMANDO A, BASIN D, BOICHUT Y, et al. The AVISPA tool for the automated validation of internet security protocols and applications[C]//Proceedings of International conference on computer aided verification. Springer, Berlin, Heidelberg, 2005: 281-285.

UPPAAL 和 SPIN 是比较经典的采用模型检测方法的工具。UPPAAL 使用时间自动机作为输入。SPIN 用 Promela 语言将需要验证的系统描述成有限状态机，语法是基于进程的描述的，结构和C语言比较类似。它们都可以使用线性时序逻辑LTL对安全目标进行规约，然后通过对状态可达性的检查来分析安全目标是否可以实现，比如是否存在死锁等。然而正如本文之前所介绍的模型检测算法，这类工具最大的问题就在于状态空间爆炸，当所需要分析的系统太过于复杂导致需要进行搜索的状态空间太过于庞大时，往往不能得到很好的结果。

Scyther以及在它的基础上进行了改进的 Tamarin虽然同样采用了模型检测的思想，但是它们考虑了对状态进行逆向搜索的方法，根据需要得到的状态推导它之前的状态，能够排除掉无关的状态以此缩减状态空间，解决状态空间爆炸的问题。同时它们不仅能够实现 Dolve-Yao 模型下的检验，还可以进行 eCK 模型下的安全性分析。不过 Tamarin 还可以进行一些 DH、双线性对、Xor 等方面的运算，可以实现更加复杂的模型。

CREMERS C J F. Scyther[J]. Proc Dimacs Workshop, 2011, 6(1): 324–337.

MEIER S, SCHMIDT B, CREMERS C, et al. The TAMARIN prover for the symbolic analysis of security protocols[C]//Proceedings of International Conference on Computer AidedVerification. Springer, Berlin, Heidelberg, 2013: 696-701.