复习《Internet安全协议与分析》。
[TOC]
CH1:无线通信系统安全
网络与因特网
网络连接许多计算机,因特网连接许多网络。
发展阶段
- 单个网络ARPANET向互联网发展:1983年TCP/IP协议成为ARPANET上的标准协议。
- 建成了三级结构的因特网:主干网、地区网和校园网(企业网)。
- 形成了多层次ISP(Internet Service Provider)结构的因特网。
组成
- 边缘部分:所有连接在因特网上的主机组成。这部分是用户直接使用,用于通信和资源共享。
- 核心部分:由大量网络和连接这些网络的路由器组成,为边缘部分提供服务(连通性和交换)。
协议体系结构
- 应用层
- 运输层
- 网络层
- 数据链路层
- 物理层
无线通信安全历史
移动通信
- 第一代:几乎没有采取安全措施
- 第二代:基于私钥密码体制的安全机制,通过系统对用户进行鉴权来防止非法用户使用网络,通过加密技术防止对无线信道进行窃听,但在身份认证及加密算法等方面存在着许多安全隐患
- 第三代:三个层面、五个安全域上提供安全措施。
无线局域网标准
IEEE 802.11 802.11b 802.11i
无线通信网的主要安全威胁
四个概念
- 无线终端:移动台/移动终端
- 无线接入点:移动通信中指基站,无线局域网中指无线路由器,负责接收和发送无线信号。
- 网络基础设施:满足通信基本要求的各种硬件与服务的总称。移动通信系统中主要是指包括基站、交换机在内的基本通信设备及其软件。
- 空中接口:无线终端和无线接入点之间的接口,移动通信系统中“移动性”的集中体现。
三个威胁
- 对传递信息的威胁:针对系统中传输的个人消息
- 侦听:非授权方可能获悉传输或存储在系统中的信息。
- 篡改:非授权方更改系统中的各种信息。(非法修改和重放)
- 抵赖:参与通信的一方否认或部分否认他的行为。(接受抵赖和源发抵赖)
- 对用户的威胁:针对系统中用户的一般行为
- 流量分析:指分析网络中的通信流量。
- 防止方法::对消息内容和可能的控制信息进行加密。(如果采用低级别(链路之间)加密通信,也可以采用其他模式进行统计分析,因此可以采用类似消息填充和插入虚假消息等作为加密措施的补充)
- 监视:监视一个特殊用户的行为。
- 防止方法:使用假名来实现匿名发送、接受和计费。
- 流量分析:指分析网络中的通信流量。
- 对通信系统的威胁:破坏整个系统的完整或功能
- 拒绝服务:系统内外的非法攻击者故以削弱系统的服务能力或使系统无法提供服务。
- 资源的非授权使用:使用禁用资源或越权使用无线信道、设备、服务或系统数据库邓系统资源。
- 越权使用资源:用户允许使用一些资源,但访问的资源超越了权限范围。
移动通信系统的安全需求
- 能唯一标识用户
- 冒充合法用户是困难的
- 信令、传输数据和身份等信息应是保密的
- 双向认证:合法的用户、信任的网络和服务提供商。
- 机密性:用户和网络服务器之间需协商会话密钥用于消息加密。密钥协商通常是认证过程的最后部分,为了增强安全性,每次通信的会话密钥必须不同。
- 用户身份的匿名性
- 不可否认性
- 完整性:消息和业务的完整性
- 新鲜性:防重传攻击的重要手段,时间戳、随机数、计数器
- 公平性
- 端到端保密
- 合法的监视
- 调度功能:
- 认证
- 通信的机密性
- 通信的完整性
移动通信系统的安全体系
系统的任何一个安全措施都可以映射成这个三维空间的一个点,可以解释为每个安全措施都是在某个安全域内,为满足某个层次上的安全需求而提供的某种安全服务。
安全服务
- 认证和密钥管理服务
- 在移动终端接入网络或一次通话开始时鉴权;认证服务包括用户和网络之间鉴权、网络实体间的认证以及在终端内安全服务模块和终端的认证。
- 密钥管理是产生、分发、选择、删除、和管理在鉴权和加解密过程中使用的密钥的过程
- 访问控制服务:防止对任何资源进行非授权访问
- 完整性服务
- 机密性服务
- 不可否认性服务
安全需求
- 管理层:对安全威胁的管理和制定合理的管理标准
- 用户层:提供事务处理的端到端安全
- 控制层:负责网络过程。
- 链路层:保证数据在无线电线路上传输的正确性和安全性。
- 物理层:由定时结构、无线电射频发射和接收等部分组成。
安全域
- 网络接入域安全:安全接入服务
- 网络域安全:网络实体间的认证、数据传输机密性和完整性、攻击信息的监视等
- 用户域安全:主要提供终端安全服务模块域用户间的认证以及终端安全服务模块域移动终端间的认证。
移动通信系统安全
GSM系统
GSM系统主要由移动终端( MS )、基站子系统 (BSS )、网络子系统(NSS )、介于操作人员与系统设备之间的操作与维护子系统 (OSS )和各子系统之间的接口共同组成。
GSM系统的安全目标
- 防止未经授权的用户接入网络:通过鉴权机制
- 用户身份认证
- 用户的隐私权保护:通过加解密技术
- 数据机密性
- 用户身份(IMSI,国际移动用户标识)保密
GSM系统的安全实体
- SIM
- GSM手机和基站
- GSM网络子系统
GSM系统的鉴权过程
- GSM网络侧从业务请求提取TMSI或IMSI,并查看是否保存有认证向量三元组triplet(RAND,XRES,Kc),有则可以直接给MS发送RAND作为挑战信息,否则继续。
- VLR向鉴权中心AuC发送认证数据请求,其中包含用户的IMSI。
- 认证中心根据用户的IMSI找到用户的密钥Ki,然后利用自己产生的随机数RAND,利用A3算法,产生预期响应XRES,利用A8算法产生用于加密的密钥Kc,即产生认证向量三元组:triplet(RAND,XRES,Kc),发送到MSC/VLR;
- MSC/VLR将其中的RAND发送给MS,MS中的SIM卡根据收到的RAND和存储在卡中的Ki,利用A3和A8算法分别计算出用于认证的响应RES和用于加密的密钥(Kc),并将RES回送到MSC/VLR中;
- 在MSC/VLR里,比较来自MS的RES和来自认证中心的XRES,若不同,则认证失败,拒绝用户接入网络;若相同,则认证成功,用户可以访问网络服务,并且在后续的通信过程中,用户和基站之间无线链路的通信利用加密密钥Kc和A5算法进行加密。
GSM系统的加密机制
被加密数据包括信令消息、业务信道上的用户数据和信令信道上无连接的用户数据。
这一机制涉及 4 种网络功能:加密方法协商、密钥设置、加解密过程的发起、加/解密的同步。加密算法采用流密码 A5 算法,待加密数据和 A5 的输出逐比特异或。
GSM系统的匿名机制
- 为保证用户身份的机密性,对用户的鉴权成功之后,网络为用户分配临时移动用户标识 TMSI 来替代国际移动用户标识 IMSI ,使第三方无法在无线信道上跟踪 GSM 用户。
GSM系统的安全性分析
- 安全算法方面:算法安全性未经公众验证。 A3/A8 算法易受到选择质询( chosen challenge )攻击 A5 语音保密算法被已知明文攻击攻破。
- 安全机制设计方面:只在空中接口实施了单项鉴权和加密,在固定网内没有定义安全功能,攻击者如果在固定网窃取认证向量三元组,就可以冒充网络单元。
- 系统对用户进行 单向实体认证 ,很难防止中间人攻击和假基站攻击
- 获取正常基站的GSM频率后,使用该GSM频率并以更高功率伪装诱骗连接。
- GSM 系统本身不提供端到端的加密;
- 用户数据和信令数据缺乏完整性保护机制。
3G系统
3G系统实体
- 移动终端
- ME :移动设备 Mobile Equipment
- USIM :全球用户识别模块 Universal Subscriber Identity Module
- 无线接入系统:UTRAN、GERAN
- 核心网:分组交换域PS、电路交换域CS
3G安全架构
特点:
- 基于IP网络
- 非话音服务的多样性和重要性
- 将增强用户服务范围的控制和对其终端能力的控制
- 存在对用户的主动攻击
- 终端将用作电子商务应用和其它应用的平台
安全域:
- 接入域
- 网络域
- 用户域
- 应用域:用户域服务提供商在应用层面安全交换数据。
- 安全的可视性和可配置性:使用户知道网络的安全性服务是否在运行,以及它所使用的服务是否安全。
LTE网络
由UE、E-UTRAN、EPC三部分构成
LTE的网络从空口无线侧开始就是 IP 网络,同时智能终端只要开启电源就会附着 IP 地址,因而智能终端、 LTE 无线接入侧、传输网侧和 EPC 都面临着原来 IP 网络固有的安全威胁:
- 无线侧智能终端面临僵木蠕、恶意代码等攻击;
- 无线智能侧终端成为 DDoS 攻击源对整个 LTE EPS 网络发起 DDoS 攻击;
- EPC 核心网元面临信令风暴问题;
- 智能终端通过 LTE EPC 、 Internet 等非信任网络时进行明文传输敏感数据时,面临泄露数据的问题;
- LTE EPS 综合业务平台面临攻击的威胁;
- EPC Pi 口 (P GW<—> 面临来自 Internet 攻击的威胁;
无线局域网安全(WLAN)
基于IEEE802.11协议的无线局域网分为基础结构(infrastructrue)模式和自组织(ad-hoc)模式
基础结构模式网络结构由AP(固定接入点)和STA(无线设备)组成。
无线局域网关联过程
AP以固定的时间间隔(通常为每秒钟10次)发送信标,它们能使无线设备发现AP的标识。STA初始化后,开始寻找AP。STA会依次调谐到每个无线频段(称为信道)上,并收听信标消息。这个过程称为扫描。
- STA->AP 认证请求
- AP->STA 认证响应
- STA->AP 关联请求
- AP->STA 关联响应
三种消息:
- 控制
- 管理
- 数据
IEEE802.11 认证
开放系统认证(默认认证机制)
整个认证过程以明文形式进行,包括认证请求和响应
共享密钥认证
响应工作站根据当前请求工作站是否拥有合法的密钥来决定是否允许接入,但不要求在空中接口传送这个密钥。
- 请求工作站->响应工作站 请求认证
- 响应工作站->请求工作站 随机质询文本
- 请求工作站->响应工作站 共享密钥加密文本
IEEE802.11 加密
802.11 定义了 WEP Wired Equivalent Privacy )来为无线通信提供和有线网络相近的安全性来有效的防止窃听。
WEP基于RC4算法,必须在每帧重新初始化密钥流,需要引入IV和ICV。
加密过程
解密过程
WEP的分析
认证及其弱点
IEEE802.11认证手段不能有效实现认证目的,且是单向认证,伪装AP的攻击很容易实现(会话劫持和中间人攻击)
- 开放系统认证:空认证
- 共享密钥认证:一旦攻击者得到密钥流,就可以完成认证
- 服务组标识符SSID:SSID是用来逻辑分割无线网络,以防止一个工作站意外连接到邻居AP 上,它并不是为提供网络认证服务而设计的。一明文形式传送,不提供用户认证。
- MAC地址控制:迫使只有注册了MAC的工作站才能连接到AP上,但用户可以重新配置无线网卡的MAC地址,并不能阻止非授权用户访问。
完整性分析
- ICV采用CRC-32实现,只用来检查随即错误,不具备身份认证能力;且CRC-32对异或运算是线性的,不能抵御对明文的篡改。
- WEP的完整性保护只应用于数据载荷,而不保护地址以及防止重放等。
机密性分析
- 弱密钥问题:RC4算法密钥空间存在大量弱密钥
- 静态共享密钥和IV空间:没有密钥管理方法,使用静态共享密钥;IV管理很困难,易重用。
IEEE802.11安全问题
- 认证协议简单且为单向认证
- 完整性算法CRC-32不能阻止攻击者篡改数据
- WEP不能抵抗重放攻击
- IV和Share Key级联在RC4算法下容易产生弱密钥
- IV易发生重用冲突
移动自组网络安全(Ad Hoc)
AdHoc网络中的每个移动终端兼备路由器和主机两种功能:
- 主机需要运行面向用户的应用程序;
- 路由器需要运行相应的路由协议,根据路由策略和路由表参与分组转发和路由维护工作。
Ad Hoc 网络节点间的路由通常由多个网段(跳)组成,由于终端的无线传输范围有限,两个无法直接通信的终端节点往往要通过多个中间节点的转发来实现通信。
移动Ad Hoc网络的特点
- 网络的自组织性
- 动态的网络拓扑
- 多跳的通信路由
- 有限的无线通信带宽
- 有限的主机能源
- 网络的分布式特点
- 安全性较差
移动Ad Hoc网络的安全弱点
- 传输信道:采用无线信号作为传输媒介,容易被窃听/干扰;
- 移动节点:节点是自主移动的,安全性比较脆弱;
- 动态拓扑:节点位置不固定,网络拓扑不断变化;
- 路由协议:路由协议假定了所有节点相互合作。
移动Ad Hoc网络的密钥管理
- 部分分布的CA:每个节点拥有证书签名密钥的一部分,可产生部分证书,但只有组合k个才能得到有效证书。
- 自安全方案:CA功能完全分布到系统每个节点。
移动Ad Hoc网络的安全路由
移动Ad Hoc网络不能采用常规路由协议,因为:
- 主机间的无线信道可能存在单向信道
- 动态变化的拓扑结构
- 有限的无线传输带宽
- 无线移动终端的局限性
Ad Hoc网络的拓扑结构主要有平面结构和分级结构两种,协议也划分为平面结构的路由协议和分簇式路由协议。
针对Ad Hoc网络路由协议的攻击
路由破坏攻击
- 篡改
- 删除
- 虫洞
- 伪造路由错误
- rushing
资源消耗攻击
- Dos
- 伪造路由发现
- 路由表溢出
Ad Hoc网络路由协议的特点
- 协议能够抵抗单攻击者的安全威胁,对于联合攻击如Worm hole无法抵抗
- 协议强调了安全性而忽视了可用性,节点算力弱,电池和通信带宽有限
- 屏蔽了路由协议的某些功能,降低了路由协议的有效性
- 有的协议要求网络中存在集中服务器,有单点失效的风险
Ad Hoc网络的入侵检测
- 无公信结点集中控制节点的认证
- 没有集中网络流量的节点,无法集中监控
- 正常节点和恶意节点的行为区别不明显
- 资源和带宽有限
无线传感器网络(WSN)
WSN系统包括传感器节点、汇聚节点(基站/网关)和管理节点。
- 传感器节点随机部署在监测区域内部或附近,通过自组织方式构成网络,用于收集数据,并且将数据路由至汇聚节点;
- 汇聚节点与管理节点通过广域网络(如Internet网络、移动通信网络或者卫星网络等)或直接进行通信,从而将收集到的数据传送到管理节点;
- 用户通过管理节点对传感器网络进行配置和管理、发布监测任务以及收集监测数据。
WSN的特点
- 无控制中心
- 自组织性
- 动态拓扑
- 多跳路由
- 节点数量大、分布广
- 与应用相关的网络
- 资源有限
WSN面临的安全威胁和措施
物理层
信号干扰/阻塞
扩频通信
窃听
加密敏感信息
节点被俘
实行篡改证明,但成本较高,WSN中不用。
数据链路层
碰撞
使用纠错码
资源耗尽
对MAC访问许可进行控制;时分复用;邻居节点监视反常行为
不公平访问(弱Dos)
网络层
仿冒节点
网络各节点之间相互认证
虫洞
HELLO洪泛:以能量足够大的信号广播,使节点认为攻击者使直接邻居,导致网络混乱
建立对密钥,以便任意两个邻居节点相互验证;利用基站检查节点身份和邻居关系
确认欺骗:使发送者相信一条差链路
虚假路由
选择性转发
使用多条路径同时发送或采取协议检测恶意节点
槽洞(sinkhole):尽可能地引诱一个区域中的流量通过恶意节点
采用随机密钥预分配机制和基站入侵检测与响应
女巫(Sybil):位于某个位置的单个恶意节点不断的声明其有多重身份(如多个位置等),使得它在其它节点面前具有多个不同的身份。
建立对密钥,以便任意两个邻居节点相互验证
传输层
- 洪泛:当需要一个协议来维护一个连接两端的状态时,通过洪泛攻击可以使内存很快耗尽。攻击者可能重复建立新的连接请求直到每个连接需要的资源耗尽或达到上限。无论是哪种情况,接下来的合法请求都会被拒绝。
- 分离式同步:是指中断一个已有的连接。比如,攻击者可能重复地对一个终端主机发送欺骗信息而引起主机要求重发丢失的包。如果时间恰当,攻击者就能够降低甚至阻止终端主机成功交换数据,因此,发送端将不断地试图恢复实际并不存在的错误而无法进行正常的通信。
应用层
CH2:安全协议概述
安全协议
- 协议:两个或以上的参与者采取一系列步骤已完成某项特定的任务
- 安全协议:密码体制基础上的一种高互通协议
安全协议常见类型
- 密钥交换协议:用于完成会话密钥的建立
- 认证协议:实体、身份、数据源、消息。用来防止篡改、假冒、否认等攻击
- 认证和密钥交换协议:互联网密钥交换协议IKE、分布认证安全服务DASS、Kerberos认证协议等
- 电子商务协议:协议双方存在利益矛盾,需要保证公平。电子商务SET协议
安全协议系统模型
- 环境定义
- 系统环境:消息的发送和接收者、攻击者(恶意网络环境)、管理消息发送和接收的规则
- 恶意网络环境:攻击者
- 攻击者操作:截取、重放、篡改、级联、分离、加密、解密
- 被动攻击者:知晓信息
- 主动攻击者:操纵信息
- 攻击行为
- 转发消息到特定接收者处
- 延迟消息的送达
- 篡改后转发
- 合并消息
- 改变部分或全部消息的去处
- 重放消息
安全协议的性质及实现
目的通过协议消息的传递来达成通信主体身份的识别与认证,并在此基础上为下一步的秘密通信分配所使用的会话密钥
认证性实现
通过共享秘密实现:可以对抗假冒攻击,确保身份
- 声称者用仅他和验证者知道的密钥封装消息
- 声称者用私钥签名,验证者用公钥验证签名
- 声称者通过可信第三方证明自己
秘密性实现
- 目的:保护协议消息不泄露;攻击者无法根据消息格式提炼消息
- 实现方法:对消息明文加密
完整性实现
- 目的:保护协议消息不被非法篡改、删除和替代
- 实现方法:封装和签名
- 不可否认性实现
- 目的:通过通信主体提供对方参与协议交换的证据来保证合法利益不受侵害
- 实现方法:签名消息
- 协议特点:证据的正确性,交易的公平性。 次要:适时中止性、可追究性
协议设计准则
消息独立完整性原则:一条消息的解释应完全由该条消息的内容决定,不必借助上下文推断
常用的协议消息描述格式:
<序列号>发送者标识->接收者标识:消息
<2>A->B:m m应包含A、B的标识,否则易造成攻击
消息前提准确原则:与消息的执行相关的先决前提条件应当明确指出,且正确性和合理性能够验证,由此判断消息是否应当被接收,即每条消息所基于的假设是否能够成立。
- 主体身份标识原则:主体标识重要时应在消息中明确附上主体名称
- 显式:明文主体名字
- 隐式:加密或签名
- 加密目的原则:加密可实现多种安全目的(秘密性、完整性、认证性),使用加密算法前确定目的
- 签名原则:主体对加密消息签名并不表明主题知道加密消息的内容,如果主体先签名再加密,则表明主体知道消息内容。同时使用加密和签名时,应先签名后加密。
- 随机数的使用原则:使用随机数的目的是提供消息的新鲜性。关键问题是随机数的真正随机性。
- 时戳的使用原则:考虑各机器的时钟与当地标准时间的差异,时戳的使用主要依赖于时钟同步。
- 编码原则:明确指出具体的编码格式
安全协议缺陷分类
- 基本协议缺陷:设计时很少考虑攻击者
- 口令/密钥猜测缺陷
- 可检测的口令在线猜测攻击:不成功的登录能被检测并记录
- 不可检测的口令在线猜测攻击:攻击者从响应中逐渐推导出正确的口令
- 可离线的口令猜测攻击:攻击者使用认证协议消息附件,猜测口令并离线验证
- 改进措施:只响应新鲜的请求;只响应可验证的真实性。
- 陈旧消息缺陷:消息的新鲜性——消息重放攻击
- 并行会话缺陷:攻击者通过交换一定的协议消息获得重要的消息
- 内部协议缺陷:协议参与者中至少有一方不能完成所有必须的动作
- 密码系统缺陷:密码算法的安全强度问题
消息重放攻击及对策
攻击利用其消息再生能力生成诚实用户所期望的消息格式并重放,分为本协议的轮内攻击和轮外攻击。
消息去向:发送方——反射攻击;第三方——第三方攻击;接收方但被延迟——直接攻击
对策:
序列号机制——接收方通过比较消息中的序列号以判断消息是新产生的还是重放的
问题:开销增大,小型系统适用
挑战-应答机制——消息的时间变量参数由接收方在该消息传递前明确地向消息发送方说明
问题:系统开销增加
时戳机制——当消息上地时戳与本地时间差值在一定范围内才有效
问题:需要全局时钟,但仍难以同步
CH3:IPSec协议
IP安全问题
IP协议从本质上来说是不安全的,修改IP包重新计算校验和很容易。
IPv4没有安全选项,缺乏通信双方真实身份验证、数据完整性和机密性保护……
IPSec
IPSec随着IPv6产生,有三种机制共同保障:认证、信息机密性和密钥管理
IPSec 提供访问控制、无连接完整性、数据源鉴别、载荷机密性和有限流量机密等安全服务。
IPSec体系结构
安全联盟SA
SA是两个通信实体间建立的一个简单单向协定,由安全参数索引SPI和目标地址组成,单个IPSec连接至少需要两个SA。
安全策略库SPD
用于提供安全策略配置,其中的动作指定某些数据流必须绕过IPSec的处理、某些丢弃、其余的必须经过IPSec模块的处理。
含有规则列表:
- Traffic Selectors: IP addresses and/or ports, protocol;
- Actions: Discard; Bypass IPsec; Apply IPsec
安全关联数据库SAD
包含了所有活跃SA的所有参数信息。
流出数据由SPD数据项包含指向某SAD数据项的指针,决定数据包使用的SA。
流入数据由SAD决定如何对数据包做处理。
认证头AH
为IP通信提供数据源认证,数据完整性和反重播保证,可防篡改,不防窃听,无机密性保护
原理:在每一个数据包上添加身份验证报头,包含一个带密钥的hash散列,提供完整性保护。
AH传输模式
AH被插在原始IP头之后但在所有的传输层协议或其他IPSec协议头之前 。
使用原始的明文IP头,安全信息在AH中,可以保证整个IP包不被修改。
AH在传输模式下和NAT是冲突的,因为NAT会修改源/目的IP地址。
AH隧道模式
AH插在原始IP头之前,共同作为IP数据部分。加密整个IP数据报,用自己的地址作为源地址加入新的IP头。
验证整个IP包,AH在隧道模式下也与NAT冲突。
封装安全载荷ESP
ESP是插入IP数据包内的一个协议头,提供机密性、数据源认证、抗重播以及数据完整性等安全服务。
ESP将保护数据加密后封装在IP包中。也提供认证服务。
ESP总是先使用,AH头在最外层
ESP传输模式与隧道模式
ESP在传输模式时会保护TCP/UDP头,但是并不保护IP 头,因此修改IP 地址并不会破坏整个数据包的完整性。但是如果数据包是TCP/UDP数据包,NAT设备就需要修改数据包的校验值(被ESP 所保护)。所以ESP在传输模式不能用于NAT穿越。
ESP隧道模式不验证IP包头,因此ESP隧道模式并不和NAT冲突。
ESP隧道模式对原IP地址也做了保护,有助于保护端对端隧道通信中数据的安全性。
因特网密钥交换协议IKE
IKE是信令协议,提供自动协商交换密钥、建立安全联盟的服务。有自保护机制,可以在不安全的网络上工作。
IKE不在网络上直接传送密钥,而通过一系列数据交换,最终计算共享密钥(即使被截获所有交换数据,也不足以计算出真正的密钥)
IKE是UDP之上的一个应用层协议,为IPSec协商建立SA,并把参数和生成的密钥交给IPSec。
IKE的安全机制
- 完善的前向安全性PFS:一个密钥被破解不影响其他密钥的安全性(由DH算法保障)
- 数据验证:数据完整性和身份保护
- DH交换和密钥分发
IKE协商过程阶段一
在网络上建立IKE SA,为其他协议的协商提供保护和快速协商。
通过协商创建一个通信信道,并对该信道进行认证,为进一步IKE通信提供机密性、消息完整性以及消息源认证服务。
协商过程包含三对消息:
- SA交换:协商确认有关安全策略
- 密钥交换:交换DH公共值和辅助数据,加密物在这个阶段产生
- ID信息和验证数据交换:进行身份验证和对整个SA交换进行验证
主模式协商
适用于两设备的公网IP固定、且要实现设备之间点对点的环境
野蛮模式协商
对于例如ADSL拨号用户,其获得的公网IP不是固定的,且可能存在NAT设备的情况下,用野蛮模式做NAT穿越,同时用name作为id-type。
两种模式对比
IKE协商过程二
使用快速模式交换,效果为协商出IPSec单向SA,为保护IPSec数据流而创建,整个协商过程受第一阶段ISAKMP/IKE SA保护。
主要功能:
- 协商安全参数保护数据连接
- 周期更新密钥信息
CH4:SSL
利用数据加密、身份验证和消息完整性验证机制,为HTTP提供安全连接
SSL位于应用层和传输层之间,能够为基于TCP等可靠连接的应用层协议提供安全性保证
SSL安全机制
- 传输数据的机密性:对称密钥算法
- 身份验证机制:基于证书利用数字签名对server和client(可选)进行身份验证
- 消息完整性验证:MAC算法
SSL分层结构
上层协议
SSL握手协议
SSL的核心协议部分,协商通信过程中使用的加密套件(加密算法、密钥交换算法、MAC算法等)、在S/C之间安全交换密钥、实现S和C的身份验证。
阶段1:建立安全能力
启动逻辑连接,建立这个连接的安全能力。
client hello消息包括:
- 支持的协议版本
- 一个客户端生成的随机数,用于生成对话密钥
- 支持的加密算法
- 支持的压缩方法
server hello消息对client hello中的信息进行确认:
- 确认使用的协议版本
- 一个服务器生成的随机数,用于生成对话密钥
- 确认加密方法
- 服务器证书
阶段2:服务器鉴别与密钥交换
- certificate:服务器发送自己的证数
- server_key_exchange:可选,包含被签名的两个随机数和服务器参数
- certificate_request:非匿名server可以请求客户端证书
阶段3:客户机鉴别与密钥交换
- 客户根据服务器证书判断是否可以接受参数
- 如果服务器请求证书就首先发送certificate消息/no_certificate警告,然后发送client_key_exchange
- certificate_verify包含对之前所有握手消息的MAC的签名
阶段4:完成
建立起一个安全的连接
- 客户发送change_cipher_spec消息(是一个独立的协议,用于告知服务端客户端已经切换到协商好的CipherSuite的状态),并把协商得到的CipherSuite拷贝到当前连接
- 客户用新的算法、密钥参数发送finished消息
- 服务器同样发送,握手完成
SSLpassword变化协议
C和S通过该协议通知对端:随后的报文都将使用新协商的加密套件和密钥进行保护和传输。
SSL警告协议
向对端报告告警信息,包含告警的严重级别和描写叙述。
- 致命消息:立即终止当前连接
- 警告消息
下层协议
SSL记录协议
负责对上层数据(上层协议和应用层协议报文)进行分块、计算并加入MAC值、加密,然后传送给对端
- 机密性:协助双方产生共有的密钥对数据加密
- 消息完整性:产生另一把密钥计算出消息认证码
操作流程
- 分片
- 压缩
- 计算MAC
- 加密
- 附加SSL头
SSL基本过程
- 建立一个会话
- 协商算法
- 分享秘密
- 身份认证
- 传送应用数据
- 确保机密性和完整性
SSL连接
- 是一个提供一种合适类型服务的传输
- 点对点的关系
- 连接是暂时的,每个连接和一个会话关联
SSL会话
- 一个SSL会话是在C和S之间的一个关联。会话由Handshake Protocol创建。定义了一组可供多个连接共享的密码安全参数。
- 会话用以避免每一个连接提供新的安全参数所需的协商代价。
SSL协议的加密和认证算法
认证算法采用X.509电子证书标准,使用RSA算法进行数字签名实现
SSL安全性分析
- 鉴别机制:公钥技术和数字证书
- 加密机制:混合密码体制,使用非对称密码体制协商处会话密钥,并选择对称加密算法
- 完整性机制:定义了共享的、可用来生成MAC的密钥
- 抗重放攻击:使用序列号作为数据包负载防重放。整个SSL握手中都有一个唯一的随机数标记这个SSL握手。
SSL脆弱性分析
- 客户端假冒:SSL并不默认要求进行客户鉴别(防止由于安全协议导致网络性能大幅下降)
- 无法提供基于UDP应用的安全保护
- 不能对抗通信流量分析:数据包的IP头和TCP头仍然暴露,只保护应用数据
- 进程中主密钥泄露:主密钥将会存留在SSL进程存储空间中
WTLS
保证传输层安全,在TLS基础上,根据无线环境增加了一些新特性
CH5:SET
电子交易主要模式
支付系统无安全措施模式
- 风险由商家承担
- 商家完全掌握用户的信用卡信息
- 信用卡信息的传递无安全保障
通过第三方经纪人支付的模型
- 用户账户的开设不通过网络
- 信用卡信息不在开放网络上传送
- 通过电子邮件确认用户身份
- 商家自由度大、风险小
- 支付是通过双方都信任的第三方完成的
数字现金支付模型
- 银行和商家之间应该有协议和授权关系
- 用户、商家和数字现金的发行都需要使用数字现金软件
- 适用于小额交易
- 身份验证由数字现金完成
- 数字现金的发行负责用户和商家之间的实际资金转移
- 数字现金和普通现金一样,可以存取转让
简单加密支付模型
- 信用卡等关键信息需要加密
- 使用对称和非对称加密技术
- 可能要启用身份认证系统
- 以数字签名确认信息的真实性
- 需要业务服务器和服务软件的支持
安全电子交易SET支付模式
SET协议的目标
- 信息在互联网上安全传输,不能被窃听或篡改
- 用户资料要妥善保护,商家只能看到订货信息,看不到用户的账户信息
- 持卡人和商家相互认证,确定对方身份
- 软件遵循相同的协议和消息格式,具有兼容性和互操作性
SET(Secure Electronic Transaction )
SET的动机和范围
- Internet的不安全性
- SET仅仅关心支付问题
交易中的主体
主体证书
- 协议各方持有名字和密钥对
- 身份使用X.509v3证书和密钥关联
SET安全架构需求
- 支付订单信息的机密性
- 传输数据的完整性
- 卡持有者身份的合法性认证
- 商家的身份认证
- 保证参与方的利益
- 独立于传输安全
- 软件架构沟通性
SET电子支付流程
- 客户在发卡行开户
- 客户持有银行签发的X.509v3证书
- 商家持有两个同类品牌的X.509v3证书(签名+密钥交换)
- 客户向商家发订单
- 商家发送证书拷贝向客户出示自己身份
- 客户发送订单和支付信息给商家
- 商家向支付网关请求支付授权
- 商家确认向客户订单
- 商家向客户提供商品或者服务
- 商家向支付网关请求支付
SET双重数字签名
将两个消息连接在一起,这两个消息面向的对象不同
- Order Information(OI):客户给商家
- Payment Information(PI):客户给银行
按需分发消息:
- 商家不需要卡信息
- 银行需要订单信息
- 保护客户隐私
具体操作
- 将 $PI$ 和 $OI$ 分别初次hash
- 连接成 $[H(PI)||H(OI)]$ 再hash
- 客户私钥加密产生双重签名 $DS=E_{KRC}[H(H(PI)||H(OI))]$
- 商家收到 $OI$ 校验签名
- 银行收到 $PI$ 校验签名
- 客户连接 $OI$ 和 $PI$,证明该关联
SET消息流
支付过程初始化InitReq/InitRes
- 持卡人浏览选择商品 , 下订单,选择银行卡;
- 持卡人向商家发送 初始请求 ,请求指定交易环境,包括
- 持卡人所使用的语言 , 交易 ID
- 使用的是何种交易卡等
- 商家接受初始请求,产生 初始应答 ,对初始应答生成消息摘要,对此消息摘要进行数字签名,将商家证书,网关证书,初始应答,消息摘要的数字签名等
购物请求
- 持卡人接受初始应答,检查商家证书和网关证书。接着用商家公钥解开消息摘要的数字签名,用 HASH 算法产生初始应答的摘要,将两者比较,如果相同则表示数据在途中未被篡改,否则丢弃。
- 持卡人发出购物请求( PReq ),它包含了真正的交易行为,由两部分组成
- 发往商家的定单信息 (OI) : links to order description
- 通过商家转发往网关的支付信息 (PI): amount, card data, IDs
- 通过双重数字签名将 OI 与 PI 进行关联
PReq消息结构
PReq消息校验
商家验证卡用户的身份和授权
- 商家接受持卡人的购物请求,认证持卡人的证书。接着验证双重签名,看数据在传输过程中是否被篡改。如数据完整,则处理定单信息,产生支付请求。
- 将支付请求用 HASH 算法生成摘要,并签名,网关收到后用商家公钥解密,并确认支付请求是此商家所发在且在途中未被篡改。生成对称密钥对支付请求加密,并用网关公钥加密形成数字信封。
- 最后将商家证书,支付请求密文,商家数字签名,数字信封和持卡人通过商家转发的: $sign[H(OP)]$ , $OI$ 摘要,$PI$ 密文,持卡人数字信封,持卡人证书等发往支付网关。
支付网关认证过程
- 支付网关分别检查确认商家发来的数据和持卡人发来的数据用 HASH 算法作用于支付请求,形成摘要,与商家发来的支付请求摘要(解开数字签名所得)相比较,如果相同则表示数据完整,否则丢弃数据
- 网关检查持卡人证书,然后用私钥打开持卡人数字信封,得到他的帐号和对称密钥。用此对称密钥解开 PI 密文,得到 PI ,接着验证双重签名,生成 PI 的摘要,与 OI 摘要相连接,再次生成摘要,其结果与 H(OP) (解双重签名所得) 相比较,如果相同则数据完整,如果不同则丢弃。
- 网关将信息发送往银行
- 支付网关和银行之间通过金融专用网相连
收单银行处理
- 解密AuthReq
- 校验商家签名
- 解密来自持卡人的PI
- 校验双重签名
- 从PI中抽取卡数据
确保 PI 和 AuthReq 的一致性,校验持卡人和商家对于订购行为的一致性 : H(Order) PI和 AuthReq,生成 AuthRes 及其 Capture Token。
支付完成
- 完成授权 交易的支付
- 通过捕获令牌完成支付
- 可能多次AuthResponses的令牌积累后完成
- Capture Token = 金额证据
下单的回复
- 完成代码CompletionCode:交易状态
- 结果Results:交易的授权/捕获代码
SET中的核心技术
- 公钥加密:对称加密和非对称加密4次
- 数字签名:进行签名5次,验证签名6次
- 电子信封
- 电子安全证书:传递证书7次,验证9次
SET和SSL的不同之处
- 首先,SET 远远不止是一个技术方面的协议,它还说明了每一方所持有的数字证书的含义,希望得到数字证书以及响应信息的各方应有的动作,与一笔交易紧密相关的责任分担。 SET 实现非常复杂,商家和银行都需要改造系统以实现互操作,并且还需要认证中心的支持。
- SET 是一个多方的报文协议,它定义了银行、商家、持卡人之间的必须的报文规范。与此同时, SSL 只是简单地在两方之间建立一条安全连接。 SSL 是面向连接的,而 SET 允许各方之间的报文交换不是实时的。
- 另外,SET 报文能够在银行内部网或者其他网络上传输,而 SSL 之上的卡支付系统只能与 Web 浏览器捆绑在一起。
- 最后,SSL 相对不安全,实际上当初它并不是为支持电子商务而设计的。很多银行和电子商务解决方案提供商仍然在使用 SSL 来构建更多的安全支付系统,但是如果没有经裁剪的客户方软件的话,基于 SSL 的系统式不能达到像 SET 这种银行卡专用支付协议所能达到的安全性的。
CH6:PGP
电子邮件系统
E-mail是Internet上最大的应用,是唯一的广泛跨平台、跨体系结构的分布式应用
不是端到端服务,是一种存储转发式的服务
电子邮件系统的主要成分
一个完整的电子邮件系统具有三个主要成分:
- 客户端用户代理 MUA(mail user agent)
- 邮件传输代理 MTA(mail transfer agent)
- 邮件投递代理 MDA(mail delivery agent)
电子邮件相关协议
SMTP
简单邮件传输协议( simple mail transfer protocol ),它是一组用于从源地址到目的地址传输邮件的规范,通过它来控制邮件的中转方式
POP3
POP 邮局协议负责从邮件服务器中检索邮件
IMAP
互联网信息访问协议( IMAP )是一种优于 POP 的新协议,它可以请求邮件服务器只下载所选中的邮件而不是全部邮件,客户可以先阅读邮件信息标题和发送者名字再决定是否下载邮件
MIME
多功能 Internet 邮件扩充服务,可使邮件包含一般文本之外,还可以加上彩色图片、视频、声音或二进制格式的文件
安全问题
- 匿名转发
- 发件人刻意隐瞒自己的信息,或通过某些方法提供错误的发件人信息
- 发送者首先将邮件发送给匿名转发系统,匿名转发邮件系统再转发给真正的收件者,并将自己的地址作为发信人地址显示在邮件的信息表头中。对安全要求高的用户必须使用邮件加密和数字签名技术
- 电子邮件欺骗
- 假冒某用户的身份给其他用户发送邮件(SMTP本身不提供任何验证)。通过身份认证避免邮件欺骗。
- 邮件炸弹和垃圾邮件
- 安装过滤器,预先检查发件人资料
- 邮件病毒
- 通过预杀毒防止
解决方案
- 端到端的安全电子邮件技术
- S/MIME和PGP,一般只对信体进行加密和签名,而信头必须保证原封不动。
- 要求信头在传输过程中也保密,使用传输层技术作为后盾
- 使用SSL SMTP和SSL POP
- 使用VPN或其他IP通道技术
- 邮件服务器本身安全可靠
PGP
PGP 提供可用于电子邮件和文件存储应用的保密与鉴别服务
PGP功能
PGP数字签名和认证
- RSA的强度保证发送方身份
- SHA-1强度保证签名的有效性
- DSS/SHA-1可选替代方案
PGP保密性操作
- 对称和非对称加密的结合缩短了加密时间
- 用公钥算法解决 $K_s$ 的单向分发问题
- 每个消息都有自己的一次性密钥
PGP保密和认证的结合
PGP压缩
PGP用ZIP算法进行压缩
- 节省空间
- 签名之后压缩
- 加密压缩之后的报文,冗余减少,加密强度增强
PGP密钥环
- PGP 在每个结点提供一对数据结构
- 一个是存储该结点拥有的公开 私有密钥对——私有密钥环
- 另一个是存储该结点知道的其他所有用户的公开密钥——公开密钥环。
PGP公钥的分发
无政府状态,由用户决定信任与否。
- 获取某人的公钥并信任它
- 将其加入自己的PGP系统
- 公钥服务器
PGP信任网
证书是可选的,彼此之间可以颁发证书(信任网)。
- 通过自己的数字签名确认
- 通过自己完全信任的人的数字签名确认
- 通过自己有限信任的多个人的数字签名确认
CH7:Kerberos
密钥管理问题
所有的密码系统都存在:如何安全 可靠地分配密钥
安全问题经常是密钥分配系统被破而不是密码算法被破
理想的情况是:密钥分配协议应得到形式化验证
Kerberos认证服务协议
- 提供一个在客户端跟服务器端之间或者服务器与服务器之间的身份验证机制 (并且是相互的身份验证机制)
- 解决的问题:
- 在一个公开的分布式环境中,工作站上的用户希望访问分布在网络中的服务器上的服务
- 服务器希望能够限制授权用户的访问,并能对服务请求进行鉴别。
Kerberos加密体制
- Kerberos 不是为每一个服务器构造一个身份认证协议,而是提供一个中心认证服务器,提供用户到服务器和服务器到用户的认证服务。
- Kerberos 采用传统加密算法(无公钥体制)
Kerberos主要功能
在一个分布式的 client/server 体系机构中采用一个或多个 Kerberos 服务器提供一个认证服务。
总体方案是提供一个可信第三方的认证服务。
- 用 tickets 验证
- 避免本地保存密码和在互联网上传输密码
- 包含一个可信的第三方
- 使用对称加密
- 客户端与服务器(非 KDC )之间能够互相验证。
满足的要求:
- 安全
- 可靠
- 透明
- 可伸缩
Kerberos Version 4
- 引入一个信任的第三方认证服务,采用一个基于Needham & Schroeder 协议。
- 采用 DES ,精心设计协议,提供认证服务。
基本概念
- Principal 安全个体
被认证的个体,有一个名字(name)和口令(password) - KDC(Key distribution center)
是一个网络服务,提供 ticket 和临时的会话密钥 - Ticket
一个记录,客户可以用它来向服务器证明自己的身份,其中包括客户的标识、会话密钥、时间戳,以及其他一些信息。 Ticket中的大多数信息都被加密,密钥为服务器的密钥 - Authenticator
一个记录,其中包含一些最近产生的信息,产生这些信息需要用到客户和服务器之间共享的会话密钥 - Credentials
一个 ticket 加上一个秘密的会话密钥 - Authentication Server (AS)
- 通过 long term key 认证客户
- AS 给予客户 ticket granting ticket 和 short term key
- 认证服务
- Ticket Granting Server (TGS)
- 通过 short term key 和 ticket granting ticket 认证客户 .
- TGS 发放 tickets 给客户以访问其他的服务器
- 授权和访问控制服务
动机:
- 认证和授权的逻辑分离
- TGT(10 hours)和ST(5 minutes)的生命周期不同
- 方便客户,降低密钥暴露时间
认证服务交换:获得票据许可票据
票据许可服务交换:获得服务许可票据
客户/服务器认证交换:获得服务
Kerberos领域和多个域服务
一个完整的Kerberos环境(域)包括一个Kerberos服务器,一组工作站和一组应用服务器
- Kerberos服务器必须在其数据库中有所有用户的UID和口令散列表,所有用户均在Kerberos服务器上注册
- Kerberos服务器必须与灭一个服务器之间共享一个保密密钥。所有服务器均在Kerberos服务器上注册
不同域的鉴别机制:每个辖区的Kerberos服务器与其他辖区内的Kerberos服务器之间共享一个保密密钥,且相互注册
跨域认证:
- 获得本地TGS的访问权
- 请求远程TGS的TGT
- 向远程TGS申领SGT
Kerberos Version 5
基于v4的改进
- 通用性:
- 加密算法 v4 仅仅 DES, v5 扩展
- 网络协议地址 : v4 IP, v5 OSI
- 票据生命周期 : v4 最大值 1280 minutes, v5 不限制
- 认证转发 : v5 允许服务器在事务中代表一个客户端访问另一台服务器
- 双重加密
- v4中的票据被重复加密
- 消息重放
- AS->C 和 TGS->C消息在票据生命周期中可被重放,v5采用新鲜数避免
- 采用同一票据的多个CS连接使用相同的会话密钥,可被重放。v5采用subkey机制
Kerberos优点
- 密码不易被窃听
- 密码不在网上传输
- 密码猜测更困难
- Single Sign on
- 更便捷 一次使用口令登录
- 不用记忆多个口令
- 票据被盗之后难以使用,因为需要配合认证头来使用
CH8:ban
安全协议的形式化分析
- 目前的技术主要用于对密钥正确的认证
- 安全协议的形式化分析有助于减轻协议设计者的部分工作量:
- 界定安全协议的边界,即协议系统与其运行环境的界面。
- 更准确地描述安全协议的行为。
- 更准确地定义安全协议的特性。
- 证明安全协议满足其说明,以及证明安全协议在什么条件下不能满足其说明。
- 基于推理结构性方法
- 基于攻击结构性方法
- 基于证明结构性方法
逻辑类分析方法
- 逻辑:运用形式化方法研究和判定推理形式有效性
形式化方法 :将一套特制的人工符号应用于演绎体系以使其严格化 、精确化的研究方法 。包含符号化和系统化 。
- 符号化:将命题 (p,q,r) 和常项(如命题连接词)用符号标识
- 系统化:在符号化的基础上将一定范围内所有有效的推理形式形成一个形式系统
狭义形式系统:形式语言和演绎装置。
- 形式语言:系统的初始符号(字母表),形成规 则(如何使用符号组成公式)。
- 演绎装置:包括定义、公理和规则。
- 广义形式系统:增加语义部分。即对初始符号 、公式和规则的解释。解释可把形式系统与一 定模型(代表客观实际)连接起来,从而赋予初始符号和公式一定的实际意义。
逻辑-推理结构性方法
运用逻辑系统从用户接收和发送的消息出发,通过一系列的推理公理退证协议是否满足其安全说明。
- 典型:BAN逻辑,Kailer逻辑,RV逻辑
特点:
- 简洁直观,易于使用
- 理想化方法,分析协议之前必须对协议进行形式化处理(用逻辑语言描述)
- 使用假设和推理规则
- 假设不正确——不能得到正确的信念
- 公里和推理规则是否合理和完备也影响性能
BAN逻辑系统
- 定义:基于主体知识和信念推理的模态逻辑
- 过程:通过推导主体是否能够从接收到消息中获得信念来判断协议是否能够达到认证目标
推理规则——消息意义规则
从加密消息所使用密钥以及消息中包含的密码来推断消息发送者的身份
推理规则——随机数验证规则
推理规则——仲裁规则
拓展主体的推知能力,使主体可以在基于其他主体已有的信仰之上推知新的信仰
推理规则——信仰规则
反映信念在消息的级联和分割的不同操作中一致性以及信仰在此类操作中的传递性
推理规则——接收规则
定义了主体在协议运行中获取消息
推理规则——新鲜规则
推理规则——传递规则
BAN逻辑的假设
时间假设
- 协议分析中区分current-time和past-time。
- current-time:起始于本次协议运行的开始阶段
- past-time:current-time之前的时间
如果某一观点在协议开始时是成立的,那么在整个current-time中也是成立的
但在past-time中成立的观点在current-time中却并不一定成立
密钥-主体-假设
- 密钥不能从密文中推导
- 不拥有正确密钥不能解密
- 主体能够知道是否正确使用了解密密钥(错误解密无意义)
主体-假设
假设参与协议运行的主体都是诚实的
自身消息可识别-假设
假设接收方能分辨接收到的消息是否为自己发送过的消息
应用BAN逻辑
- 对协议进行理想化预处理(初始化)。
- 给出协议初始状态及其所基于的假设。
- 形式化说明协议将达成的安全目标。
- 运用公理和推理规则以及协议会话事实和 假设,从协议的开始进行推证直至验证协议 是否满足其最终运行目标。
BAN逻辑应用实例——NS协议漏洞
BAN逻辑的局限性
- 省略掉对于推知主体信仰无用部分,如明文。
- 协议的理想化过于依赖于分享者的直觉,使得原始协议与理想化协议间存在语义鸿沟。
- 协议的理想化是将协议过程语言中对协议主体行为的描述解释为用逻辑语言描述的主体的知识和信仰 ,并以此来表示协议说明的语义。现有的逻辑形式 化分析系统很难解决此问题。
- BAN证明没有问题,并不能保证该协议没有问题。
BAN逻辑缺陷:
- 不合理的假设
- BAN逻辑钟,初始状态的假设难以确定,从而无法确 认和自动验证假设的正确性和有效性
- BAN逻辑系统认为参与协议运行的主体都是诚实的
- 不能检查协议并发运行带来的攻击
- BAN缺少一个良好定义的语义
CH9:csp
攻击结构型方法
模型检测方法:给定模型M和性质P,检查M中P是否成立
- 主体数目的有限性:通常分析有限主体实例,只说明在某个数目下未发现错误
- 无法解决状态空间爆炸问题:当协议只有三五条、主体数目只有四五个时,效率较高,超过时会出现内存和时间问题。
- 无法解释安全协议的内部机理
通用的形式化验证方法——通信顺序进程CSP
- 专为描述并发系统消息交互而设计的抽象语言
- 将协议的安全问题描述为CSP进行是否满足其CSP规约的问题,并使用FDR对协议的性质进行分析和验证
CSP基本术语
- 事件:协议系统通过其执行的一系列事件加以描述。c.i.j.m包括一个信道c、一个消息源i、一个目的地j和一个消息m
- 信道:不同事件类型看成不同信道,并规定它所传递的数据类型
- 进程:CSP通过用某一进程可能涉及的事件来描写该进程,从而提供了一种描述进程可达状态的方法
- 执行状态中的一个动作(事件)+动作结束后的状态
常见的CSP进程:
协议目标的CSP描述
- 保密性
- 认证性
- 完成安全协议的 CSP 建模及安全目标描述 以后,可以采用 基于模型检测的分析方法 对 安全协议进行分析。
- 基本原理:主要采用自动化分析工具 FDR(Failures Divergences Refinement, 故障发散提炼器) 工具 完成。
- FDR 接受协议规范和协议实现的两个 CSP 作为输入:
- 规范:一个抽象 的 系统 具有 一 定的 性 质 。
- 实现:较具体的系统,常希望其具备某种性 质 。
- FDR 检查协议的实现是否精炼了规范,即实现的每一个迹是否为协议规范的一个迹