网络安全协议的形式化分析与验证课件绪论

信息在开放网络环境中传输遭受到的攻击：

偷听攻击 截取攻击 伪造攻击 篡改攻击 …

网络安全直接关系到信息系统安全，是整个信息 基础结构的安全基础。

维护网络环境安全的技术：


密码技术：主要功能是提供安全的服务，通过使用密码 算法对消息明文进行加密以保证消息本身的安全从而保 证通信过程的安全可靠。 安全协议：是一个分布式算法，它规定了两个或多个通 信主体的安全性。安全协议利用密码技术实现开放网络 环境下的安全通信，达到信息安全的目的，广泛地应用 于身份认证、接入控制和密钥分配等领域。





3.完整性 含义：通常是指数据不能被篡改，或者至少针对数据的任 何篡改都能被检测出来。 目的：保护消息不被未授权地篡改、删除或替代。可以理 解为在储存的数据上再加上一层防止篡改的保护层。 常用方法：封装和签名。




4.不可否认性 含义：不可否认性主要是考虑如何保护通信的一方不被对方 欺骗，在协议执行过程中能够为用户提供证据，来证明协议 中某些步骤确实发生过，而且这些证据是不可伪造的。 不可否认性是电子商务协议的一个重要性质，是保证交易正 常进行的必要条件。 保证不可否认性最常用的技术是数字签名。
第一章
安全协议概述 形式化技术基础
绪 论
形式化方法在安全协议验证中的应用
小结
1.1

安全协议概述
安全协议的基本概念 安全协议的缺陷分析 安全协议的攻击手段 形式化分析方法的重要性
1.1


安全协议概述
信息安全最基本的目标:
实现信息的机密性 保证数据的完整性 实现身份或信息的鉴别性和不可抵赖性 对信息的授权和访问控制 保证信息资源的可用性 …


6.匿名性
含义：匿名性是指保证消息接收者不知道发送者的身份。 直观上看，一个在某个事件集 E 匿名的系统将拥有的特性为： 当事件集E中的一个事件发生时，从观察者的角度看，即使他可 以推断出发生了事件集E中的一个事件，他也不能确定是哪个事 件。
一个安全协议需要提供的特性和服务只是以上安全 属性集的子集，这取决于其具体的应用环境。 不存在“绝对安全”、“绝对正确”的安全协议。


只是在某些假设环境中，对某几类特定的威胁是安全的。
几类重要的安全属性:


1.保密性 含义：保密性是指入侵者无法发现合法用户的任何活 动。换言之，系统中高级用户的活动不会对系统的低 级用户或外部观察者产生任何明显的影响。（严格） 保护消息在传输过程中不会泄露给非授权拥有此 消息的人（对大多数应用而言） 方法：实现安全协议保密性的最直接方法是对机密信 息进行加密。

安全协议研究和设计的现状：


安全协议作为实现信息安全的基础，其自身的安全性问 题已成为安全研究的重要内容。目前，针对安全协议的 安全性验证已形成了许多不同的流派、理论和方法。 安全协议的设计是一项非常复杂而困难的工作，许多在 设计时被认为是安全的协议，后来都被发现存在安全漏 洞，而且采用不同的分析方法和工具，可能发现的漏洞 也不大一样。因此，安全协议的设计越来越受到关注。
密码协议的安全属性（Security
Attributes）集（目标集
合）:



认证性（Authenticity） 保密性（Secrecy） 完整性（Integrity） 不可否认性（Non-Repudiation） 公平性（Fairness） 匿名性（Anonymity） 可用性（Usability） 可追究性（Accountability） 原子性（Atomicity） 。。。

安全协议的形式化方法现状:


已经具备了比较完整的理论体系和模型，但目前对安 全协议的分析和设计大都使用人工完成，效率低，更 重要的是会人为地带入一些误差，造成安全协议的分 析设计结果可信度降低，甚至导致失败。 自动化的协议分析和设计工具逐渐成为协议研究的另 一个重要领域。目前已经开发实现了一些安全协议自 动化分析设计工具，比较常用的工具有NRL协议分析器、 认证协议自动分析器（Automatic Authentication Protocol Analyzer，AAPA）等。





2.认证性 认证性是最重要的安全性质之一，所有其他安全性质的 实现都依赖于此性质的实现。 含义：认证是一个过程，通过这个过程，一个主体向另 一个主体证明某种声称的性质。 可细化为：消息源认证、实体认证、认证的密钥建立。
பைடு நூலகம்息源认证是指消息的接收者能验证消息所声称的源地址 是其真正发出的地址，并进一步确认发出消息的时间值没 被篡改过； 实体认证用于验证主体身份的真实性，即验证某个主体声 称的身份是否与其真实身份一致。数据源认证机制是实现 实体认证的一种有效方法。 认证的密钥建立通常与实体认证过程密切相关。主体间进 行实体认证的目的在于能够进行安全通信，而密钥是安全 信道的基础，所以在主体进行安全通信之前，通常也需要 密钥建立过程（也称为密钥交换或密钥协商）。

密码学变换算法从数学上提供了达到一定程度的通信安全的基本 机制。 目标：通过正确使用加解密技术来解决网络通信的安全问题。如 实现信息的机密性、保证数据的完整性、实现身份或信息的鉴别 性、具有不可抵赖性、对信息的授权和访问控制以及保证信息资 源的可用性等。

密码协议：使用密码学技术的网络安全协议。



5．公平性
目的：公平的目的在于确保协议参与各方的地位和作用平等， 参与各方所拥有的能力也是相同的。 含义：对公平性可以直观地理解为在协议运行的任何时刻每一 个参与者都不会得到特别的好处。或者说，没有一方可以得到 自己要的证据却可以避免另一方得到相应的证据。 应用：公平性常被用于电子商务、电子选举和电子投票事务当 中。
1.1.1

安全协议的基本概念
协议的定义：指两个或者两个以上的参与者为完成 某项特定的任务而采取的一系列步骤。 包含三层含义：

协议自始至终是有序的过程，每一个步骤必须执行，在 前一步没有执行完之前，后面的步骤不可能执行。 协议至少需要两个参与者。 通过协议必须能够完成某项任务。

安全协议：安全协议是由参与通信的各方按确定的步骤做 出一定的通信动作完成的，这些通信动作实现了通信本身， 而动作的内容则隐含了一些密码学变换算法的实施。