一种基于Isabelle/HOL 的安全通信协议验证方法

夏 锐，钱振江，2，刘 苇

（1.苏州大学 计算机科学与技术学院，江苏 苏州 215000；2.常熟理工学院 计算机科学与工程学院，江苏 常熟 215500；3.国网电力科学研究院，南京 211000）

0 概述

随着信息技术的不断发展，数字化信息借助互联网络进行广泛传播，信息安全逐步成为公众关注的焦点，而通信协议对于确保信息安全起着至关重要的作用。通信双方在进行信息交互时会遵守事先约定的通信协议，但这并不能保证信息交互过程的绝对安全，很多重要信息仍会面临被盗取的风险，并且通信协议本身可能就存在某些安全漏洞，因此通信协议的安全性分析技术应运而生。

安全通信协议的形式化分析是信息安全领域的重要研究方向，根据技术特点可分为定理证明和模型检测两类。定理证明是一项以数学为基础的技术，主要是在逻辑层面验证程序是否正确［1］。在形式化验证研究领域，定理的机械证明作为形式化验证方式，主要通过人工方式和验证工具进行交互对数学定理进行半自动的推理和证明，进而在逻辑关系上对定理的正确性做出判断［2］。定理证明方法的工作重点在于对安全通信协议中出现的实体对象进行形式化表示，将实体抽象成数据对象并使用形式化操作语义描述实体行为［3］。对象建模和行为抽象是验证工作的核心步骤，根据期望性质建立定理并采用形式化策略证明其正确性是验证工作的关键。模型检测方法的优点是检测过程完全自动化，但只能处理有限状态的系统，在应用过程中需要对检测范围加以限制［4］，并且模型检测方法可直观地发现通信协议的安全漏洞，然而其最大的弊端在于即使没有发现通信协议漏洞，也不能确保通信协议绝对安全。为更全面地对通信协议进行逻辑上的安全性分析，本文使用Isabelle/HOL 定理证明辅助工具［5］对D_protocol 混合密钥加密协议建立通信代理和消息序列的形式化模型，并采用规则归纳方式验证该通信协议的安全性。

1 相关工作

形式化验证通信协议的主要任务是对通信协议中涉及的实体对象、消息、动作、知识状态和信任关系等进行逻辑抽象［6］。近年来，已有很多专家和学者对通信协议安全性进行验证研究并取得了重要成果。文献［7］采用以RDP 协议为基础的仿真技术还原了RDP 协议的数据信息，研究结果表明RDP 协议存在中间人攻击的漏洞，因此作者在此基础上利用绑定IP 地址和修改端口号的方式对其进行改进。文献［8］基于二重特征值的思想，提出一种三方密钥交换协议，其既可抵御中间人攻击，又可进行用户合法性认证。该协议通过生成新的会话密钥以避免旧密钥多次使用的安全隐患，并通过对比分析的方式证明该协议具有良好的安全性和高效性。

传统匿名认证协议存在匿名不可控和通信时延大等问题。文献［9］提出的基于异构无线网络的可控漫游认证协议解决了以上问题，该协议仅需一轮消息交互即可完成对移动终端的身份合法性认证，并借助CK 安全模型验证了该协议的可靠性。文献［10］在分析Li 匿名协议的安全缺陷基础上，提出一种基于共享密钥的轻量级匿名认证方案，并通过安全分析和仿真测试对方案可靠性进行验证，结果表明其可抵御时间关联等攻击，且具有较小的计算量和存储开销。文献［11］从理论分析角度研究TCP/NC 协议的吞吐量模型，模型仿真和理论分析结果均表明网络编码可有效提升传统TCP 协议的安全性能。文献［12］提出一种抵御中间人攻击的可信网络连接协议S-TNC，在生成协商密钥的基础上导出会话密钥实现认证端和通信端的绑定。分析结果表明，S-TNC 协议相比现有协议未增加新的实体和证书，并且具有较高的安全性。

