密码协议实现的逻辑安全分析与设计

内容简介

本书主要探讨密码协议实现（密码协议程序源代码）时的逻辑安全性，并以密

码协议实现时的安全性为前提条件，设计了新的方案。本书引入了逻辑推理与规则

的安全证明，在分析方面，讨论了密码协议实现时的轨迹安全、快速判断密码协议

实现时导致的不安全原因、基于内容安全的密码协议代码实现模型分析和密码协议

实现时的侧信道安全分析。在设计方面，讨论了非签名认证的密钥协商协议设计和

基于协议底层实现安全的密钥协商协议。所有的方法都通过源代码（C语言和Socket

通信编程）进行实验分析，实验结果符合预期要求。

本书可作为计算机科学与技术、网络空间安全、数学与应用数学等信息安全专

业本科生、研究生的学术性指导教材，也可供高等院校从事网络空间安全研究的学

者以及其他领域对信息安全感兴趣的爱好者作为参考资料之用。

图书在版编目（CIP）数据

密码协议实现的逻辑安全分析与设计/吴福生,李延斌

著.—北京：中国铁道出版社有限公司,2022.7

ISBN978-7-113-29091-7

Ⅰ.①密…Ⅱ.①吴…②李…Ⅲ.①密码协议-研究

Ⅳ.①TN918.1

中国版本图书馆CIP数据核字(2022)第071385号

书名：密码协议实现的逻辑安全分析与设计

MIMAXIEYISHIXIANDELUOJIANQUANFENXIYUSHEJI

作者：吴福生李延斌

责任编辑：荆波编辑部电话：（010）51873026邮箱：the-tradeoff@

封面设计：

责任校对：焦桂荣

责任印制：赵星辰

出版发行：中国铁道出版社有限公司（100054，北京市西城区右安门西街8号）

印刷：北京富资园科技发展有限公司

版次：2022年7月第1版2022年7月第1次印刷

开本：787mm×1092mm1/16印张：12字数：252千

书号：ISBN978-7-113-29091-7

定价：79.00元

版权所有侵权必究

凡购买铁道版图书，如有印制质量问题，请与本社读者服务部联系调换。电话：（010）51873174

打击盗版举报电话：（010）63549461

前言

密码协议实现的安全分析是属于数学、计算机和密码学等交叉学科的研究热点之

一，该领域的研究背景不仅需要数学、密码学以及计算机程序语言编程技术等，而且还

涉及逻辑、统计等学科的体系知识，这是一个多学科交叉的研究领域。

密码协议实现涉及复杂环境和多学科知识融合，交叉学科研究前景广阔，主要应用

于密码软件实现的逻辑安全分析、软件设计的逻辑缺陷分析、基于逻辑安全的密码协议

设计与分析、系统实现的漏洞检测与分析等网络空间安全领域。

密码算法是密码技术的核心固件，是网络空间安全的核心技术。在保护公共信道方

面，信息传输起到至关重要的作用。密码协议的安全是建立在密码算法安全基础之上的，

但又不同于密码算法。密码协议至少存在两个参与者，按照一定的规则交互式地交换信

息。虽然基于密码技术的协议在互联网上得到了广泛的应用，在网络空间安全领域中作

出了巨大的贡献，但是随着密码协议实现环境的复杂化以及协同化要求越来越高，网络

攻击事件频频发生，密码协议的分析与设计面临巨大挑战。

基于密码技术的密码协议在理论上被证明是安全的，但是在其编码成为软件实现

时，并不一定是安全的，原因在于密码协议在设计时并没有考虑其实现时的安全性，以

及在设计时的逻辑安全。针对这种情况，本书把密码协议实现时的安全性作为阐述重点，

主要讨论密码协议代码实现时的安全性，并以此作为设计新密码协议方案的前提条件；

在复杂环境下，引入数理逻辑规则与逻辑证明、π-演算的移动与交互理论等，设计新

的密码协议方案，并对新的密码协议实现时进行逻辑安全分析。

对读者的要求

本书主要探讨复杂环境下密码协议实现时的安全性，分析密码协议实现的安全性需

求，设计新的密码方案等。所以在技术上对读者有如下几方面的要求：

（1）具备良好的数学基础知识、现代密码学基础知识和数理逻辑知识，例如，离散

数学、数论、现代密码基础知识以及逻辑规则等；

（2）具备计算机程序语言编程能力，例如，C语言、C++语言以及汇编语言等；

（3）需掌握一定的计算机网络知识与网络编程技术，例如，TCP/IP基础知识以及

基于Socket套接字编程技术；

（4）具备一定的漏洞分析能力、反汇编能力和相关工具的使用能力；例如，漏洞分析、

熟悉C/C++反汇编语言、工具olldbg使用等；

（5）掌握一定的大数据处理与分析技术，例如，数据挖掘、机器学习和统计分析等。

本书写作思路

本书是在长期从事网络空间安全教学与科研的基础上写成的，秉承着理论与实践相

结合的写作思路。

ii密码协议实现的逻辑安全分析与设计

首先，基于密码学的困难数学问题对密码协议代码实现的安全性进行分析，以密码

协议代码实现时的安全因素作为前提条件，设计新的密码协议或改进现有的密码协议，

使新的密码协议适用于对复杂环境下信息的安全保护。

