网络安全教程 田园 第14章 网络安全协议的分析与

《网络安全教程 田园 第14章 网络安全协议的分析与》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、第14章网络安全协议的分析与验证技术14.1协议的strand-图模型14.2消息代数的理想14.3strand-图理论的几个普遍结论14.4协议的安全性质14.5协议分析的例子14.1协议的strand-图模型14.1.1消息代数与strand-图14.1.2攻击者strand14.1.1消息代数与strand-图消息是一个形式表达式，为强调其形式结构今后也常称为消息表达式或消息式，其递归定义如下。（1）A∪T∪V∪K中的元素都是消息式。（2）若M、N是消息式，则M，N是消息式。（3）若M是消息式，K∈K是密钥符号，则{M}K是一个消息式。两个消息式M、N之间

2、有一种极其重要的半序关系——子项关系，记做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'=E'1,E'2,…,E''k-1,E''k

3、,E''k+1,…,E'r也是个strand，s和s'有关系s∈D，并且有性质如下。（1）若s'∈S且s

4、图顶点的任何非空子集{S1,…,Sn}必存在*−极小元，即存在这样的Sk,从任何其他的Si出发都没有能到达Sk的路径。□引理14.3S是strand图G的顶点集合，具有这样的性质：若m、m'∈G且un_term(m)=un_term(m'),则m∈S当且仅当m'∈S。设x*是S的极小元，则x*必是正号的。引理14.4G是strand图，t是给定的消息，n*是顶点集合S(t)={x∈G:t∠un_term(x)}的极小元，则n*是t的源生strand。定理14.5一个strand图是一棵strand树iff存在且只有一条遍历所有顶点的有向路径。图14-1Lampo

5、rt图和strand图14.1.2攻击者strand定义攻击者strand是有以下迹的strand之一。（1）M-strand:+t,t∈Tp，Tp是T的一个子集。（2）F-strand:-g,g∈L（3）Tee-strand:-g,+g,+g（4）C-strand:-g,-h,+gh（5）S-strand:–gh,+g,+h（6）K-strand:+K,K∈Kp,Kp是攻击者已知的密钥集合（7）E-strand:–k,–h,+{h}k,k∈K（8）D-strand:–k–1,–{h}k,+h,k–1∈Kp图14-2所示是这些攻击者strand的图表示。图14-

6、2攻击者strand图14-3所示是对经典的Needham-Schroeder协议攻击的第一步，这里组合了一个D-strand和一个E-strand。图14-3组合的攻击者strand14.2消息代数的理想L是消息代数，KK，消息代数的K±理想是一个满足以下条件的集合IL。（1）对任何h∈I、g∈L，有gh∈I和hg∈I。（2）对任何h∈I、k∈K，有{h}k∈I。设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、

7、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.6K∈K*，SL，对所有的s∈S，s不为形式{g}

8、K。如果{h}K∈IK*