{正版现货新书} 网络安全协议的形式化分析 9787560675176 付玉龙

第一单元基础知识

第1章绪论

1.1形式化安全方法概述

1,2通信安全中的形式化方法

1.3软件安全中的形式化方法

1.3.1软件安全的重要性与漏洞历史案例

1.3.2软件漏洞的挑战与统计

1.3.3软件安全技术与形式化方法的发展

本章小结

本章习题

第2章离散数学基础知识

2.1数理逻辑

2,1.1命题逻辑与安全断言

2.1.2命题逻辑的推理理论

2.1.3一阶逻辑

2.1.4时序逻辑与高阶逻辑

2.2集合论

2.2.1集合代数

2.2.2二元关系与函数

2.3代数结构

2.3.1代数系统

2.3.2群、环与格

2.4图论

2.4.1图的基本概念

2.4.2树

本章小结

本章习题

第3章密码学基础知识

3.1密码基本理论与技术概述

I3.1.1密码学相关术语的定义

3.1.2两类加密算法

3.2对称密码

3.2.1流密码

3.2.2分组密码

3.3公钥密码体制。

3.3.1公钥密码体制的基本概念

3.3.2 RSA密码机制。.

3.3.3基于身份的密码机制

椭圆曲线密码机制

3.3.5无证书密码机制-..

3.4 Hash 函数

3.4.1 Hash函数用来提供认证的基本使用方式

3,4.2 Hash函数应满足的条件

3,4,3第工类生日攻击

3.4.4第1类生日攻击

3.5数字签名

3.5.1数字签名算法

3.5.2椭圆曲线数字签名算法

3.5.3代理签名算法

3.5.4聚合签名算法

3.5.5多重签名算法

本章小结

本章习题

第4章协议工程与软件工程基础知识

4.1协议工程.......

4.1.1协议设计原理

4.1.2协议安全..

4,1,3协议验证技术

4.2软件工程.....

4.2.1软件生命周期

4.2.2软件安全

4.2.3软件验证技术

本章小结

本章习题.

第二单元形式化安全分析方法

第5章基于演绎推理的形式化安全方法

5.1 BAN逻辑

5.1.1 BAN逻辑的定义

5.1.2形式化描述

5.1.3形式化的协议验证目标

5.2 GNY逻辑

5.2.1基本术语

5.2,2推理规则

5.3 SVO 逻辑

5.3.1 SVO逻辑的语法

5.3.2 SVO逻辑推理公理

……

7.5.1 ProVerif

7.5.2 Tamarin

7.6实例分析与实验

7.6.1使用 Tamarin验证 Diffie Hellman协议

7.6.2使用ProVerif分析5G-AKA协议

本章小结

本章习题

第三单元形式化安全方法的综合应用

第8章通信软件安全性的形式化验证实例

8.1通信软件的形式化安全验证流程

8.1.1通信软件设计的安全性验证流程

8.1.2通信软件代码的安全性验证流程

8.2通信软件形式化安全验证实例

8.2.1分析对象

8.2.2 CHAP软件设计安全性验证

8.2.3 CHAP软件代码一致性验证

本章小结

参考文献

本书共分为三个单元。第一单元(第1-4章)主要介绍网络协议形式化安全分析方法的相关基础知识，包括绪论、离散数学基础知识、密码学基础知识、协议工程与软件工程基础知识等内容，明确了采用形式化方法对计算机系统中网络协议和软件的安全性进行分析的主要步骤，以及形式化安全方法发展的历史和趋势。第二单元(第5-7章)主要介绍现有的网络协议形式化安全分析方法，系统地讲解了相关方法在确保通信协议和软件实现的安全性方面的关键应用，包括基于演绎推理和自动机模型的形式化安全方法和基于进程演算的形式化方法。第三单元(第8章)主要介绍通信软件安全性的形式化验证实例，展示形式化方法在实际安全应用中的具体实施和效果。