其次，对提出或改进的新密码协议进行源代码分析，包括密码协议代码实现时的特

征和行为的逻辑安全分析。

最后，通过具体的密码协议源代码实现的实验来证实新方案的可行性。

本书是一本学术专著，基本框架是理论与实践的融合，其理论主要来自数学、π-

演算以及移动通信系统等，考虑密码协议代码实现时的安全因素，提出新的密码协议实

现安全分析方案或设计新的密码协议。

本书读者

本书可作为信息安全、网络空间安全以及计算机科学与技术专业的本科生、研究生

学习与学术研究的指导性教材，还可供在高等学校从事信息安全、密码学与应用密码学、

网络空间安全等研究的工作者，以及网络空间安全爱好者学习参考之用。

作者团队与感谢

本书第8章由李延斌编写，其余章节由吴福生编写，并由吴福生对全书统稿。

本书的出版得到了国家自然科学基金项目（No.62062019,62072247,62061007）和贵

州财经大学学术专著出版专项资助。在写作过程中，引用了大量的文献，在此谨向这些

文献的作者表示诚挚的谢意。

因笔者学术水平有限，书中难免会有不妥和错误之处，对此，恳请读者的理解和批

评指正，并于此先致感谢之意。

衷心感谢博士生导师张焕国教授，感谢硕士生朱嘉杰、王雪梅的细心校对以及给予

指导、支持和帮助的所有领导、专家和同行，衷心感谢本书的每一位读者。

吴福生李延斌

2022年5月

目录

第1章绪论

1.1引言1

1.2关键技术3

1.3本书结构介绍4

参考文献5

第2章密码协议实现安全的研究现状

2.1代码模型提取安全验证分析9

2.1.1C语言模型提取分析9

2.1.2Java语言模型提取分析15

2.1.3F#语言模型提取分析16

2.2代码自动生成安全验证分析18

2.2.1基于编译器代码自动生成分析19

2.2.2基于Java语言代码自动生成分析20

2.3基于操作语义安全验证分析22

2.4密码协议精化安全验证分析27

2.4.1精化检测工具协议分析27

2.4.2程序精化分析28

2.4.3信息流精化分析29

2.5本章小结30

参考文献30

第3章非签名认证的密钥协商协议设计

3.1新协议涉及的群同态基础知识39

3.1.1群同态的基本定义39

3.1.2群同态的基本定理39

3.2整数乘法同态二叉树的构造与分析40

3.3整数乘法同态二叉树的基本遍历与性质41

3.4整数乘法同态二叉树的密钥协商协议42

3.4.1构造一棵叶子结点为素数的整数乘法同态二叉树42

3.4.2整数乘法同态二叉树密钥协商协议具体步骤43

3.5协议安全分析44

ii密码协议实现的逻辑安全分析与设计

3.5.1一般安全性分析44

3.5.2随机预言模型（RandomOracleModel）的可证明安全分析45

3.6新协议结构的安全分析46

3.7新协议性能比较与实验分析46

3.7.1新协议的二叉树存储与遍历46

3.7.2新协议实现的实验47

3.7.3参数n对网络通信的影响50

3.8本章小结52

参考文献52

第4章通过密码协议在代码级上实现时的轨迹行为是否异常来评估其

安全性

4.1相关研究工作55

4.2知识准备56

4.2.1标号迁移系统与强模拟56

4.2.2程序的精化57

4.2.3密码协议源代码的程序精化58

4.3建立模型58

4.3.1密码协议的符号化描述59

4.3.2密码协议源代码精化59

4.3.3程序控制流图63

4.3.4从控制流图到状态图65

4.3.5密码协议实现的轨迹65

4.4密码协议实现的安全分析66

4.4.1函数返回值的操作语义66

4.4.2非理想轨迹与理想轨迹67

4.5针对Needham-Schroeder协议与Diffie-Hellman协议及它们的改进协议在理想与攻击

环境下的实验68

4.5.1新方法实现的步骤68

4.5.2Needham-Schroeder协议及其改进协议实现的实验69

4.5.3Diffie-Hellman协议及其改进协议实现的实验77

4.5.4密码协议实现的实验分析84

4.6本章小结88

参考文献88

第5章快速判断密码协议在代码级上实现时导致的不安全原因

5.1相关研究工作92

5.2知识准备92

目录iii

5.2.1标号迁移系统92

5.2.2密码协议实现操作语义93

5.2.3密码协议实现规范94

5.3新模型的建立94

5.3.1函数返回值字典94

5.3.2函数返回值序列95

5.3.3密码协议代码实现安全分析95

5.4针对经典密码协议的实验与分析96

5.4.1NSL协议代码实现的符号化规范97

5.4.2NSL协议部分源代码标注97

5.4.3NSL协议代码实现的安全分析101

5.4.4新模型与原来模型比较103

5.5本章小结104

参考文献105

第6章针对代码底层汇编语言实现跳转设计新的密钥协商协议

6.1知识准备109

6.1.1程序运行时寄存器的分配情况109

6.1.2程序调用（CALL）与返回（RET）操作情况110

6.1.3内存溢出造成漏洞攻击情况111

6.2改进的密钥协商协议112

6.2.1基础知识112

6.2.2改进的密钥协商协议设计113

6.3改进的密钥协商协议安全分析114

6.3.1基于密码理论的安全分析114

