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

安全协议理论与方法 基于推理的结构性方法 逻辑类分析方法简介 逻辑:运用形式化方法研究和判定推理形式有效性.

形式化方法:将一套特制的人工符号应用于演绎 体系以使其严格化、精确化的研究方法.包含符号 化和系统化. 符号化:将命题(p,q,r)和常项(如命题连接词)用 符号(可重复和可辨认的标记)表示. 系统化:在符号化的基础上将一定范围内所有有 效的推理形式构成一个形式系统. 逻辑类分析方法简介 狭义形式系统:形式语言和演绎装置. 形式语言:系统的初始符号(字母表),形成规则 (如何使用符号组成公式). 演绎装置:包括定义、公理和规则. 广义形式系统:增加语义部分.即对初始符号、 公式和规则的解释.解释可把形式系统与一定模型 (代表客观实际)连接起来,从而赋予初始符号和公 式一定的实际意义. 逻辑--推理结构性方法简介 推理结构性方法:运用逻辑系统从用户接收和发送 的消息出发,通过一系列的推理公理推证协议是否 满足其安全说明. 基于知识:if you know P, then P is true. 基于信仰:不关心P的正确与否. 推理公理:从已知知识或信仰推出新知识或信仰. 典型:BAN逻辑、Kailer逻辑、RV逻辑. 逻辑--推理结构性方法简介 公式:具有一定形成规则,解释后有意义的符号串. 定理:表示系统内的重言式(或称永真式). 规则:变形规则.从已有定理产生其他定理的方法. 从A得出B 或者 若A,则B .A=>

B. 蕴含: 若…,则… 关系: 实质蕴含 简称 蕴含 ,记为 A?B ? ((not A) or B). 含义:不是通常逻辑思考中的充分条件关系. 误解: 伦敦不在英国 蕴含 巴黎在法国 . 逻辑--推理结构性方法特点 1: 简洁直观,易于使用.相对于以后所讲的其他形 式化分析方法. 2: 理想化方法.由于相同的消息在不同的协议中可 能代表不同的含义,因此分析协议之前必须对协议 进行形式化处理,即用逻辑语言描述.具体的形式 化方法没有给出,靠人的经验. 3: 使用假设和推理规则. 假设不正确,不能得到正确的信念;

公理和推理规则是否合理和完备也影响性能. BAN逻辑系统 定义:基于主体知识和信念推理的模态逻辑. 过程:通过推导主体是否能够从接收到的消息中 获得信念来判断协议是否能够达到认证目标. 1.首先给出一套形式化标记方法,用于对协议消 息、初始假设、推理规则和主体信念进行描述. 2.在公理和推理规则的作用下,从协议的初始假 设和消息中蕴含的公式推导出主体的信念,来判断 协议是否满足既定的目标. BAN逻辑系统 消息描述:用形式化方法对协议消息进行描述. 初始假设:对协议外部特性的一些假设,如对可 信第三方的信任假设,对共享密钥安全性的假设, 对随机数新鲜性的假设等. 推理规则:逻辑类分析方法的核心. 主体信念:表明了主体对信念的理解,是逻辑分 析方法的结果. BAN逻辑系统---所用符号 A,B,S等:泛指参与协议的主体. Kab,kbs,kas:主体之间的共享密钥. Ka,kb,ks: 代表主体的公开密钥. Ka-1,kb-1,ks-1: 代表对应主体的秘密密钥. Na,Nb,Ns: 代表主体各自生成的用于确认新 鲜性的随机数Nonce. P,Q.R: 代表主体变量. X,Y: 代表公式变量. K:代表密钥变量. BAN逻辑系统---所用符号 sees(P,X)(P sees X): P接收到X. said(P,X)(P said X): P发送X. cont(P,X)(P cont X): P拥有对X正确与否的判决权. fresh(X)(#X): X是新鲜的. skey(P,K,Q)(SharedKey(K,P,Q)):K是PQ共享密钥. goodkey(P,K,Q):K是PQ共享的良好密钥. pubkey(P, K)(PK(K,P)): K是P的公开密钥. secret(P,X,Q)(sec(X,P,Q):X是P和Q的共享秘密. {X}k: 用密钥K加密X得到的结果. Y:X和Y的组合,Y是P和Q之间的秘密. P bel X: P相信X. BAN逻辑---推理规则 消息意义规则 随机数验证规则 仲裁规则 信念规则 接收规则 新鲜规则 传递规则 推理规则---消息意义规则 从加密消息所使用密钥以及消息中包含的秘密 来推断消息发送者的身份(假设P和Q为不同的主体) 对于共享密钥,bel(P,goodkey(P,K,Q))and sees(P,{X}k)=>