Internet 安全协议,6个安全协议实例+安全协议分析方法
第一部分 安全协议基础
第一章 概述
1.1 Internet协议与安全需求
信息系统安全范围:物理安全,计算机安全,网络安全
信息安全的目标:保密性,完整性,可用性——CIA
攻击类型:Interruption(拦截),Interception(窃听),Modification(篡改),Fabrication(伪造)
网络安全需求:
- 身份鉴别
- 访问控制
- 可用性(3A)
- 数据机密性
- 数据完整性
- 抗否认性
常见安全协议:
- Kerberos协议:解决分布式场景下的安全认证与授权问题
- IPSEC:解决IP层的安全加固问题
- SSL/TLS协议:解决传输层的安全加固问题
- SET协议:提供安全支付的一种经典问题解决方案
- PGP协议:无政府状态下的互联网信任安全问题解决方案
- CSP: 提供一种电子合约签订的解决方案
1.2 密码学回顾
加密四要素:密钥,算法,明文,密文
公钥密码体系:加密,鉴别
- 数字签名(签名和校验两部分),安全属性:不可否认性,不可伪造性,可第三方仲裁
- 密钥分配:
- 公钥证书:初始化阶段,颁发阶段,撤销阶段
- 安全属性:保密性,完整性,不可否认性
- 基于CA的电子证书(包含公钥,申请者信息,证书有效期)
- 创建过程:申请人创建公私钥;填充申请信息并发送(用CA公钥加密);CA检验申请;CA创建证书并用自己私有密钥对其签名;发送/邮寄证书
- PKI:核心是CA
- 可逆公钥密码体制
- 公钥证书:初始化阶段,颁发阶段,撤销阶段
Hash函数:输入任意长度,输出固定长度;单向函数;容易计算
1.3 逻辑学回顾
- 命题逻辑
- 连接词将原子谓词组合为符合谓词:合取,析取,否定
- 谓词逻辑
- 原子公式与符合谓词公式
第二章 安全协议
基础概念
- 协议:一组语义和语法规则,决定功能部件在通信时如何进行工作;两个或两个以上的参与者采取一系列的步骤,以完成某项特定的任务
- 安全协议(背!):基于密码体制,在分布式系统和通信网中,实现密钥分配、身份认证、信息保密、电子商务等服务
- 准则:主体身份标识,签名,随机数,时戳——系统中各个主体承认的可靠分布式时钟
- 随机数用于提供消息的新鲜性,每轮随机数不同,可防止重放攻击
- 时戳依赖于系统承认的分布式时钟
- 缺陷:陈旧消息(上一轮次消息),并行会话
- 准则:主体身份标识,签名,随机数,时戳——系统中各个主体承认的可靠分布式时钟
- 消息重放对策:序列号,时戳,挑战应答
- 挑战应答:客户端要求进行身份认证,服务器查询是否合法,合法则产生随机数,作为挑战发给客户端。客户端将ID和随机数哈希并发回。服务端对比,若相同则认证成功
- 良好密钥标准:新鲜,来自可信第三方,仅为协议指定合法主体拥有
协议实例
RPC 协议:利用已有的共享密钥建立新的会话密钥
多重会话攻击:攻击者在不同会话中,先后扮演接收方B和发送方B,重放A的部分。最终A更新了会话密钥,实际的B没有更新
加固:在加密内容中添加接收方的身份标识
NS 对称密钥协议:可信第三方参与,分配会话密钥
- 攻击:替换加密内容,使双方获得的会话密钥不相同
Otway-Rees 协议:通过可信服务器分配共享密钥
- 攻击:攻击者伪装B,收到1)后重放,即 $Z(B)\rightarrow A:M,E(K_{as}:N_a,M,A,B)$
- 加固:挑战应答,新鲜数+1
大嘴青蛙协议:一种对称密钥管理协议
- 攻击:
- 加固:在发往S的消息中加入发送方的身份标识
NS 公钥协议:A和B通过可信第三方交换公钥
- 攻击:攻击者可以是合法用户,在两个轮次内重放。
- 轮次1:A与攻击者握手交换key
- 轮次2:攻击者假冒A与B通信,使B以为与A交换公钥,但A并不知情
- 加固:在6)中加入发送方和接收方的身份标识
- 攻击:攻击者可以是合法用户,在两个轮次内重放。
Denning Sacco 密钥分配协议
- 攻击:B可向C重放被A私钥加密的内容(用C的公钥封装),使C以为和A有会话密钥
加固:A私钥加密内容中,加入接收方的身份标识
协议设计原则:
- 不引入额外的加密和消息字段
- Nonce 与时戳不可完全混用
- nonce 本身需要加密——基于随机数的挑战应答机制,需要有效保护随机数
- 时戳使用前提是有可靠的分布式时钟机制
第二部分 常见的安全协议
第三章 Kerberos
基本概念和过程
单点登录机制:能够使用一组凭据登录一次,并访问有权访问的所有系统和联机资源
- KDC 给予 ticket
tgt——认证 - TGT 可以用于获取其他的服务票据 ticket
v——授权
- KDC 给予 ticket
Kerberos 协议原理
基于 NS 可信第三方协议和 Denning Sacco 协议
基本概念:
- Principal:被认证的安全个体
- AS:认证用户(通过long-term key),给予用户tgt和short-term key
- tgs:通过tgt和short-term key认证用户,通过发放ticket对用户授权和访问控制
- KDC:网络服务,提供ticket与临时会话密钥
- Ticket:一个记录,客户凭此向服务器证明身份。被服务器密钥加密
- Authenticator:一个特殊记录,包含最近产生的信息,被客户与服务器之间的共享密钥加密
- Credentials:一个ticket加上一个会话密钥
- Principal:被认证的安全个体
认证与授权逻辑分离
设定不同的票据生命周期
过程:第一轮与AS交互(返回tgs票据和与TGS的会话密钥,同时通过Kc认证C的身份),第二轮与TGS交互(发送tgs票据与认证头,告诉tgs用户已被AS认证,返回v票据以及临时会话密钥),第三轮与V交互(发送v票据与认证头,票据用于证明用户已被AS认证,认证头用于验证票据,返回一个应答)
v5过程:
Kerberos v5
- 改进:
- 扩展加密算法
- 不限制票据生命周期
- 跨域访问更为自然:获得本地 TGS 的访问权,请求一张远程TGS的票据许可票据,向远程TGS申请服务许可票据
- 不再双重加密
- 采用新鲜数防止消息重放;采用 subkey 机制,防止使用同一票据的使用同一会话密钥的多个client-server连接被重放攻击
Kerberos 协议优缺点
- 优点:
- 密码不在网上传输,猜测更困难
- 单点登录机制,更加便捷,不用记忆多个口令
- 存储上有性能优势
- 票据与认证头结合,票据被盗后难以使用
- 缺点:
- 缺少撤销机制:tgt 无法撤销
- 服务器可模拟任何人;可能是性能的瓶颈:所有人都要连接
- 密钥管理
- 使用了时戳,需要时钟同步
- 跨域认证繁琐
- 口令安全问题
第四章 PGP&CSP
PGP
公钥环,私钥环,PGP的处理流程
基础:
- 主要解决身份鉴别和保密性问题:跳转节点不可控,服务器可能在境内或境外
- Email工作原理:电子邮件客户端——SMTP协议、发送方电子邮件服务器端口25——TCP连接,SMTP协议——接收方电子邮件服务端口25——pop3协议tcp连接端口110——电子邮件客户端
- PGP公钥分发:
- 每个人都可以做CA,将B的公钥签发给第三方,第三方自行决定是否信任——B信任A且获得A签名的C公钥,则B信任C公钥
- 存在风险:A检查不当/A被贿赂——用不用在于B本身,同时可设定公钥(证书)的信任度
- none,partial,complete
- 个体的信任水平决定了签发的证书信任水平
- 可主动撤销公钥;证书颁发者可撤销证书;证书和密钥存在有效期
加密与认证过程(要求能够默写!):
- 压缩在签名之后进行:便于采用不同的压缩算法;验证方可以只存储原始内容和签名
- 加密在压缩之后进行:加强加密强度,冗余减少,密码分析更为困难
- 加密在签名后进行:如果不是,可能被替换签名
消息生成与接收:passphrase:口令,用户解密private key
- 生成:
- 用户id作为索引获取发送者的私钥,用户输入口令来解密私钥,创建签名(发送方私钥环)
- 生成会话密钥加密,接收方ID作为索引获取接受方的公钥,创建消息(发送方公钥环)
- 接收:
- 消息内密钥ID字段作为索引获取加密私钥,用户输入口令解密私钥,获得会话密钥解密内容(接收方私钥环)
- 签名密钥id作为索引获取公钥,恢复摘要,计算摘要并认证(接收方公钥环)
- 生成:
密钥数据库
- 公钥环 pubring:主要存储其他节点的公钥。时戳,key id,公钥,信任度,user id等
- 私钥环 secring:存储节点生成的公私钥对,私钥加密处理。时戳,key id,公钥,加密私钥,user id
信任模型:
- web of trust信任模型
- 无集中授权机构
- 计算公钥环内每个公钥的信任度,用户解释信任水平
- 公钥信任水平决定于密钥的签名数目和每个签名的信任度,要不时计算
CSP(不考)
TTP的作用,Asokan-Shoup-Waidner 协议, Abuse-Free 版本协议
要求公平交换:同时成功或同时失败
问题:
- 若进程出错,则难以达成一致;网络存在时延
- 异步提交协议存在 “脆弱性窗口(window of vulnerability)”,即单个进程的延迟会导致系统的等待
没有TTP则协议并不健壮:每一次消息发送均有TTP参与,或者TTP仅在被请求时候决断
- 公平性:不允许欺骗对方(A没有B的签名,则B不能有A的签名——TTP的撤销功能)
- 及时性:不必无限等待(TTP进行恰当的实时的终止)
Asokan-Shoup-Waidner 协议
- 三种场景
- 成交子协议:没有收到m3或m4,在没有提出撤销的情况下,强制实行,否则撤销
- 撤销子协议:没有收到m2,在没有成交的前提下,强制撤销。a1为 sig
M(abort, m1),否则成交
- TTP职责:
- AB同意下,T 强制达成协议
- T 发放撤销令牌,合同不成立
- T 基于first-come-first-serve 之上决定撤销还是签订,且T仅在A或者B请求下介入——乐观的协议
- 重放攻击:K在上一轮获得了M的两条消息,由此K在下一轮冒充M与Q签订合同
- 改进:
- 三种场景
Abuse-Free
Private Contract Signature:特殊的加密原语,防止abuse
- B 无法将来自A的消息拿来呈现给 C,仅B和T能验证签名有效性
- T 转换签名为公开的sigA,但不自用
TTP作用:
- 将PCS转换为普通签名
- 发布撤销令牌
- 仅在被请求时候介入,先来先服务
三种场景:
攻击:攻击者率先申请撤销,之后B迟迟收不到第三个消息,向T申请成交,则T泄露了sig
B(text)
改进:如果T转换为传统签名,则T被追责
任何公平,乐观和及时的签订协议中, 若一方是乐观的, 则另一方拥有优势
第五章 SET
- 电子支付基本流程,双重数字签名,SET流程
SET简介
- 电子交易类型:
- 无安全措施支付模式:风险由商家承担,并掌握用户信用卡信息
- 通过第三方代理人支付模式:电子邮件确认用户身份,支付由可信第三方完成
- 数字现金支付模式:适用于小额交易,数字现金完成身份认证,数字现金发行负责用户与商家的资金转移
- 简单加密支付系统模式:对称与非对称加密,数字签名确认真实性,业务服务器和服务软件支持
- 安全电子交易SET支付模式:商家只看到订货信息,持卡人与商家相互认证
- SET只关心支付问题;脱离于底层协议的安全性,安全来自SET本身
- 要求独立于传输安全
双重数字签名
- 数字签名:内容哈希,私钥签名摘要
- 数字证书:
- data with digital signature from CA;data:过期日期,证书颁发涉及的双方
- 数字ID包括:公钥,名字,地址,过期日期,颁发CA
- 双重数字签名:
- 两个消息连接在一起,这两个消息面向的对象不同
- Order Information (OI): 客户给商家,订单信息
- Payment Information (PI): 客户给银行,消费信息
- A给商家OI+PI,商家看不到PI,商家发PI给S(银行)——确保信息不被非法使用
SET流程
消息流:
具体流程
- 客户发送订单和支付信息
- 商家向支付网关请求支付授权
- 商家确认客户订单
- 商家向客户提供商品
- 商家向支付网关请求支付
InitReq/InitRes:下订单,支付初始化,明文
- InitReq:持卡人获得商家与支付网关的证书
- InitReq:持卡人获得商家与支付网关的证书
PReq/Pres:持卡人校验证书,生成OI/PI,下单
- PReq:SET核心
- 发送:
- 商家验证:存储PI并转发,校验持卡人证书,双重签名,从支付网关获取授权,发回响应确认订单(授权延迟,则发回“请稍后查询”)
- PRes:无加密,商家仅签名消息,其中完成代码(CompletionCode)代表交易状态
- PReq:SET核心
AuthReq& AuthRes:认证,校验持卡人信用;商家签名并公钥加密AuthReq,根据AuthRes结果运输商品。H(Order)表明和PI的一致性,
- AuthReq:
- 接收后的处理:解密Req,校验商家签名,解密PI,校验双重签名,PI抽取卡数据。
- 确保PI和AuthReq的一致性
- H(Order),PI,AuthReq共同校验持卡人、商家对订购行为的一致性
- 生成AuthRes与捕获令牌
- 接收后的处理:解密Req,校验商家签名,解密PI,校验双重签名,PI抽取卡数据。
- AuthRes:
- AuthReq:
CapReq&CapRes(Cap:捕获):完成已授权交易的支付
- 通过捕获令牌Cap Token(金额证据)完成支付(可能在多次AuthRes的捕获令牌累积后完成,即CapReq中一次发送多个Cap Token)
- CapReq:${ { CapReq} sig_M } PK_A$;CapRes:${ { CapReq} sig_A } PK_M$
交易过程:
- 验证电子证书9次
- 传递证书7次
- 验证数字签名6次
- 进行签名5次
- 对称加密和非对称加密4次
SET核心技术
- 数字证书
- 数字签名
- 电子信封(会话密钥加密,公钥加密会话密钥)
- 公钥加密
对比SSL:
- SET实现非常复杂,商家和银行都需要改造系统以实现互操作,需要CA支持
- SET是一个多方的报文协议,允许各方报文交换不是实时的;SSL面向连接,且只是在两方之间建立一条安全连接
- SET报文能够在银行内部网或者其他网络上传输,SSL之上的卡支付系统只能与Web浏览器捆绑
- SET安全性更高
第六章 IPSEC
- IPsec的基本概念:SA, SPD,AH,ESP, 隧道模式, 传输模式, Outbound & Inbound 处理,两个阶段SA的区别
- IP安全
- 通信双方身份验证
- 数据完整性与机密性保护
- IP地址欺骗
IPsec概念
- IPsec:一组安全IP协议集,现代密码学方法支持机密性和认证性服务
- 认证包的发起者,防止传输中的拦截和篡改,提供访问控制、无连接完整性、数据源鉴别、载荷机密性和有限流量机密服务
- IPv4可选,IPv6必选
- 机制:认证、信息机密性和密钥管理
- 两个分离的层:IKE(互联网密钥交换)与 IP-Sec record sub-layer(流量封装与保护)
- SA(Security Association)
- 由SPI(Security Parameter Index,安全参数索引)和目标地址组成,它表示通信方如何使用安全服务进行安全通信
- 单个IPsec连接至少需要2个SA
- 参数:认证算法与模式,加密算法与模式,密钥及生命周期等
- SPI:两部VPN主机之间以随机数或手动指定的唯一值,其目的是要作为数据库的索引值
- SAD(Security Association Data)
- 含有所有活跃的SA
- 存放在 SAD 中的参数有 SPI 值、目的端IP、安全协议号(AH或ESP)、AH 验证算法等
- SPD(Security Policy Data)
- 用户定义的策略:每个报文的安全服务及其水平
- 用来存放 IPSec 的规则,这些规则用来定义哪些流量需要走 IPSec
- AH(Authentication Header)
- 每一个数据包上添加一个身份验证报头,提供数据源认证、完整性保护和重放保护,无机密性保护
- AH校验包含源地址,与NAT冲突
- 传输模式:AH被插在IP头之后、所有的传输层协议之前、其它IPSec协议头之前
- 隧道模式:AH插在原始的IP头之前,并生成一个新的IP头放在AH之前
- 输出:
- SA查找
- 生成序列号
- 计算ICV校验值(完整性保护)
- 填充,分段
- 接收:
- 重组
- SA查找
- 序列号验证
- ICV验证
- 输出:
- ESP(Encapsulating Security Payload)
- 完整性,加密性,重放保护,无不可否认性,认证性取决加密算法
- IP包头部(含选项字段)不会被验证,不存在NAT模式冲突;原IP地址被当作有效载荷的一部分受到保护;可以隐藏数据包目的地址,以保护端对端隧道通信中数据的安全性;隧道模式可提供数据流加密服务
- 传输模式:origin IP hdr + ESP hdr + TCP + Data + ESP trlr + ESP auth;加密 TCP 到 ESP trlr,认证 ESP hdr 到 ESP trlr
- 隧道模式:New IP hdr + ESP hdr + origin IP hdr + TCP + Data + ESP trlr + ESP auth;加密origin IP hdr 到ESP trlr,认证ESP hdr 到ESP trlr
- ESP 提供加密处理,AH无法提供;AH 提供抗抵赖性,ESP无法提供。组合使用时,先ESP后AH,因此ESP头可被AH保护
- 输出:同上,生成序列号后对数据包加密
- 接收:同上,ICV验证后对数据包解密
- 模式架构
- 对称加密(DES),基于对称加密的单向哈希(MD5/SHA-1)
IPsec机理
- ISAKMP:SA协商与密钥管理协议
- Internet Key Exchange(IKE)用于配置 IPSEC,位于UDP之上,是后者的信令协议;通信双方协商加/解密算法及其密钥、密钥的生命期、验证算法,在 ISAKMP 规定的一个框架内运作;IKE不是在网络上直接传送密钥,而是通过一系列数据的交换,最终计算出双方共享的密钥
- IKE为IPsec协商建立SA,并把建立的参数及生成密钥交给IPsec;IPsec使用IKE建立的SA对IP报文加密或验证处理
- 阶段1:两个IKE对等体间创建一个认证过的安全通道(通过UDP端口500),即协商建立IKE SA
- 主模式:协商加密与hash算法,并用Diffie-Hellman交换密钥,校验身份(六个报文)
- 主动(快速)模式:所有协商、密钥交换等压缩成更少的包,更快但容易被嗅探(三个报文)
- 区别:
- 交互6个消息——交互3个消息
- 只能基于IP确定预共享密钥——基于ID(主机名+IP)确定预共享密钥
- 安全性较高,前四个消息明文传输,后两个消息加密,保护对端身份——安全性较低,前两个消息明文传输,后一个消息加密,不保护对端身份
- 速度较慢——速度较快
- 适用于公网IP固定,点对点环境——适合公网IP不定,且可能存在NAT设备
- 主模式:协商加密与hash算法,并用Diffie-Hellman交换密钥,校验身份(六个报文)
- 阶段2:协商 IPSec SA参数,建立 IPSec SA,周期性的重新协商IPSec SA
- 主模式身份验证方式:
- 预共享密钥认证
- 数字签名认证
- 公钥加密认证
- IPsec 执行:
- 可在主机或网关上使用:
- 主机:端到端安全服务,可用IPSec所有模式
- 路由器:对进入专用网络的用户进行身份验证和授权,允许创建VPN
- 在OS或堆栈的bump上集成
- 可在主机或网关上使用:
IPsec应用
- 具体应用
- 加强电子商务安全
- IP级别加密和/或验证所有流量
- 分布式防火墙
- 虚拟专用网
- 应用流程:
- 主机A通知本机的IPSec驱动程序检查IP筛选器,查看数据包是否需要受保护以及需要受到何种保护
- 驱动通知IKE开始安全协商
- 主机A给B发送IKE请求安全协商通知,主机B上的IKE收到请求安全协商通知,并响应,A与B建立SA第一阶段协商,生成共享主密钥
- A与B建立SA第二阶段协商,生成SA对(入站SA和出站SA, SA包括密钥和SPI )
- 驱动程序用出站SA对数据包进行签名(完整性检查)和加密
- IP层发送与接收
- 接收方驱动程序使用入站SA检查完整性签名与/或对数据包进行解密
- 驱动程序将解密后的数据包提交上层TCP/IP驱动程序,再由TCP/IP驱动程序将数据包提交主机B的接收应用程序
第七章 SSL
- 基本概念,协议过程
SSL概念
加固 http 层,使得TCP实现可靠、端对端的服务
TLS 向后兼容 SSLv3
- 认证(公私钥+数字证书)
- 保密性(会话密钥)
- 完整性(查验Message Authentication Code,MAC)
- 抗重放攻击(序列号与随机数)
子层:SSL Record Protocol (所有操作发生的位置),SSL Management: (握手/密码更改/警报协议)
体系:
核心为握手协议,完成传输数据前的加密算法协商,共享密钥建立,相互认证
基本过程
- 握手过程流程图:
- 过程1:建立安全能力
- $r_A$:新鲜数,4字节时戳+28字节随机数
- $SessID$:新的会话则为0,否则为已有会话ID
- $CiphList$:客户机支持、按优先级递减的密钥交换和加密算法列表
- $Ciphchoice$:服务器选择的加密套件
- 最后双方知道:(1)SSL版本(2)密钥交换、信息验证和加密算法(3)压缩方法(4)有关密钥生成的两个随机数。
- 过程2:服务器认证与密钥交换
- 服务器发送X.509证书及证书链($K_G$为服务器私钥)
- 服务器发送公钥(可选,有些情况不需要)
- 服务器向客户端请求证书(ValidCertAuthorities 标识服务器将接受的权限)
- 备注:仅当已发送的服务器证书消息包含的数据不足以允许客户端交换密钥时,服务器才会发送服务器预主密钥交换消息。
- 过程3:客户机认证与密钥交换
- 客户验证并发送证书
- 消息9用于认证
- $+K_G$:公钥,来自服务器证书
- $Message1to8$:前8条消息的串联
- $MS$:主密钥
- 如果服务器请求证书,发送certificates;如果客户没有证书,则发送client key exchange消息。最后发一个verify,对第一条消息以来的所有握手消息的MAC值进行签名。
- 备注:
- 主密钥master key:48字节,预主密钥转化为来
- 预主密钥premaster key:两个伪随机流互斥混合在一起
- 过程4:建立起一个安全的连接
- 客户机通知服务器更改密码(通过更改密码协议)
- 服务器用自己更改的密码消息进行响应
- Finish Message为用加密套件和会话密钥加密的数据,用于验证正式传输数据之前对刚刚建立的加解密通道
- ChangeCipherSpec 是一个独立的协议,用于告知服务端,客户端已经切换到之前协商好的加密套件(Cipher Suite)的状态,准备使用之前协商好的加密套件加密数据并传输了
- 证书校验:必须识别证书链中信任的CA(一个CA可以为另一个CA颁发证书);必须验证证书是否已被撤销(CA发布证书撤销列表)
- 加密密钥:
- Master Secret:由双方分别生成的随机值和预共享密钥生成
- Key material:由master secret和双方共享的随机值生成
- Encryption key:从Key material中提取,是对称密钥
- 总结:
- 交换Hello消息,对于算法、交换随机值等协商一致
- 交换必要的密码参数,以便双方得到统一的premaster secret
- 交换证书和相应的密码信息,以便进行身份认证
- 产生master secret
- 把安全参数提供给SSL记录层
- 检验双方是否已经获得同样的安全参数
- SSL 告警协议:表明异常出现
- 2个字节的消息
- warning则第一个字节为1,fatal则第一个字节为2且第二个字节说明错误种类(握手失败,意外消息等)
- SSL 记录协议:提供机密性(双方共有的密钥加密)与认证性(产生另一把共有密钥计算MAC)
- 数据分段后压缩
- 添加MAC(消息认证码)后加密
- 添加Record Header(内容类型+内容长度+SSL版本)
- 间接问题:比TCP会话慢2-10倍
- 握手阶段的公私钥加密
- 数据传输阶段的对称密钥加密
- 不提供UDP应用的安全保护,不能对抗通信流量分析,存在主密钥泄露和客户端假冒问题
第三部分 安全协议分析
第八章 BAN
- 消息描述:形式化方式对协议消息进行描述
- 初始假设:对协议外部特性假设,如对可信第三方的信任假设、对随机数新鲜性的假设,
- 推理规则:逻辑方法的核心
- 主体信念:逻辑分析方法的结果
BAN逻辑概念
- 符号:
BAN逻辑框架
推理规则:
- 消息意义规则:从加密消息所使用密钥和消息中的而秘密,推断发送者身份
- 随机数验证规则:P相信X新鲜,且P相信Q曾经发送过X,则P相信Q相信X $bel(P,fresh(X))\ and \ bel(P,said(Q,X)) => bel(P,bel(Q,X))$
- 仲裁规则:扩展主体的信任
- 信念规则:信念在消息级联与分割中的一致性,以及信仰在此类操作中的传递性
- 接受规则:主体在协议运行中获取消息:P接收到消息,也就接收到消息的组成部分;收到加密消息后能读出消息原文的情况
- 新鲜规则:消息的一部分是新鲜的,则整个消息也是新鲜的;随机数验证规则;
- 传递规则:P相信Q发送过整个消息,则P相信Q发送过消息的一部分 $bel(P, said(Q, (X,Y)) \ => bel(P, said(Q, X))$
- 消息意义规则:从加密消息所使用密钥和消息中的而秘密,推断发送者身份
若干假设:
- 时间假设:区分此次协议开始的时间和过去的时间;某一观点在协议开始时成立,则当前轮次也成立;过去的观点不一定成立
- 密钥假设:密钥不能从密文推出;无密钥则不能解密;主体能够知道是否它使用正确解密密钥
- 主体假设:参与协议的主体都是诚实的
- 自身消息可识别假设:接收方能分辨消息是否是自己已发送过的
应用:
- 协议理想化预处理
- 给定初始状态和基于的假设
- 形势化协议达成的安全目标
- 由推理规则、会话事实与假设,推理
案例分析
NS协议漏洞分析
- 假定:三个主体(S的权威性),两个长期共享密钥,一个临时会话密钥,两个随机数(新鲜性);目标:完成协议后,A和B相信拥有一个仅它们和服务器知道的会话密钥
- 理想化协议
- 初始状态与假设
- 安全目标
- 逻辑证明
BAN逻辑缺陷
- 非标准的理想化协议过程,省略对推理主体信仰无用的部分——明文忽略问题
- 理想化过分依赖于分享者的直觉,原始协议和理想化协议存在语义鸿沟
- 不合理假设:主体诚实
第九章 Commsp
- 从反面寻找协议漏洞,如果找到攻击步骤,说明协议有缺陷
- CSP(communication Sequential Processes,通讯顺序进程):一种用于描述通过传递消息进行通信的并行代理(parallel agents)系统的符号