6.3.2基于串空间的改进的密钥协商协议实现的安全分析115

6.4基于RET改进的密钥协商协议实验116

6.4.1修改RET配件链117

6.4.2密钥协商协议实验118

6.4.3实验结果与性能分析122

6.5本章小结124

参考文献124

第7章基于内容安全的密码协议代码实现行为安全

7.1相关研究工作128

7.2基础知识129

7.2.1霍恩子句逻辑129

7.2.2密码协议规范129

7.3新模型的建立与分析131

iv密码协议实现的逻辑安全分析与设计

7.3.1密码协议的操作语义131

7.3.2建立密码协议行为安全的分析模型132

7.4基于经典密码协议的新分析方法实验133

7.4.1具体的实现步骤133

7.4.2模拟实验134

7.5安全与性能分析135

7.5.1NSL协议描述135

7.5.2NSL协议代码实现的安全分析137

7.5.3行为安全分析137

7.5.4新模型与现有分析模型比较138

7.6本章小结139

参考文献139

第8章密码协议的软件实现安全分析

8.1软件实现的物理层安全142

8.1.1侧信道攻击142

8.1.2密码协议软件实现的物理层安全147

8.2密码防护方案的实现安全152

8.2.1掩码方案安全性153

8.2.2软件实现安全性分析155

8.2.3针对实际环境中软件实现的安全性分析实验161

8.2.4防护策略167

8.3本章小结169

参考文献169

第9章总结与未来展望

9.1总结176

9.2未来展望178

参考文献181

第1章绪论

在开放网络空间中，密码协议是保护信息安全传输[1]，严防信息在传输过程中隐私泄

露的关键技术[2]。迄今为止，设计一个安全、适用的密码协议仍是研究者们关注的重点问

题之一。很多协议从设计到使用总会出现“使用→发现漏洞→修改→使用→发现漏洞

→……→修改→使用”的循环现象。这一现象说明密码协议设计与安全实用之间仍存在

一定差距。因此，研究者们思考：能否在密码协议设计阶段就考虑它实现时的安全性？

为了解决这一问题，在密码协议设计时，研究者们引入许多密码协议分析方法（例如，

形式化、计算模型、计算可靠的形式化等），以便发现协议的漏洞，弥补协议实现时安全

性的不足。常用的密码协议安全分析方法只能从理论上验证或证明密码协议的安全，无

法确保密码协议实现的安全。只有当密码协议在转换成软件（程序源代码）实现时被验

证或证明是安全的，才能保证密码协议是安全的。因此，密码协议实现的安全分析与设

计是值得关注的方向，也是网络空间安全领域研究的热点之一。

1.1引言

一直以来，密码协议安全验证分析是衡量协议是否安全可靠的重要手段之一。随着

大数据、云计算、物联网和5G等技术的不断成熟，传统单一的端到端网络通信模式已转

换为多对一、多对多的新型网络通信模式。在新型网络环境下，通信信息更易受到攻击，

用户的隐私更易泄露[3,4]。因此，常用密码协议的安全验证分析方法已无法满足新型网络

通信模式下的信息安全需求，对密码协议的安全分析与设计提出了更高要求[5]。

常用的密码协议安全验证分析只能验证或证明协议的理论安全，无法确保密码协议

在代码级上实现时的安全。究其原因是没有考虑下述几种情况：

①程序设计语言的语法和语义结构（例如，C语言内存泄漏、指针越界、缓冲区溢

出等）；

②程序代码执行时产生很多临时的异常情况（例如，函数调用的不确定返回值、程

序中断、程序断言等）；

③程序代码实际执行的运行环境（例如，不同网络环境、不同语言环境等）。由此可

见，密码协议实现时的安全验证分析比形式化模型或计算模型下的密码协议安全验证分

析复杂。密码协议实现的安全验证，特别是在代码级上实现时的安全分析与设计是网络

空间安全领域研究的新方向[6]。

密码协议实现的安全分析与设计作为网络空间安全领域一个新的研究方向，在国内

2密码协议实现的逻辑安全分析与设计

外处于起步阶段。在国外，代码级的密码协议安全验证分析的研究包括代码模型提取[7]、

代码自动生成[8]、操作语义分析[9]和精化（refinement）验证分析[10]。在国内，仍以常用

的安全验证分析方法为主，例如，基于网关口令的认证[11]、基于关键字域可变协议的验

证[12]等。这些安全验证分析基于计算语义安全来分析密码协议的安全性，或用现有工具

和软件检测模型技术来验证密码协议是否安全[13,14]。而针对密码协议实现时的安全分析

与设计相关研究少之又少。

密码协议安全验证分析是验证或证明协议安全属性是否成立，确保密码协议在设计

上没有缺陷，在代码级上执行时能避免漏洞产生。传统的密码协议安全验证分析方法有

三类：形式化分析、计算模型分析和计算可靠的形式化分析。

（1）密码协议形式化分析

形式化分析是对协议的各要素进行抽象符号化，然后基于逻辑的推导，从而发现密

码协议中的缺陷。文献[15]正式提出密码协议安全验证的形式化分析，形成以Dolev-Yao

模型假设[16]为基础的形式化安全分析方法。文献[17]首次在密码协议的形式化分析中应用

BAN逻辑推导，基于BAN逻辑的形式化安全验证分析方法是密码协议安全分析的一个里