传统对称密钥管理方案存在存储空间占用大、安全性低等问题。文献［13］提出基于对称和非对称密码体制的密钥管理方案，当该方案应用于无线传感器网络时，使用公开的临时主密钥对节点公钥进行身份认证，而节点间信息交互使用的成对密钥是基于非对称密码技术建立。实验结果表明，该方案较好地解决了传感器节点的计算限制问题，但作者未对其可靠性证明展开进一步研究。文献［14］提出的密钥生成（SKG）协议利用对称的临时密钥认证网络中的节点，而实际的会话密钥使用非对称密码技术建立。仿真结果表明，SKG 协议虽然提高了网络吞吐量并且降低了密钥分配功耗，但该协议缺少安全性证明。文献［15］提出一种新的可验证多秘密共享（Verifiable Multi-Secret Sharing，VMSS）方案，该方案以椭圆曲线加密系统为基础，在缩短密钥长度的情况下保证了协议具有良好的抗攻击性，最终通过建立数学定理验证了该方案的正确性。文献［16］证明了双因素身份认证方案存在去同步攻击问题，并且其容易受到特权内幕攻击和已知的密钥攻击。为解决以上问题，WANG 等人提出一个具有可证安全性的增强方案，该方案在没有增加额外计算成本的情况下具有较高的安全性和隐私性。文献［17］提出一种双因素认证方案的评估框架，该框架由12 条标准集和1 个对手模型组成，可及时发现服务器信息泄露并阻止离线猜测问题的发生。

现有研究表明：由于静态共享密钥和短暂临时密钥的存在，因此导致YAK 公钥身份认证协议存在一定的安全隐患，且不能抵御所有已知攻击。文献［18］通过加强验证机制和实体身份认证等对YAK 协议进行改进，并且在Diffie-Hellman 随机预言假设下验证了YAK 协议的安全性。文献［19］以现有EuroRadio 安全通信协议为基础，设计并实现了一套适用于无线调车机车信号和监控系统（STP）的安全通信协议，采用ASK-CTL 时序逻辑对协议进行形式化验证，结果表明该协议在一定的信道干扰条件下仍可实现功能安全。为更好地研究第二代内壳协议（SSHV2）的安全性，文献［20］采用Blanchet 演算方式对协议流程进行分析，并借助CryptoVerif 建模工具模拟协议执行过程，验证结果表明该协议可实现服务端对客户端的认证，并且具有较高的安全性。

2 通信协议

2.1 协议简介

密钥加密算法包括对称加密算法和非对称加密算法［21］两类。对称加密算法是一种传统的密码加密算法，主要分为加密和解密密钥相同及通过算法从解密密钥中计算得到加密密钥两种类型。在通常情况下，对称算法中加密和解密过程使用相同的密钥，因此该算法也被称为单密钥算法。对称密钥算法要求通信双方在进行安全通信前商定一个密钥，该密钥的保密性直接决定通信过程是否安全。如果泄露密钥，则恶意攻击者就能对消息进行加密或解密，甚至可以对原始消息进行篡改以欺骗其他用户。因此，在对称密钥体制下，为保证通信过程安全可靠，密钥必须严格保密。相对非对称加密过程而言，对称加密算法的密钥长度较短，数据计算量较小，加密速度较快。然而，不同用户之间需要使用特定的密钥进行消息处理，由此导致密钥数量大、不易管理的问题。非对称加密算法采用公钥加密和私钥解密的技术，其中，公钥对协议网络中其他用户公开，私钥仅由用户保管，在非对称加密过程中由于公钥通常复杂度较高，因此在消息加密和解密时计算量较大。非对称加密算法基于公钥加密和私钥解密的特点，适用于用户间身份认证及无事先约定的秘密通信等场景。本文基于混合密钥思想构造D_protocol 协议，通信双方各有公开密钥（Pubkey）和私有密钥（Prikey）两个密钥。除此之外，D_protocol 协议还包括一条双方代理共享的临时密钥Temkey。

1）公开密钥：所有人可知，用于对明文消息的加密操作。

2）私有密钥：密钥持有者可知，用于对收到的加密消息进行解密操作。

3）临时私有密钥：通信代理的一方产生该密钥并发送给另一方，仅由双方代理共享，用于消息加密和解密操作。

