网络安全协议的形式化分析与验证

出版说明

前言

第1章绪论

1.1安全协议概述

1.1.1安全协议的基本概念

1.1.2安全协议的缺陷分析

1.1.3安全协议的攻击手段

1.1.4安全协议形式化方法的必要性

1.2形式化技术基础

1.2.1模态逻辑技术

1.2.2模型检测技术

1.2.3定理证明技术

1.3形式化方法在安全协议验证中的应用

1.3.1安全协议形式化理论发展现状

1.3.2安全协议形式化方法发展趋势

1.4本章小结

1.5习题

第2章基于模态逻辑技术的安全协议分析方法

2.1BAN逻辑

2.1.1基本术语

2.1.2推理规则

2.1.3应用实例

2.2类BAN逻辑

2.2.1GNY逻辑

2.2.2AT逻辑

2.2.3SVO逻辑

2.2.4Kailar逻辑

2.3Bieber逻辑

2.3.1历史模型

2.3.2KT5逻辑

2.3.3CKT5通信逻辑

2.3.4消息的解释

2.3.5认证与保密

2.4非单调逻辑

2.4.1安全协议的Nonmonotomic逻辑描述

2.4.2安全协议的Nonmonotomic逻辑分析

2.5本章小结

2.6习题

第3章基于模型检测技术的安全协议分析方法

3.1Dolev-Yao模型

3.2通信进程方法

3.2.1CSP的基本概念

3.2.2CSP的网络模型

3.2.3协议安全性质的CSP描述

3.2.4CSP协议分析

3.3NRL协议分析器

3.3.1协议描述

3.3.2协议分析

3.3.3实例

3.4模型检测工具Murφ

3.4.1Murφ系统

3.4.2Murφ协议分析过程

3.4.3Murφ协议分析实例

3.5模型检测工具ASTAL

3.6协议分析工具BRUTUS

3.6.1BRUTUS协议描述模型

3.6.2BRUTUS协议属性逻辑

3.6.3BRUTUS协议验证算法

3.6.4BRUTUS协议分析实例

3.7本章小结

3.8习题

第4章基于定理证明的安全协议分析方法

4.1Paulson归纳法

4.1.1Paulson归纳法简介

4.1.2Paulson归纳法的自动化理论

4.1.3Paulson归纳法协议分析示例

4.2Schneider阶函数

4.2.1阶函数的定义

4.2.2阶函数定理

4.2.3协议分析实例

4.2.4基于阶函数的自动化验证技术

4.3串空间

4.3.1基本概念

4.3.2协议入侵者描述

4.3.3安全属性的表示

4.3.4协议分析举例

4.3.5认证测试方法

4.4重写逼近法

4.4.1预备知识

4.4.2逼近技术

4.4.3对NS公钥协议的描述与分析

4.5不变式产生技术

4.5.1基本概念

4.5.2描述攻击者不可知项集合的不变式

4.5.3描述攻击者可知项集合的不变式

4.6本章小结

4.7习题

第5章安全协议的形式化设计方法

5.1合成协议模型及其安全性

5.1.1HT模型

5.1.2协议的组合

5.2Fail-stop协议

5.2.1Fail-Stop协议及其分析

5.2.2复杂协议

5.3BSW简单逻辑

5.3.1模型

5.3.2逻辑

5.4本章小结

5.5习题

第6章Internet密钥交换协议及其分析

6.1Internet密钥交换协议概述

6.1.1阶段1主模式交换

6.1.2阶段1野蛮模式交换

6.1.3阶段2快速模式交换

6.2IKE协议的形式化分析

6.2.1采用NRL协议分析器进行形式化分析

6.2.2利用扩展BSW逻辑分析

6.3IKEv2协议概述

6.3.1IKEv2密钥交换

6.3.2密钥算法协商

6.3.3加密密钥与认证密钥

6.4IKEV2协议的形式化分析

6.4.1扩展串空间理论

6.4.2IKEv2协议分析

6.5本章小结

6.6习题

第7章电子商务安全协议及其分析

7.1早期的电子商务安全协议

7.1.1Digicash协议

7.1.2FirstVirtual协议

7.1.3Netbill协议

7.2SSL协议及其分析

7.2.1SSL协议介绍

7.2.2SSL协议的形式化分析

7.3SET协议及其分析

7.3.1SET协议的流程

7.3.2双重签名技术

7.3.3数字信封

7.3.4SET协议的形式化分析

7.4本章小结

7.5习题

第8章移动通信安全协议及其分析

8.1移动通信安全协议

8.1.1第1代移动通信安全协议

8.1.2第2代移动通信安全协议

8.1.3第3代移动通信安全协议

8.2AUTLOG认证逻辑对AKA协议的分析

8.2.1AUTLOG认证逻辑

8.2.2协议的形式化描述

8.2.3假设前提

8.2.4协议目标

8.2.5形式化证明

8.3利用认证测试方法对3GPP-AKA协议进行安全性分析

8.3.1移动用户与移动核心网之间的安全性验证

8.3.2服务网络基站与移动核心网之间的安全性验证

8.3.3服务网络基站与移动用户之间的安全性验证

8.4本章小结

8.5习题

第9章群组通信安全协议及其分析

9.1群组通信概述

9.2群组密钥管理协议

9.3密钥管理方案

9.3.1集中式密钥管理方案

9.3.2分布式密钥分发方案

9.3.3分担式密钥协商方案

9.4群组密钥交换协议的形式化描述及安全性分析

9.4.1AT-GDH协议

9.4.2AT-GDH2协议

9.4.3AT-GDH3协议

9.5本章小结

9.6习题

参考文献

　　本书概述了形式化技术在网络安全协议分析、验证中的主要应用原理及现状；在此基础上详细地叙述了网络安全协议的形式化分析技术、形式化设计技术；最后重点介绍了目前的形式化分析技术对当前典型应用环境下复杂、实用网络安全协议的分析成果。本书可作为信息安全专业高年级本科生教材，也可作为高等学校电子信息类、计算机类等相关专业的参考书。　　信息安全是关系到国家安全和经济发展的重大战略问题，至关重要。安全协议作为实现信息安全的基础，其自身的安全性问题已成为安全研究的重要内容。目前，针对安全协议的安全性验证已形成了许多不同的流派、理论和方法。本书概述了形式化技术在网络安全协议分析、验证中的主要应用原理及现状；在此基础上详细地叙述了网络安全协议的形式化分析技术、形式化设计技术；最后重点介绍了目前的形式化分析技术对当前典型应用环境下复杂、实用网络安全协议的分析成果，包括IPSec协议、SSL协议、电子商务协议、移动通信安全协议及群组通信安全协议等。本书理论与应用并重，深入浅出地介绍了各类形式化分析技术的基本原理及其在大型复杂安全协议分析中的实际应用。　　本书可作为信息安全专业高年级本科生教材，也可作为高等学校电子信息类、计算机类等相关专业的参考书。