程碑。

（2）密码协议计算模型分析

计算模型分析采用概率大小衡量密码协议的安全性，其理论基础为计算理论（例如，

可忽略函数、多项式时间和计算不可区分性等），并涉及困难数学问题（例如，大整数因

式分解、离散对数和椭圆曲线等）。相关研究可见文献[18][19][20]。

（3）密码协议计算可靠的形式化分析

计算可靠的形式化分析是形式化模型与计算模型有机结合的一种密码协议安全验证

分析方法。该分析方法是指如果密码协议在形式化模型下安全，则在计算模型下也必然

安全，即密码协议安全属性的形式化分析与计算模型分析是等价的，该分析方法的代表

模型是AbadiRogway模型[21]（简称AR模型）。基于AR分析方法，文献[22]进一步提出

密码协议计算语义与形式化模型结合的分析方法，基于逻辑语义分析方法来分析密码协

议的安全性。文献[23]证明协议属性在计算语义与形式化两种不同的模型下都是安全的，

即密码协议安全属性的可靠性（soundness:表示在交互式证明系统中两个状态或模型变换

时，某一属性变化的概率可忽略不计，即协议属性可靠）是等价的。文献[24]提出自动的

密码协议安全可靠性证明，提升了密码协议安全属性的可靠性，并在实际中得到应用[25]。

基于计算语义与形式化模型，文献[14]提出刚性与相似性概念的安全验证分析方法。这种

分析方法以密码协议语法和语义赋值为理论，从而构建有攻击能力模型的非自由消息代

数理论框架，同时证明协议在该框架内满足安全的可靠性。

常用的密码协议安全验证分析已取得丰硕的成果[6]，但并没有考虑密码协议代码级上

实际执行时存在的问题：

第1章绪论3

①程序语言结构困难（例如，C语言的内存泄漏、Java封装、F#语义等）；

②从密码协议规范到代码执行产生漏洞（例如，程序中断、变量的不正确使用等）；

③程序代码执行迹的困难（例如，代码的消息匹配、函数调用的不正确返回值等）；

④程序代码执行的行为困难（例如，在具体状态空间下，密码协议的属性验证）。要

解决这一系列问题，需拓展密码协议在代码级上实现时的安全分析与设计方法。

1.2关键技术

代码级上实现的安全验证分析有助于发现协议设计阶段不容易发现的问题（例如，

缓冲区溢出和密码协议设计的缺陷），这些问题往往在密码协议实现过程中才被发现，把

密码协议在代码级实现的安全因素作为设计前提，可以有效避免漏洞的产生以及利用漏

洞进行的攻击。如果把密码协议代码实现时的安全性引入到设计阶段，可以有效地预防

和避免协议代码实现过程中漏洞的产生和遭受利用漏洞的攻击（例如，代码重用攻击和

shellcode注入攻击），从而达到密码协议设计的目的。

1．非签名认证的密钥协商协议设计研究方法

密钥协商协议广泛应用于各种网络环境中，例如，无线传感器网络、IoT（Internetof

Things，物联网）网络和云计算环境等。目前，现有的密钥协商协议为保证交互式通信中

的安全，常常引入额外的安全技术（签名和认证等）。额外的签名认证技术增加了密钥协

商协议实现时的计算量，不适用于计算能力有限的移动终端通信设备的通信。如何设计

出计算量少且又安全的密钥协商协议是研究者们思考的问题。针对这种情况，基于二叉

树特点，设计一种新的密钥协商协议[29]，该密钥协商协议具有计算量少、使用强安全假

设少的优点。

2．通过密码协议在代码级上实现时的轨迹行为是否异常的研究方法

根据自动机原理，程序运行实质上是状态之间的转换，这种转换表现出程序代码实

现的行为。只有当密码协议转换成某一种具体程序语言代码时才能体现其价值。程序语

言在代码实现时函数之间的调用是必不可少的，例如，C/C++语言、Java语言和Python

语言等。函数调用得到的函数返回值影响程序流的走向，从而影响密码协议交互式通信

的行为。基于这一观点，根据程序代码实现时函数返回值轨迹的变化来分析密码协议实

现的安全性[26]。

3．快速判断密码协议在代码级上实现时导致不安全原因的研究方法

密码分析模型一直以来都是信息安全研究的重点之一，特别是分析密码协议代码实

现的安全模型值得关注。针对密码协议代码实现的安全分析，本书提出一种基于字典序

列模型的密码协议代码实现的安全分析方法[27]。这种方法是在密码协议代码实现时，通

过函数返回值序列的变化来分析协议实现是否安全。基于新模型的安全分析方法，给出

经典密码协议实现的实例。实验结果表明，新模型方法相比以前的模型分析方法更好。

4密码协议实现的逻辑安全分析与设计

新模型方法的提出为密码协议实现的设计、评估和测试提供了帮助。

4．针对代码底层汇编语言实现跳转设计新的密钥协商协议的研究方法

目前，大多数密钥协商协议还是基于Dolev-Yao模型假设来评估其安全性，在密钥协

商协议设计阶段未考虑代码实现时的安全性。这导致密钥协商协议代码实现时会出现很

多不安全的问题（例如，缓冲区溢出、注入攻击和代码重用攻击等）。基于程序代码实现