为确保消息的实时性，避免出现由多条旧消息组成的虚假消息的现象，D_protocol协议中将引入一次性随机数的概念，在随机数的字节长度足够长的情况下，特定的随机值在一次通信过程中连续出现的概率可近似为0。消息包含一组新生成的随机数来说明其不是重复发送的过时消息，随机数作为确保消息实时性的重要信息，需要被加密存放在消息体中。

2.2 协议内容

D_protocol 协议使用公钥加密和私钥解密技术，执行过程具体为：在建立通信前，需要使用非对称密钥加密手段确定通信双方代理的身份，而在消息交互过程中采用临时密钥加密方式，其运行流程相对简单且不涉及可信第三方。以具体的通信过程为例，如D_protocol 协议用户Tom 希望与用户Dick 建立通信，则消息交互过程如图1 所示，采用如下半形式化方式进行描述：

Message 1：Tom→Dick：Pubkey_D｛random_T，Tom｝

Message 2：Dick→Tom：Pubkey_T｛random_T，Temkey，Dick｝

Message 3：Tom→Dick：Temkey｛random，Tom｝

Message 4：Dick→Tom：Temkey｛random｝

图1 用户消息交互过程Fig.1 Process of user message interaction

以上通信过程是结合对称密钥算法和非对称密钥算法的具体应用实例。消息中多次加入了发送方签名，目的在于防止用户将消息发送给不可信任的用户，这些不可信任的用户代理可能会将消息进行存储转发给其他协议用户，从而引起消息内容泄露，即中间人攻击。以具体的通信过程为例，如D_protocol 协议用户Tom 希望与用户Dick 建立通信，间谍Harry 窃听消息并对其进行转发，则消息交互过程如图2 所示。

图2 中间人攻击过程Fig.2 Process of man in the middle attack

在消息中加入用户签名后，如果接收方解密消息，发现消息发送者不是约定好的用户代理时便终止通信过程，该方式可以有效避免内部攻击的发生。在传统公钥加密过程中，由于公钥长度过长，因此导致加密数据量较大的信息时加密速度慢，严重影响通信效率。D_protocol 协议克服了公钥加密过程复杂的问题，在确认通信方身份后，利用对称密钥加密算法对消息进行加密，由于对称密钥可在很短时间内完成加密和解密操作，因此当传输信息量较大时能明显提高通信效率。本文使用Isabelle/HOL 定理证明辅助工具对D_protocol 协议进行形式化建模，采用规则归纳方式验证其安全性。

2.3 协议安全性分析

从算法角度而言，D_protocol 协议属于以密码学相关知识为基础的密钥加密算法，在不发生密钥泄露的情况下通信过程不可攻击。D_protocol 协议将对称密钥加密技术和非对称密钥加密技术进行结合，使用非对称加密技术确定用户身份并传输随机生成的共享单密钥，以临时单密钥的方式对通信主体过程进行消息加密操作。首先考虑非对称加密过程的安全性，用户的公开密钥对其他用户而言是透明的，而私有密钥不对外界公开，仅由持有者可知。公开密钥复杂度较高，导致加密算法的运行速度缓慢。密钥的高复杂度也使得协议攻击者无法在合理的时间范围内由公开密钥推导出私有密钥，即使协议攻击者捕获了密文消息也无法对其进行解密操作。而对称加密算法的加密过程和解密过程使用相同密钥，该密钥仅由通信双方掌握，一旦泄露则消息内容就会被轻易窃取。由于对称加密的密钥复杂度相对较低，因此在很短时间内即可完成加密操作，并且能大幅提升通信效率。

3 通信协议的形式化建模

在D_protocol 协议的形式化证明部分，本文首先对Isabelle/HOL 定理证明辅助工具进行简单介绍，然后建立用户代理和通信消息的抽象模型，并在此基础上对攻击协议的不诚信用户进行形式化建模，使用集合的闭包性质描述攻击行为，最后对D_protocol 协议建立消息流程模型。

3.1 Isabelle/HOL 定理证明辅助工具

Isabelle/HOL 是基于高阶逻辑的形式化证明系统，被广泛应用于计算机软硬件模块的可靠性证明及数学定理的安全性验证等任务中［5，22］。Isabelle/HOL 具有强大的对象描述能力和程序规约表达能力，可以借助类型系统与逻辑之间的同构关系，将定理证明的过程转变为程序编写的过程。由于证明过程的正确性可以通过机器进行自动检查，因此无须依靠自动定理证明算法的正确性，验证结果更具说服力［23］。本文证明过程主要涉及Isabelle/HOL 的归纳集合论，通过定义不同的数据类型及成员函数对D_protocol 协议内容进行表达。

