网络安全教程 教学课件 田园 第14章 网络安全协议的分析与.pptVIP

第14章 网络安全协议的分析与验证技术 ;14.1 协议的strand-图模型 ;14.1.1 消息代数与strand-图; 两个消息式M、N之间有一种极其重要的半序关系——子项关系，记做M∠N，定义如下。 （1）M∠M （2）若M∠N则对任意的k有M∠{N}k （3）若M∠N则对任意的N1有M∠N1N、M∠NN1 ;; 若M是消息式，则+M或?M表示一个事件，分别表示发送消息M和接收消息M。 strand 是一个事件序列及一个指定的消息作用点，作用点的位置用下划线表示。 s = E1,E2,…,Ei?1,Ei,Ei+1,…,Es 称s=…,+t,…是正号的，s=…,-t,…是负号的。 s设Ei=±M，记un_term(Ei)=M。 不标记作用点位置的事件序列称做一个迹（trace）。; 设s = E1,E2,…,Ek-1,Ek,Ek+1,…,Er也是个strand，s和s 有关系ss 若E1=E1,…, Ei =Ei且 k=i+1；s和s 有关系s→s 若 i=k 且 Ei?=+M, E i?=?M。 广义strand，图是一个有向图（S，D），S是strand的一个集合，若ss 或s→s，有向边s，s∈D，并且有性质如下。 （1）若s∈S 且ss，则s∈S； （2）若s∈S，s =…, M,…, 则必有且仅有一个s∈S，s =…, +M,…，使s→s。; 定理14.1 广义strand图是无圈有向图当且仅当其中所有的消息作用点可按Lamport时序协议排成线性序。 定理14.2 strand图顶点的任何非空子集{S1,…,Sn}必存在*?极小元，即存在这样的Sk, 从任何其他的Si出发都没有能到达Sk的路径。□; 引理14.3 S是strand图G的顶点集合，具有这样的性质：若m、m∈ G且un_term(m)= un_term(m), 则m∈S当且仅当m∈S。设x*是S的极小元，则x*必是正号的。 引理14.4 G是strand图，t是给定的消息，n*是顶点集合S(t)={x∈G : t∠un_term(x)}的极小元，则n*是t的源生strand。 定理14.5 一个strand图是一棵strand树iff存在且只有一条遍历所有顶点的有向路径。;图14-1 Lamport图和strand图;14.1.2 攻击者strand;图14-2所示是这些攻击者strand的图表示。 ; 图14-3所示是对经典的Needham-Schroeder协议攻击的第一步，这里组合了一个D-strand和一个E-strand。;14.2 消息代数的理想 ; 设KK，递归地定义两个消息式M、N之间的K-子项关系如下，记做M∠KN。 （1）M∠KM。 （2）若有k0∈K使N={N0}k0且M∠KN0，则有M∠KN。 （3）若M∠KN，则对任意的N1有M∠KN1N、M∠KNN1。; 设KK ，I1⊿KL、I2⊿KL，则I1∩I2⊿KL、I1∪I2⊿KL（习题14-4），并且（习题14-5） （1）IK[H]={t: 存在h∈H使h∠Kt}。 （2）IK[H]=∪x∈HIK[x]。 （3）IK[H1∪H2]=IK[H1]∪IK[H2]。 （4）IK[H1∩H2]IK[H1]∩IK[H2]。 对K1、K2K ，恒有IK1[H]∪IK2[H]IK1∪K2[H]、IK1∩K2[H]IK1[H]∩IK2[H]。 称一个消息式M是简约的，若M≠M1M2。因此若M是简约的，则M∈T 或者M={h}K。; 引理14.6 K∈K*，SL ，对所有的s∈S，s不为形式{g}K。 如果{h}K∈IK*[S]，则必有h∈IK*[S]。 引理14.7 k∈K*，K0K ，SL ，所有的s∈S都是简约的且不为形式{g}k。 如果{h}k∈IK0[S]，则必有k∈K0。;14.3 strand-图理论的几个普遍结论 ; 定理14.11 G是一个strand图，K0=S∪K*-1，S与Kp不相交。 如果存在一个strand m∈G使un_term(m)∈IK*[S]，则必存在合法strand n∈G使n是IK*[S]的入口。 定理14.12 G是一个strand-图，K0=S∪K*-1，S与Kp不相交。 如果G的任何合法strand都不是IK*[S]的入口，那么任何形如{g}k，k∈S的消息项都不可能源生于攻击者strand。;14.4 协议的安全性质 ;14.5 协议分析的例子 ;14.5.1 Needham-Schroeder-Low