时的函数返回的RET指令值，设计一种新的密钥协商协议[28]。该方案在密钥协商协议设

计阶段就考虑其代码实现时的安全性。该方案不仅考虑协议理论上的安全，而且考虑协

议实现时防止代码重用攻击和缓冲区溢出攻击等问题。

5．基于内容安全的密码协议代码实现行为安全的研究方法

安全分析模型是密码安全实现的重要保障，行为安全是信息安全研究的内容之一。

现有的分析模型仅仅从理论上保证密码协议实现的安全，而没有考虑密码协议实现时的

行为安全（例如，无线网络中的拒绝服务、会话劫持和程序漏洞攻击等）。密码协议实现

的行为是否安全，取决于其实现时的行为是否异常，所以针对密码协议实现的行为安全

模型被提出[30]。该模型将密码协议实现的行为定义为外部行为和内部行为两个部分。外

部行为是指开放网络空间实体之间交互通信的行为；内部行为是指密码协议编码程序源

代码实现的行为。通过外部行为与内部行为的异常分析，从而发现、控制或纠正密码协

议实现的异常行为，掌握对密码协议实现行为的可控性。为验证该模型的可控性，本章

以经典协议密码协议为实例进行模拟实验，并验证了密码协议实现是安全可控的。

6．密码协议软件实现的物理层安全分析的研究方法

随着掩码的发展，对应的攻击技术也不断提升，针对一阶或高阶掩码防护方案，对

应出现了二阶功耗分析[31]和高阶功耗分析[32]，其攻击原理与一阶功耗分析相似，在进行

区分器分析之前需要对不同掩码操作对应的功耗点利用组合函数进行预处理。攻击方法

不断追求着优化泄露模型与区分器模型，寻求更低复杂度或其他角度去攻击。

基于密码协议实现的安全性考虑，针对密码协议实现的逻辑安全分析与设计，本书

分别从密码协议设计、密码协议源代码实现的行为安全、基于汇编语言的密码协议源代

码底层实现的安全和密码协议实现的侧信道攻击等方面的研究进行探讨。

1.3本书结构介绍

本书内容共分为9章，下面来简要了解一下各章的主要内容。

第1章绪论。本章介绍研究的背景与意义，陈述国内外研究现状以及研究内容，最

后给出本书的组织结构。

第2章密码协议实现安全的研究现状。本章分别介绍代码模型提取安全验证、代码

自动生成安全验证、基于操作语义安全验证、密码协议精化安全验证等研究内容。

第3章非签名认证的密钥协商协议设计。为了满足计算能力有限的通信设备，基于

第1章绪论5

二叉树特点和同态映射设计了一种非签名认证的新密钥协商协议。该密钥协商协议没有

使用额外的签名认证技术，所以在协商共享密钥时，具有计算量少和强安全假设少等优

点，适用于计算能力有限的移动通信设备。

第4章通过密码协议在代码级上实现时的轨迹行为是否异常来评估其安全性。基于

程序代码实现时的函数返回的RET指令值，设计一种新的密钥协商协议。该方案在密钥

协商协议设计阶段就考虑其代码实现时的安全性。该方案不仅考虑协议理论上的安全，

而且考虑协议实现时防止代码重用攻击和缓冲区溢出攻击等问题。

第5章快速判断密码协议在代码级上实现时导致的不安全原因。使用密码协议代码

实现的函数返回值组成的迹，分析协议实现的安全。具体以经典的密码协议

（Needham-Schroeder协议和Diffie-Hellman协议）为实例，分析密码协议代码实现时的

中间人攻击情况。通过理论分析与实验表明该方法是可行和有效的。

第6章针对代码底层汇编语言实现跳转设计新的密钥协商协议。攻击者利用程序漏

洞改变RET值，导致程序实现顺序被攻击者任意控制，严重地影响密码协议实现的安全

性。设计一种基于RET配件链的新密钥协商协议。该密钥协商协议不仅考虑密码技术上

的安全，而且考虑程序代码实现时的控制流完整性，防止密钥协商协议实现时程序漏洞

的攻击和代码重用攻击。

第7章基于内容安全的密码协议代码实现行为安全。设计一种基于密码协议实现的

行为安全分析模型。该模型把密码协议实现分为两部分：一是外部行为（开放网络空间

交互通信的行为）；二是内部行为（代码实现的行为）。通过行为的可控性，能够发现、

控制或纠正密码协议实现的安全。基于该分析模型方法，本章以经典的密码协议为实例

进行模拟实验。实验结果表明，密码协议实现的行为安全是可控的。

第8章密码协议的软件实现安全分析。本章介绍针对密码协议编码成为软件实现的

物理层安全，以密码协议实现的侧信道攻击为主，探讨一阶或高阶掩码防护方案，阐述

密码软件实现的安全性。

第9章总结与未来展望。本章介绍对研究内容进行了总结，并对未来的工作进行

展望。

参考文献

[1]张焕国,韩文报,来学嘉,等.网络空间安全综述[J].中国科学:信息科学，2016,46(2):125-164.

[2]章睿,薛锐,林东岱.海云安全体系架构[J].中国科学:信息科学，2015,45(6):796-816.

[3]冯登国,张敏,李昊.大数据安全与隐私保护[J].计算机学报，2014,37(1):246-258.

