《安全协议分析与设计 普通高等教育十一五 国家级规划教材 教学课件 ppt 作者 卫剑钒 陈钟 安全协议-第5章-下》由会员分享，可在线阅读，更多相关《安全协议分析与设计 普通高等教育十一五 国家级规划教材 教学课件 ppt 作者 卫剑钒 陈钟 安全协议-第5章-下（24页珍藏版）》请在金锄头文库上搜索。
1、安全协议分析与设计 第五章（下）,卫剑钒,2,NSL协议的串空间方法证明,NSL协议是Lowe对NSPK协议的改进，其中A、B代表协议主体，Na、Nb分别代表A和B产生的随机数，KA、KB分别代表A、B的公钥。,3,定义NSL串空间,先为串空间中的项代数增加两个成员如下。 主体标识集Tname：它是T的子集，包含主体的名字，如A、B等。 映射Key：TnameK，这个映射是主体到其公钥的映射，如主体A的公钥为Key（A），记作KA。假设该映射是单射的，即如果KA=KB，则A=B。,4,定义NSL串空间,定义5.6 当串空间中只有以下3种串时，称为NSL串空间。 （1）攻击者串p。 （2）发起方
2、串tInitA,B,Na,Nb，其迹为，其中A、BTname，Na、NbT，但Na!Tname，串对应的主体是A。 （3）响应方串sRespA,B,Na,Nb，其迹为，其中A、BTname，Na、NbT，但Nb!Tname，串对应的主体是B。,5,证明响应方B的认证目标,命题5.1 设 （1）为NSL串空间，C是中的一个丛，s是一个响应方串，满足sRespA,B,Na,Nb，且高度为3； （2）KA1!KP； （3）NaNb，Nb唯一地产生于。 则C中存在一个发起方串tInitA,B,Na,Nb，且高度为3。,6,为了方便，下面记节点（即响应方串的第2个节点+Na,Nb,BKA）为n0；记节点
3、（即NbKB）为n3；记term(n0)为V0，记term(n3)为V3。后面将附加两个节点n1和n2，使得n0n1n2n3。,7,引理5.1,为证明命题5.1，先证明一组引理。 引理5.1 Nb产生于n0。 证明：因为NbV0，并且n0的方向为正，根据对“产生”的定义，只需证明对n0前的节点n，都有Nb! term(n)即可。由于在同一串上，V0前只有这个节点，term()=Na,AKB，只需检验NbNa和NbA即可。前者是命题5.1的假设，后者则由NSL串空间定义中Nb!Tname的假设直接得出。,8,引理5.2,引理5.2 S=nC: Nb term(n)V0!term(n)有一个极小元
4、n2，n2是正规节点并且方向是正的。 证明：由于n3C，NbV3，V0! V3，所以集合S是非空的，由极小元定理，S至少含有一个极小元n2，由正向定理，该极小元的符号为正。 n2是否可能为一个攻击者节点？下面用穷举所有可能攻击者串的办法来验证。 对于M串，迹为，tT，若要成为n2，只有t=Nb才可以，但若t=Nb，则Nb产生在这个串上。命题5.1第3条中指出Nb唯一地产生于，引理5.1指明了Nb产生于n0，所以t=Nb不可能成立。,9,F串缺乏正向的节点，故而不可能含有n2。 T串具有的形式，其中的正向节点都不是S的极小元。 C串具有的形式，同T串一样，其中的正向节点不是S的极小元。 K串具有
5、的形式，k0Kp，NbT，故Nb!k0，所以该情况下不可能含有n2。 E串具有的形式，假设项为+hk0这个正向节点属于集合S，则有Nbhk0V0! hk0, 故而可得Nb h，V0! h，则h这一点也属于集合S，故+hk0这个E串中唯一的正向节点不是极小元。,10,D串具有的形式，如果项为+h的这个节点是S的极小元，则有：V0!h并且V0hK0，否则项为hk0的节点就是极小元了。由完善加密假设，若V0hK0，则必有h=Na，Nb，B且K0=KA，故必存在一个节点m并且term(m)=KA1（也即D串的第1个节点），由于KA1!KP，由定理5.5，KA1产生于正规节点，但是，发起方串和响应方串都
6、没有产生KA1，故S的极小元不在D串上。 S的极小元不在S串上的证明略。 经过上述分析，n2并不位于攻击者节点上，所以一定在正规节点上。 ,11,引理5.3,引理5.3 在节点n2前存在同一个串上的节点n1，并且term(n1) = Na, Nb, B KA。 证明：由引理5.1可知，Nb产生于n0。由于V0term(n0)而V0!term(n2)，所以n2不等于n0，又由于Nb唯一地产生于，故Nb不可能产生于n2，根据“产生”的定义可知，一定有和n2同一个串上之前节点的n1，并有Nbterm(n1)。由n2的极小元特性，一定有V0term（n1），由于没有一个正规节点把加密项作为子项的，所以
7、V0=term(n1)= Na, Nb, B KA。,12,引理5.4,引理5.4 包含n1和n2的正规串是一个发起方串，并且包含在C中。 证明：n2是一个正向的正规节点并且在一个形如*,*,*K的节点后，所以只可能是在发起方串上（因为在响应方串上，跟在形如*,*,*K的节点后的只有一个负向的节点），并且位于该串的第3个节点，根据引理5.2及“从”的定义，该串在C中，高度为3。 由引理5.3和引理5.4，可以直接得到命题5.1的证明。到这里就已经证明了非单射一致性目标。,13,证明单射一致性目标,命题5.2 如果为NSL串空间，且Na在中被唯一产生，则对于给定的A、B和Nb，中最多只有一个发起
8、方串tInitA, B, Na, Nb。 证明：如果tInitA, B, Na, Nb，t的第1个节点是正向的，Naterm，所以Na产生在。由于Na唯一地产生于，所以最多只可能有一个t。这就证明了NSL的单射一致认证目标。,14,如果是对NSPK协议的分析,对于NSPK协议的单射一致认证目标，证明是类似的，主要的区别在于引理5.3的表述应该改为：节点n2前存在同一个串上的节点n1，并且term(n1) = Na, Nb KA。 这样的改动，导致无法证明命题5.1中的tInitA, B, Na, Nb，只能得出存在某个主体C且tInitA, C, Na, Nb。,15,证明NSL的保密性,先证
9、明随机数Nb在协议运行时保密。 命题5.3 设 （1）为NSL串空间，C是中的一个丛，s是一个响应方串，满足sRespA,B,Na,Nb； （2）KA1!KP，KB1!KP； （3）NaNb，Nb唯一地产生于。 则对于C中的所有满足Nbterm(m)的节点m，要么Na, Nb, BKAterm(m)，要么NbKBterm(m)，特别地，Nbterm(m)。,16,证明：记为n3，n3的项记为V3，即V3=term(n3)，考虑集合S： S=nC： Nbterm(n) V0!term(n)V3!term(n) 如果能证明S是空集，则命题就可以得证。假设S非空，则S一定有至少一个极小元，下面引入两
10、个引理，如果这两个引理能够被证明，就可以证明本命题。 引理5.5 S的极小元不会是正规节点。 引理5.6 S的极小元不会是攻击者节点。,17,引理5.5的证明,引理5.5的证明：假设m是S的极小元，并且是一个正规节点，根据正向定理，m的方向为正。由于响应方串s中只有n0是正向的，但V0=term(n0)，所以n0不可能是m，也即m不会位于s上。m也不可能在其他不等于s的响应方串s上，这是因为如果m位于s，则m=，所以term(m)=N,N,CKD，由于Nbterm(m)，所以要么Nb=N，要么Nb=N。 如果Nb=N，则Nbterm()，term()=Nb,DKC，又由于V0!Nb,DKC，V
11、3!Nb,DKC。所以S，而 C m,这和m是极小元的前提矛盾。 如果Nb=N，则Nb产生于m，又因为Nb产生于n0，与Nb唯一产生于的假设矛盾。 故m不可能位于s。故m不可能位于任何响应方串上。,18,现在来看m是否可能位于发起方串t上，由于m是正向的，所以m要么位于t的第1个节点，要么位于t的第3个节点。 如果m=，由于Nbterm(m)，所以Nb产生于m，这与Nb唯一产生于n0的假设是矛盾的。 如果m位于t的第3个节点，则term(m)形如NbKC，而且CB，因为m作为S中的点，要求满足V3!term(m)。那么具有*,Nb,CK的形式。这样的话，S，而 C m,这和m是极小元的前提矛盾
12、。 所以m不可能位于任何发起方串上。引理5.5证毕。,19,引理5.6的证明,对于引理5.6的证明，几乎等同于引理5.2的证明，主要不同的是对于D串的分析，这时需要考虑两种情况，一种是h=(Na,Nb,B)，K0=KA的情况，一种是h=Nb,K0=KB的情况。,20,证明随机数Na的保密性,命题5.4 设 （1）为NSL串空间，C是中的一个丛，s是一个发起方串，满足sInitA,B,Na,Nb； （2）KA1!KP，KB1!KP； （3）Na唯一地产生于。 则对于C中的所有满足Naterm(m)的节点m，要么Na, AKBterm(m)，要么Na，Nb，BKAterm(m)，特别地，Nater
13、m(m)。 该命题的证明与Nb的保密性证明非常相似。,21,发起方的认证目标,命题5.5 设 （1）为NSL串空间，C是中的一个丛，s是一个发起方串，满足sInitA,B,Na,Nb，且高度为3； （2）KA1!KP，KB1!KP； （3）Na唯一地产生于。 则C中存在一个响应方串tRespA,B,Na,Nb，且高度至少为2。,22,证明思路,考虑集合mC:Na,Nb,BKAterm(m)。集合是非空的，因为至少是其中一个元素，所以集合有一个极小元m0，如果m0位于正规串t上，就容易证明tRespA,B,Na,Nb，且高度至少为2。反之，如果m0位于攻击者串t上，则t应该是E串，其迹为：，这违
14、背了命题5.4，即Na的保密性。 单射一致性目标的证明和命题5.2的证明类似，但需要假设NaNb。 命题5.1到命题5.5给出了NSL协议的认证性和秘密性的证明。,23,定理证明分析的局限性,定理证明类分析方法的优越性存在争议，这主要是因为协议安全性证明存在以下的几个局限BM03。 （1）目前的协议安全性证明技术无助于协议的设计，对协议做一个微小的改动，就可能需要一个全新的证明过程。 （2）协议安全性证明无法完全自动化，致使该方法的使用范围受到了一定限制。分析者需要大量的数学知识背景，证明过程中充满了数学推理，因此向一般用户的推广困难重重。 （3）在目前不计其数的安全协议中，能被证明安全性的协议寥寥无几，更糟糕的是，一些已经被证明安全的协议在后来却发现了重大的安全缺陷。这很可能意味着几乎没人对证明过程做进一步的分析和检查。,24,Wei Jianfan,Thank You !,