3.2 代理和消息的形式化表示

由于所有安全通信协议规范都涉及通信消息的理论，因此本文首先定义通信协议的参与者类型ptl_agent，具体包括诚实通信代理（User）和通信协议的攻击者（Attacker）两个数据类型，形式化表示如下：

datatype ptl_agent=User|Attacker

D_protocol 协议使用自然数类型作为通信密钥的数据类型，浮点数类型密钥的安全性很强，但其较高的计算复杂度将会严重影响通信效率。由于每个用户都有一个对外公开的公钥和一个秘密存放的私钥，因此定义mapK 函数将用户公钥映射到与之相匹配的私钥，形式化表示如下：

type_synonym key=nat

consts mapK：："key⇒key"

通过定义ptl_msg 数据类型引入通信中消息的标准形式，标准消息包括由代理、密钥、用户生成的随机值、复合消息及加密后的消息等信息，形式化表示如下：

datatype

ptl_msg=Define ptl_agent

Form key

Random nat

Couple ptl_msg ptl_msg

Encrypt key ptl_msg

以上消息类型中出现了Encrypt 加密函数，Encrypt 加密函数是单射函数。在指定加密函数的情况下，如果两条密文消息相同，根据单射函数的性质，则可以确定这两条密文消息对应的明文消息，并且其加密密钥也相同。

理论上而言，一段加密消息只可以用一个密钥解密，且只产生一段明文消息。虽然一段密文也可以用其他密钥解密，但产生的通常是垃圾消息。通过在明文消息尾部添加一些冗余信息，当使用正确密钥对相应的密文消息进行解密后，则可以查出这些附加内容。通过定义mapPu_Key 函数将用户代理映射到与之匹配的公钥，形式化表示如下：

consts mapPu_Key：："ptl_agent ⇒key"

定义NonceK 函数可将用户代理映射到其随机生成的临时单密钥，形式化表示如下：

consts NonceK：："ptl_agent ⇒key"

与以上函数定义类似，通过定义mapPr_Key 函数可将用户代理映射到与之匹配的私钥。mapPr_Key 函数是mapK 和mapPu_Key 函数的结合，形式化表示如下：

abbreviation mapPr_Key：："ptl_agent ⇒key"

where "mapPr_Key A ≡mapK（mapPu_Key A）"

在该通信体制下，分配用户的密钥必须彼此不同，这是保证通信过程安全的必要条件。任何两个用户代理不会有相同的公钥，也不会出现不同用户的公钥和私钥相同的情况。本文验证过程使用事件轨迹的方式记录用户之间传输消息的行为过程，形式化表示如下：

datatype trace=Send ptl_agent ptl_agent ptl_message

3.3 攻击者行为建模

在该协议证明过程中，协议攻击者具有重要作用。攻击者通常是了解协议内容但不遵守协议规则的恶意用户，通过利用协议漏洞对通信过程进行入侵，窃取消息内容，甚至捕获其他代理的密钥。除此之外，攻击者还会使用已获得的用户密钥，构造虚假消息欺骗其他用户，严重危害协议内部的通信安全。

基于Isabelle/HOL 集合理论，构造ptl_analyse 和ptl_create 形式化函数表示通信协议中攻击者的入侵和欺骗行为。ptl_analyse 函数通过对消息集合进行分析得到知识集合，而ptl_create 函数通过对消息集合中的信息进行重组得到虚假消息集合。集合ptl_analyseM表示以消息集合M为参数，函数ptl_analyse 从集合中挖掘有用知识的过程。其闭包性质的递归定义以如下形式化方式表示：

inductive_set

ptl_analyse：："ptl_msg set ⇒ptl_msg set"

for M：："ptl_msg set"

where

Decrypt［intro］："［|Encrypt C A∈ptl_analyse M；

Form（mapPr_Key C）∈ptl_analyse M|］⇒A∈ptl_analyse M"