[4]陈克非,翁健.云计算环境下数据安全与隐私保护[J].杭州师范大学学报（自然科学版），

2014,13(6):561-571.

[5]曹珍富.密码学的新发展[J].四川大学学报（工程科学版），2015,47(1):1-12.

6密码协议实现的逻辑安全分析与设计

[6]雷新锋,宋书民,刘伟兵,等.计算可靠的密码协议形式化分析综述[J].计算机学报，2014，37(5)：

993-1016.

[7]BHARGAVANK,FOURNETC,ANDREWDG,eta1.Verifiedinteroperableimplementations

ofsecurityprotocols[J].ACMTransactionsonProgrammingLanguagesandSystems,2008,31(1):1-61.

[8]O’SHEAN.VerificationandValidationofSecurityProtocolImplementations[D].Schoolof

Informatics,UniversityofEdinburgh,UK,2010.

[9]CREMERSC,MAUWS.OperationalSemanticsandVerificationofSecurityProtocols[J].

Springer-VerlagBerlinHeidelberg,2012.

[10]ABADIM,LAMPORTL.Theexistenceofrefinementmapping[J].TheoreticalComputer

Science,1992,82:253-284.

[11]魏福山，张振峰，马传贵.标准模型下网关口令认证密钥交换协议的通用框架[J].计算机学

报,2012,35(9)：1833-1843.

[12]苗银宾，马建峰，刘志全，等.关键字域可变的可验证密文检索[J].西安电子科技大学学报

（自然科学版）,2017,44(1)：57-63.

[13]唐朝京,鲁智勇,冯超.基于计算语义的安全协议验证逻辑[J].电子学报,2014,6(42):1179-1185.

[14]田园,王颖,金锋,等.基于刚性与相似性概念的密码协议分析方法[J].计算机学报，

2009,32(4):618-634.

[15]NEDDHAMRM,SCHROEDERMD.Usingencryptionforauthenticationinlargenetworksof

computers[J].CommuicaonsoftheACM,1978,21(12):993-999.

[16]DOLEVD,YAOAC.Onthesecurityofpublickeyprotocols[C]//Proceedingsofthe22nd

SymposiumonFoundationofComputerScience.Oakland,USA.1981:350-357.

[17]BURROWSM,ABADIM,NEEDHAMR.Alogicofauthentication[R].PaloAlto,USA:Digital

EquipmentCorp,SystemsResearchCenter,1989:39.

[18]BLUM,MICALIS.Howtogeneratecryptographicallystrongsequencesofpseudorandom

bits[C]//Proceedingsofthe23rdAnnualSymposiumonFoundationsofComputerScience.Los

Alamitos,USA,1982:112-117.

[19]YAOAC.Theoryandapplicationoftrapdoorfunctions[C]//proceedingsofthe23rdIEEE

SymposiumonFoundationsofComputerScience.Califonia,USA,1982:80-91.

[20]GOLDWASSERS,MICALIS.Probabilisticencryption[J].JournalofCompterandSystemSciences,

1984,28(2):270-299.

[21]ABADIM,ROGAWAYP.Reconcilingtwoviewsofcryptography:thecomputational

soundnessofformalencryption[J].JournalofCryptology,2002,15(2):103-127.

[22]MICCIANCIOD,WARINSCHIB.CompletenesstheoremsfortheAbadi-Rogawaylogicof

encryptedexpressions[J].JournalofComputerSecurity,2004,12(1):99-129.

第1章绪论7

[23]BLANCHETB.Computationallysoundmechanizedproofsofcorrespondenceassertions[C]//

Proceedingsofthe20thIEEEComputerSecurityFoundationsSymposium.Venice,Italy,2007:97-111.

[24]CORTIERV,WARINSHIB.Computationallysound,automatedproofsforsecurityprotocol

analysis[J].LogicalMethodsinComputerScience,2007,3(3),396-458.

[25]BACKESM,PFITZMANB,WAIDNERA.Acomposablecryptographiclibrarywithnested

operations[C]//Proceedingsofthe10thACMConferenceofComputerandCommunicationsSecurity,

NewYork,UK,2003:122-136.

[26]WUFS,ZHANGHG,WANGWQ,etal.ANewMethodtoAnalyzetheSecurityofProtocol

ImplementationsBasedonIdealTrace[J].SecurityandCommunicationNetworks,Volume2017:1-15.

[27]WUFS,ZHANGHG.ADictionarySequenceModeltoAnalyzetheSecurityofProtocol

ImplementationsattheSourceCodeLevel[J].ChineseConferenceonTrustedComputingand

InformationSecurity.23November2017:126-142.

[28]WUFS，ZHANGHG，NIMT，etal.ANovelKeyAgreementProtocolBasedonRETGadgetChains

forPreventingReusedCodeAttacks[J].IEEEAccess.2018，6:70820-70830.

[29]吴福生,张焕国.基于二叉树的非签名认证密钥协商协议[J].计算机研究与发展.

2017,54(12):2797-2804.

[30]吴福生,张焕国,倪明涛,等.基于密码协议实现的行为安全分析模型[J].山东大学学报（理学

版）.2019,54(3):1-11.

[31]OSWALDE,MANGARDS,HERBSTC,etal.Practicalsecond-orderDPAattacksformasked

smartcardimplementationsofblockciphers[C].Cryptographers’TrackattheRSAConference.Springer,

