PDF《安全协议理论与方法》

bel(P,said(Q,X)) 对于私钥, bel(P,pubkey(Q,K))and sees(P,{X}k -1)=>

bel(P,said(Q,X)) 对于共享秘密有 bel(P,secret(P,X,Q))and sees(P,(X)Y)=>

bel(P,said(Q,X)) 推理规则-随机数验证规则(现时检验规则) bel(P,fresh(X)) and bel(P,said(Q,X)) =>

bel(P, bel(Q,X)) 解释:如果P相信X是新鲜的,并且P相信Q曾经 发送过X,那么P相信Q相信X. 推理规则---仲裁规则 作用:拓展主体的推知能力,使主体可以在基于其 他主体已有的信仰之上推知新的信仰. bel(P, cont(Q, X)) and bel(P, bel(Q, X)) =>

bel(P, X) 解释:如果P相信Q对X是有仲裁权的,并且P相信 Q是相信X的,那么P相信X. 推理规则---信念规则 作用:反映信念在消息的级联与分割的不同 操作中的一致性以及信仰在此类操作中的 传递性. bel(P,X) and bel(P,Y)?bel(P,(X, Y)) bel(P,(X,Y)) ? bel(P,X) OR bel(P,Y) bel(P,bel(Q,(X,Y))) ? bel(P,bel(Q,X)) or bel(P,bel(Q,Y)) 推理规则---接收规则 作用:定义了主体在协议运行中获取消息. sees(P, (X,Y)) ? sees(P, X) sees(P, Y) ? sees(P, X) bel(P, goodkey(P,K,Q)) and sees(P, {X}k)?sees(P,X) bel(P, pubkey(P,K)) and sees(P, {X}k) ?sees(P,X) bel(P, pubkey(Q,K)) and sees(P, {X}k -1) ?sees(P,X) 解释:如果P接收到一个消息,P也就收到了这个 消息的组成部分,以及P能够从中解出的消息. 推理规则---新鲜规则 bel(P, fresh(X)) ? bel(P, fresh(X,Y)) bel(P, fresh(X)) and bel(P, said(Q,X)) ? bel(P, bel(Q,X)) 解释:如果公式的一部分是新鲜的,则整个 公式也是新鲜的.以密文出现才有意义,密 文中有一部分是新鲜的,则整个部分也是新 鲜的. 推理规则---传递规则 bel(P, said(Q, (X,Y)) ? bel(P, said(Q, X)) 解释:如果P相信Q曾发送过整个消息,那么P相信Q曾发送过消息的 子部分. BAN逻辑---若干假设 时间假设 密钥假设 主体假设 自身消息可识别假设 时间假设 协议分析中区分两个时间: current-time: 起始于本次协议运行的开 始阶段. past-time: current-time之前的时间. current-time: 如果某一观点在协议开始 时是成立的,那么在整个current-time中 也是成立的.但是在past-time中成立的观 点在current-time中却并不一定成立. 密钥―主体―假设 密钥不能从密文中推导出来. 不拥有正确密钥不能解密报文. 主体能够知道他是否正确地使用了解密密 钥.正确的密钥解密得到的明文有意义, 错误的密钥解密得到的明文没有意义. 主体―假设 假设参与协议运行的主体都是 诚实的. 自身消息可识别―假设 假设接收方能分辨接收到的消 息是否为自己发送过的消息. 使得消息含义规则的成立有合 理性. 如何应用BAN逻辑 1.对协议进行理想化预处理(初始化). 2.给出协议初始状态及其所基于的假设. 3.形式化说明协议将达成的安全目标. 4.运用公理和推理规则以及协议会话事实和 假设,从协议的开始进行推证直至验证协议 是否满足其最终运行目标. 协议描述 初始化 初始假设 会话消息 BAN逻辑推理规则 协议目标 协议是不安全的 协议是安全的 应用BAN逻辑发现NS协议漏洞 1).A?S: A,B,Na 2).S?A: {Na,B,Kab,{Kab,A}Kbs}Kas 3).A?B: {Kab,A}Kbs 4).B?A: {Nb}Kab 5).A?B: {Nb-1}Kab NS协议是1978年提出的基于共享密钥体系 的协议.........