|mp［simp］："A∈M⇒A∈ptl_analyse M"

|cptl："｛［A，B］｝∈ptl_analyse M⇒A∈ptl_analyse M"

|cptr："｛［A，B］｝∈ptl_analyse M⇒B∈ptl_analyse M"

在以上建模过程中，"｛［］｝"中包含内容为传输消息体，消息体中可能包括一次性随机数、用户签名或者随机单密钥等重要信息。Couple 函数为消息体，（CoupleM1，CoupleM2，…，CoupleMn）即为｛［M1，M2，…，Mn］｝，表示消息体中包含n条消息分量。

对于解密规则，攻击者只要在捕获用户发送消息的前提下进一步取得加密公钥对应的私钥，就可以破解该条消息。通过规则归纳分析可以得知，ptl_analyse 函数具备单射蕴含性质，即如果消息集合A包含消息集合B，那么攻击者通过分别对其进行分析，可以获知知识信息集合A'也必然包含知识信息集合B'。此外，ptl_analyse 函数还具有幂等性质，即攻击者对一个消息集合M进行分析可得到另一个信息集合M'，但即使对M'再次进行分析，也不会产生新的有用信息，形式化表示如下：

Analyse_ide：ptl_analyse(ptl_analyse M)=ptl_analyse M

与ptl_analyse 函数类似，ptl_create 函数的映射关系也是由一个消息集合指向另一个消息集合，攻击者从消息集合中可获知所有遵守该协议的通信代理。对Encrypt 加密函数进行分析，假设X是攻击者从消息集合M中生成的信息，公钥K也属于集合M，因此使用K加密X后的消息仍属于虚假消息集合。由于警惕性较高的用户不可能将私钥作为任何消息的组成部分，也不会将没有经过处理的随机值放在消息中，因此消息集合M中不包含随机值和用户私钥。由上述分析可知，ptl_create 函数可以将消息集合中的信息重新组合，加密生成虚假消息，在入侵过程中用于欺骗其他用户，并不断扩充知识信息集合的容量。基于以上建模基础，继续构造ptl_piece 函数，借助该函数可以较好地分析用户行为的正确性。集合ptl_pieceM由消息集合M的元素分量组成，除了对应的Encrypt 构造函数不同，该归纳函数的定义与ptl_analyse 类似，由于本文篇幅原因，具体定义过程不予给出。

3.4 事件跟随建模

本文将D_protocol 协议的通信过程形式化为一个各项事件跟随的集合，以时间为顺序对各项事件进行串联并记录完整的通信过程。通过该方式可将协议系统中的异常行为定位到具体环节。为避免旧消息的重放攻击，协议系统要求用户产生一个新的随机值。past trace 集合形式化表示为在跟随事件trace 时涉及的所有项目。past 函数通过直接递归定义，事件跟随则是一个信息不断积累的过程。

在攻击者特有的操作函数基础上进一步构造一个面向所有用户的ptl_master 函数，使用该函数可形式化表示用户的知识。与诚实用户相比，攻击者掌握的信息更应受到关注，Attacker ptl_master trace 语句表示在跟随事件trace 时攻击者可用信息的集合。攻击者早在消息交互前就开始处理一些旧的加密消息，在获得被害用户私钥的前提下，对于通信过程中出现的所有以该用户密钥加密的消息，攻击者都可以直接解密并窃取消息内容。集合ptl_analyse（ptl_master Attacker trace）表示在跟随事件的过程中攻击者对于事件trace 中涉及的信息进行分析得到的知识集合。集合ptl_create（ptl_analyse（ptl_master Attacker trace））表示知识生成的虚假信息集。

3.5 协议流程建模

在协议流程形式化表示的过程中，对于用户代理发送的消息序列采用规则归纳方式进行建模，具体过程如下：

inductive_set D_protocol：："trace list set"

where

Null："［］∈D_protocol"

| False："［| M∈ptl_create（ptl_analyse（ptl_master Attacker tracef））；tracef∈D_protocol；|］⇒Send Attacker B M # tracef∈D_protocol"

|MSG1："［|Random RA？past trace1；trace1∈D_protocol；|］⇒Send A B（Encrypt（mapPu_Key B）｛［Random RA，Define A］｝#trace1∈D_protocol）"