Berlin,Heidelberg,2006:192-207.

[32]LEMKERUSTK,PAARC.GaussianMixtureModelsforHigher-OrderSideChannelAnalysis[M].

CryptographicHardwareandEmbeddedSystems-CHES2007.SpringerBerlinHeidelberg,2007:14-27.

第2章密码协议实现安全的研究现状

从应用的角度看，密码协议最终以程序代码形式表现，其作用需落到代码实现上去。

因此，一个密码协议是否安全适用，最终还得看协议的代码实现是否安全适用。由于密

码协议代码实现环境复杂，在分析它的安全性时会产生这样的问题：即使经过理论证明

安全的协议，在其代码实现过程中，若引入新的不安全因素，则会导致密码协议代码实

现时的不安全。究其原因是没有考虑下述几种情况：

①程序语言的语法和语义结构不完善（例如，C语言指针越界和缓冲区溢出等）；

②程序代码实现时会产生临时的异常情况（例如，函数调用返回值的不确定性、程

序中断和程序断言）；

③程序代码实现在不同的运行环境（例如，网络环境与语言环境等）下实现。

由此可见，密码协议代码实现的安全分析方法比常用的安全分析方法复杂。密码协

议代码实现的安全分析是保证信息安全传输的关键技术。现已发展成为信息安全研究的

新方向[1]。漏洞对软件的危害是工业界与学术界关注的信息安全重点问题之一。漏洞产生

原因：

一是软件设计不完善，存在缺陷；

二是程序设计语言自身有缺陷。

最值得关注的是C与C++等计算机程序语言中普遍存在漏洞。例如，计算机指令

可对内存直接存取；C与C++语言对用户的输入没有自动的边界检查机制，以及对释放

的指针再次利用[2]。导致利用基于缓冲区溢出[3]漏洞的代码重用攻击。代码重用攻击是利

用程序漏洞的一种典型攻击行为，而且具有远程特征，破坏性极大。攻击者可以灵活使

用代码重用攻击绕过当前很多防御机制。因此，这种攻击在国际学术界引起了极大的关

注。例如，2017年WannaCry勒索病毒，本质上是攻击者利用WindowsSMB协议的漏

洞，通过远程实施代码来提升自身系统权限而实施的一种攻击。2015—2020年间在国际

顶级的安全会议[CCS（ACMConferenceonComputerandCommunicationsSecurity）、S&P

（IEEESymposiumonSecurityandPrivacy）和USENIX(USENIXSecuritySymposium)和

NDSS（NetworkandDistributedSystemSecuritySymposium）]发表大量有密码协议安全分

析的学术论文。

密码协议属于软件的范畴，同样可能遭受因程序语言结构缺陷所带来的攻击。例如，

2014年4月8日，研究人员发现OpenSSL的源代码中存在一个漏洞，可以让攻击者

获得服务器上64K内存中的数据内容，并为其起了个形象的名字：心脏出血[4]。导致这

第2章密码协议实现安全的研究现状9

次事件的直接原因是OpenSSL协议源代码中的C语言部分函数无法完成边界检测。

TLS协议是广泛使用的应用协议。针对密码协议的安全性研究出现了很多研究成果（最

近五年，在四大国际顶级系统安全会议发表关于密码协议的研究成果，如表2-1所示）。

由此可见，基于密码协议安全分析与设计越来越受到学术界与工业界的重视。

表2-1发表与密码协议相关论文统计表

年份201520162017201820192020

篇数111317161915

密码协议代码实现的安全分析与设计不同于传统的方法，不管是协议的安全分析还

是设计新的协议，都是基于协议代码实现时的安全性来考虑，这也正是研究者们希望达

到的目标。如果设计新的协议时不考虑它的代码实现情况，就不能从代码实现上去分析

其安全性，这样往往导致协议代码实现时发生错误。密码协议代码实现的安全分析是信

息安全的关键环节，是协议实现安全的重要保障，在整个通信安全中起到关键作用。

2.1代码模型提取安全验证分析

模型提取方法来源于程序属性的抽象解释论[5]和经典的抽象理论[6]。代码模型提取是

把密码协议的某一具体属性映射成它的某一抽象属性，并证明如果抽象属性成立，那么

具体属性也成立。

MMP,E=()

不妨设P是协议，E是环境，M为建模，具体协议模型为c；α()⋅是抽象映

α()M∅

射，则抽象模型为c。不妨设为密码协议的具体属性，它对应的抽象属性为α()∅。代

α()Mα()∅→M∅→

码模型提取的数学表示为c├c├，其中，“├”表示推导，“”表示蕴含。

由此可见，代码模型提取考虑两个因素：

①映射函数α()⋅的可靠性。文献[7]把密码协议代码（用C语言编写程序代码）的注

释假设为可信任项，并把它作为模型提取研究的一部分；

②协议环境（例如，语言特征，程序运行的环境等）。由于Java语言、F#语言等是具

有良好封装性的高级语言，所以在代码模型提取中侧重于考虑程序运行的环境问题。

不同程序设计语言的语义、语法、句法不尽相同。例如，C语言考虑指针，Java语

言进行封装，F#语言具有相对完备的语义且封装程度更高。下面分别介绍基于C、Java、

F#三种语言的密码协议代码模型来提取安全验证分析。

