[合同协议]安全协议理论与方法_13792.ppt

模型检测工具对协议的分析 ■对协议2的分析 认证性：对于协议一轮的运行，认证的性质是成立的。但如果A、B皆发起多个会话，认证性将不成立。攻击为： A?S: A,{Ta,B,Kab}kas S?B: {Ts, A, Kab}kbs 1’) Z(B)?S: B,{Ts,A,Kab}kbs 2’) S?Z(A): {Ts,B,Kab}kas 模型检测工具对协议的分析 1”) Z(A)?S: A, {Ts’, B, Kab}kas 2”) S?Z(B): {Ts”, A, Kab}kbs 1”中的Ts’有问题，本应为Ta。 ■秘密性： kab?KS ■在协议认证性被破坏后，存在一个攻击破坏协议的秘密性，描述为： A?Z(S): A, {Ts’, B,Kab} Z(S)?B: {Ts”, A, Kab}kbs 逻辑推证工具对协议的分析 ■协议1不能提供认证的缺陷。协议1的安全目标是：A，B双方都相信对方已拥有了M。由于没有任何签名和预共享的秘密，所以协议的目标是不能达到的。如果基于以下两个假设,通过逻辑推证其秘密性是成立的。 Believes(A, maysee(B, M)) Believes(B, maysee(A, M)) 但实际上，通过前面的证明可知协议1的秘密性是不成立的。原因 为认证的缺乏和双层加密造成的。而一般的逻辑推证工具的推理 规则不能判断由双层加密造成的秘密性缺陷。 逻辑推证工具对协议的分析 ■协议2是一个密钥交换协议，其信仰目标是： G1: believes(A, goodkey(A,Kab,B)) G2: believes(B, goodkey(A,Kab,B)) G3:believes(A, believes(B, goodkey(A,Kab,B))) G4:believes(B, believes(A, goodkey(A,Kab,B))) 逻辑推证工具对协议的分析 ■协议的基本假设为： A1: believes(A, goodkey(A, kas, S)) A2: believes(B, goodkey(B, kas, S)) A3: believes(A, fresh(Ta)) A4: believes(S, fresh(Ts)) A1: believes(S, controls(A,Kab)) 逻辑推证工具对协议的分析 推证过程略。 由假设A1,A2以及可信服务器的权限,可证明协议的G1,G2 是满足的。 但由于协议没有认证体系,S无法判断接收到的消息的确发自A以及B的确为消息的意定接收者，同理对于A,B也无法判断S的可信性，因此G3,G4是不满足的。即A、B不能得到有关对方主体相信Kab是良好的共享密钥的信仰。 混合分析技术对协议的分析 ■ML: 分析协议1 运用模型检测工具对协议进行分析,若不安全,则： 使用逻辑推证工具去判断协议的哪一个假设是导致协议遭受现实攻击的原因。 ■LM: 分析协议2 运用逻辑推证工具对协议进行分析，发现协议有漏洞以及导致此漏洞的关键性假设，则 运用模型检测工具有针对地为关键性假设构造可能的攻击路径。 混合分析技术ML对协议1的分析 ■首先用逻辑推证工具发现协议1不能提供认证的缺陷。协议1的安全目标是：A,B双方都相信对方已拥有了M。 将Z取代B，将攻击模型化为3条消息的协议。 A?Z: {M}ka Z?A: {M}ka A?Z: {M} 混合分析技术ML对协议1的分析 ■下面假设对于协议满足其安全目标是必须的： Believes(Z, maysee(A,M)) Believes(A,maysee(Z,M)) ■由于该协议没有认证功能，因此并不能肯定M是被意定的主体接收的信仰。所以很有可能M为攻击者获取，因此 混合分析技术LM对协议2的分析 ■为达到安全目标就必须修改协议或者允许服务器S使用不正确的推理规则，以及为满足安全性质，需要增加额外的假设 Believes(S, fresh(Ta)) 让攻击者Z扮演S的角色，通过模型检测工具进行自动检测可得到一个前述的对协议秘密性的攻击。 结论：认证性的缺乏将导致对消息的不恰当的解释以及不恰当的假设可引发Z对协议秘密性的攻击。 混合分析技术分析对照表 协议2 协议1 模型检测 逻辑推证 混合分析 ML LM 认证性 ? ? ? ? ? ? 秘密性 ? ? ? ?