|MSG2："［|Send A'B（Encrypt（mapPu_Key B）［Random RA，Define A］）∈set trace2；

trace2∈D_protocol；Random RA？past trace2|］⇒Send B A（Encrypt（mapPu_Key A）｛［Random RA，NonceK B，Define B］｝）# trace2∈D_protocol"

|MSG3："［|Send A B（Encrypt（mapPu_Key B）｛［Random RA，Define A］｝）∈set trace3；

Send B A'（Encrypt（mapPu_Key A）｛［Random RA，NonceK B，Define B］｝）∈set trace3；

trace3∈D_protocol；Random r ？past trace3|］⇒Send A B（Encrypt（NonceK B）｛［Random r，Define A］｝）# trace3∈D_protocol"

|MSG4："［|Send A B（Encrypt（mapPu_Key B）｛［Random RA，Define A］｝）∈set trace4；

Send B A（Encrypt（mapPu_Key A）｛［Random RA，NonceK B，Define B］））∈set trace4；

Send A'B（Encrypt（NonceK B）｛［Random r，Define A］｝）∈set trace4；trace4∈D_protocol|］⇒

Send B A（Encrypt（NonceK B）｛［Random r］｝）# trace4∈D_protocol

除了Null 规则和False 规则之外，以上形式化建模的具体步骤都是按照消息序列的归纳定义而来。Null 规则引入了空追踪，是归纳证明的第1 步操作，False 规则模拟攻击者构造欺诈消息的行为。通信协议入侵者采用重放攻击的策略，将上一阶段通信过程中的有利信息用于此次的攻击操作。

从语义方面解释MSG3 规则，与其对应的半形式化语句如下：

Tom →Dick：Temkey { random，Tom }

MSG3 规则中涉及的第1 个Send 事件表示A 用户向B 用户发送的第1 条消息已经加入第3 步事件跟随中。该规则中涉及的第2 个Send 事件则表示B 用户向另一方回复第2 条消息，用以确定通信另一方用户A 的身份。上述两个事件在第3 步事件跟随前已经发生。分析MSG3 规则中的第3 步操作：

Send A B（Encrypt（NonceK B）｛［Random r，Define A］｝）# trace3 ∈D_protocol

该操作是MSG3 规则的一项扩充事件，其作为用户身份信息的补充说明，并以新密钥加密随机值，在正式通信之前再次握手，确认双方身份。

在通信过程中，每新增一条消息则需要将其加入到事件轨迹中，更新跟随状态。当通信过程受到入侵时，可以很容易将入侵行为定位到具体的消息步骤进而对其进行分析。以上形式化过程的语义模型主要基于Isabelle/HOL 中的集合论，将归纳分析方法作为形式化策略，将非正式的半形式化表达式转化为正式的形式化模型。

4 通信协议安全性证明

4.1 相关定理证明

根据通信协议规范，诚实用户代理总会生成新的随机值说明当前消息的时效性，在一次通信过程中双方代理生成相同随机数的概率几乎为0，只有攻击者才会试图以旧的随机值欺骗用户，因为其不知道该随机值的特殊性。通过定理1 说明通信过程中双方代理生成的随机值互不相同。

定理1

lemma unlike_random：

"［|trace ∈D_protocol；

Encrypt（mapPu_Key E）｛［Random RA，Define A］｝∈ptl_piece（ptl_master Attacker trace）；

Encrypt（mapPu_Key F）｛［RA'，Random RA，Define C］｝∈ptl_piece（ptl_master Attacker trace）|］⇒

Random RA ∈ptl_analyse（ptl_master Attacker trace）"

验证过程如下：

apply（erule rev_mp，erule rev_mp）

apply（simp_all）

apply clarify

apply（erule D_protocol.induct）

apply（auto）

apply（simp add：ptl_analyse_insertI）

apply（blast intro：ptl_analyse_conjE）+

done

在定理1 的基础上，提出与随机值相关的定理2。在一次通信过程中，如果两条消息的结构相同且消息包含的随机值不被入侵者掌握，则可以确定这两条加密消息完全相同。

定理2

lemma："［|trace ∈D_protocol；Random ra ∉ptl_analyse（ptl_master Attacker trace）；