2.1.1C语言模型提取分析

C语言的主要特点是指针运算和函数，但密码协议的规范无法表达C语言的内部函

数（例如，allocation,pointer等）与外部函数库（例如，memcpy、strcpy等）的链接，这

使密码协议代码安全验证分析变得复杂和困难。为解决这一矛盾，C语言代码模型提取把

具体模型的协议代码映射为抽象模型的协议规范，然后根据抽象模型的协议规范进行安

10密码协议实现的逻辑安全分析与设计

全验证分析。本小节从以下三个方面介绍C语言的密码协议代码模型提取。

（1）基于信任断言分析

信任断言分析是一种C语言代码模型提取的协议代码执行安全验证分析方法，由内

部和外部两个模型组成。它将密码协议代码安全验证的复杂性与困难性作为信任假设，

构建密码协议代码实际执行时的内部信任（InternalTrust）和外部信任（ExternalTrust）。

文献[7]首次提出信任断言模型的C语言代码模型提取分析方法。该方法使用霍恩子句逻

辑（HornClausesLogic）来表示密码协议规范和攻击者的能力。它假设密码协议代码执

行的C语言指针运算为内部信任，建立信任断言模型（TrustAssertionsModel）对协议进

行安全验证分析。

①外部信任断言模型（ExternalTrustAssertionsModel，ETAM）假设攻击者拥有信任

断言的能力（knows作为谓词，knows（X）表示攻击者具有获得X知识的能力），如表2-2

所示。

②内部信任断言模型（InternalTrustAssertionsModel，ITAM）假设C语言内部的编

译序列为信任断言。

表2-2外部信任断言模型

霍恩子句模型化入侵者能力

knows(nil)

入侵者建立列表

knows(cons(X,Y))<-knows(X),knows(Y)

knows(X)<-knows(cons(X,Y))

入侵者读取列表所有基本信息

knows(Y)<-knows(cons(X,Y))

knows(crypt(X,Y))<-knows(X),knows(Y)入侵者能够加密

knows(pub(X))入侵者知道公钥

knows(X)<-knows(crypt(X,pub(Y))),knows(prv(Y))

knows(X)<-knows(crypt(X,prv(Y))),

knows(pub(Y))入侵者用他知道的解密密钥能够解密密文

knows(X)<-knows(crypt(X,sk(Y,Z))),

knows(sk(Y,Z))

x,t∈AtomPQQQn←≠,,,,
0

设，xrect表示x信任t。根据霍恩子句逻辑表示（12n，

P表示过程名；Qi表示过程调用，且in∈）可知，逻辑表达式成立：

xtrec←xrect

11

（2-1）

xrectxt,,
rec

22nn

这里的xirecti表示xi信任ti。例如，一条简单的C语言代码：msg−>id_[]10=id[]0，根

据C语言内部编译可得到编译序列如下：

第2章密码协议实现安全的研究现状11

zx==0&id,,[]zxx=∗

121

x=→_1（）

3msgid2-2

xxzxx=∗=[],

4342

由式（2-1）和式（2-2）得到表达式（2-3）成立：

zrec0,xrecid[]z

1

xxx∗→,_（）

213recrecmsgid12-3

xxzxx[],∗

43rec42rec

由霍恩子句逻辑可知式（2-4）成立：

msg−>id_[]10recid[]0←

zx,[]z

rec01recid

（2-4）

xxx∗→,_1

213recrecmsgid

xxzxx[],∗

43rec4rec2

由此可见，基于信任断言的具体分析过程是密码协议源代码经过C语言内部编译后，

得到一些有序的编译序列，通过霍恩子句逻辑推导得到ITAM编译序列。根据ITAM和

ETAM对密码协议代码执行的安全验证分析。

文献[7]提出信任断言方法考虑到密码协议代码实际执行的情况，但无法解决密码协

议代码执行的具体行为（例如，初始化加密、解密和Hash函数[8]等），也没有考虑到C语

言数组越界[9]和缓冲区溢出[10]等情况，更没有考虑到密码协议的安全认证。基于信任断言

模型的密码协议安全验证分析仍有待进一步完善。有进一步需求的读者，请参考文献[7]

中的相关内容。

（2）基于自动化分析

自动模型提取采用自动模型框架对密码协议代码执行进行自动安全验证分析。文献

[11]提出基于C语言的ASPIER（AutomatedSecurityProtocolImplementationverifyER，

自动模型框架的密码协议代码）执行安全验证分析方法，该方法使用ASPIER自动模型框

架对OpenSSL进行安全验证分析。文献[12]提出VCC（VerifyingConcurrentC）并发框架

和多线程的安全验证分析，适用于通用自动模型提取的密码协议代码执行安全验证分析。

①ASPIER自动分析。这种分析是基于软件模型检测标准的安全验证分析方法。在具

体的密码协议代码执行自动模型提取分析中，用状态规范机制SSMs（SSMs=specification

statsmachines）取代C语言库函数，对密码协议安全属性进行验证分析。ASPIER有类似

于C语言的语法结构。因此，ASPIER自动分析适用于代码级的密码协议安全验证分析。

与C语言不同，ASPIER有自己的语言结构和验证方法，即把密码协议的C语言源代码

转换为类似于C语言的抽象伪代码。ASPIER自动分析表现在自动验证、作为抽象工具和

12密码协