Encrypt（NonceK agy）｛［Random ra，Define agx］｝∈ptl_piece（ptl_master Attacker trace）；

Encrypt（NonceK agy'）（Random ra，Define agx'）∈ptl_piece（ptl_master Attacker trace）|］⇒

agx=agx'⋀agy=agy'"

如果用户生成的随机数或者其私钥被攻击者窃取，则该用户参与的通信过程很容易受到入侵，此时需要将其纳入被害用户集合victim_Muster。反之，如果用户的随机数和密钥均为保密，则该用户不在victim_Muster 集合中。根据以上描述，提出并验证安全性定理3。

定理3

lemma secure_user：

"［|trace ∈D_protocol；

（Form（mapPr_Key C）∈ptl_piece（ptl_master Attacker trace））；

Random C ∈ptl_analyse（ptl_master Attacker trace）|］⇒C ∈victim_Muster"

验证过程如下：

apply ptl_master_aux

apply（drule mp，assumption）+

apply（erule D_protocol.induct）

apply（erule conjE）

apply（auto）

done

4.2 安全性证明

如果通信协议双方都为安全，则其交互的信息必然不会被攻击者窃取，随机生成的密钥值为绝对安全，且后续通信过程也不会遭受攻击。以通信协议的第2条消息为例，通过定理4 证明密钥的保密性。

定理4

lemma Key_Secret［simp］：

"［|trace ∈D_protocol；

T ∉victim_Muster；D ∉victim_Muster；

Send T D（Encrypt（mapPu_Key D）｛［Random RT，NonceK T，Define T］｝）∈set trace |］⇒

NonceK T ∉ptl_piece（ptl_master Attacker trace）"

验证过程如下：

apply（simp_all）

apply（insert D_protocol_victim_aux）

apply（force simp add：protocol_secret_pros）

apply（erule D_protocol.induct）

apply（auto）

done

D_protocol 协议流程建模的主要目的是为建立代理用户的通信，确保双方身份的真实性。用户A向用户B 发送一条消息，并且用户B 的反馈消息内容符合协议规范，则可确定用户A 身份的真实性。由于用户A 和用户B 均不属于被害人集合，因此加密消息体将保持绝对安全，并且此后的通信过程可避免随机值重放攻击现象的发生。为提高协议流程的整体安全性，提出安全性定理5。

定理5

Theorembelief："［|trace ∈D_protocol；

A ∉victim_Muster；B ∉victim_Muster；

Send A B（Encrypt（NonceK B）｛［Random r，Define A］｝）∈set trace；

Send B' A（Encrypt（NonceK B）｛［Random r］｝）∈set trace |］⇒（Random r ∉ ptl_analyse（ptl_master Attacker trace））⋀（Send B A（Encrypt（NonceK B）｛［Random r］｝）∈D_protocol）"

定理5 在Isabelle/HOL 中的验证过程与结果如图3 所示，No subgoals 表明验证完成且未产生新的待证子目标。

图3 Isabelle/HOL 验证过程与结果Fig.3 Verification process and result of Isabelle/HOL

5 结束语

Isabelle/HOL 作为一种功能全面的定理证明辅助工具，在确保验证过程正确性的同时可以提高验证效率，并被广泛应用于各种安全性验证研究工作中。本文借助Isabelle/HOL验证了新构造的D_protocol协议的安全性，在对协议流程进行形式化建模的基础上，采用归纳分析方式对消息交互过程涉及的相关性质展开验证，结果显示D_protocol 协议具有抵抗外部攻击能力的同时可以规避中间人欺骗行为的发生。另外，本文使用Isabelle/HOL 对用户对象进行形式化建模并采用函数语义模型抽象描述用户行为，展示了其在验证通信协议性能方面的应用，并且可为其他领域的形式化验证研究提供理论依据。然而，由于本文使用的定理证明方法主要在数理逻辑层面验证系统相关性质的正确性，但数量有限的定理无法描述无限的系统状态，因此验证结论在一定程度上是不完备的。下一步将结合定理证明和模型检测两种形式化分析方法检查通信协议漏洞并验证相关性质的正确性，从而更全面地分析并研究通信原型系统的安全性。