安全協(xié)議分析與設(shè)計

第五章（下）衛(wèi)劍釩NSL協(xié)議的串空間方法證明NSL協(xié)議是Lowe對NSPK協(xié)議的改進，其中A、B代表協(xié)議主體，Na、Nb分別代表A和B產(chǎn)生的隨機數(shù)，KA、KB分別代表A、B的公鑰。2定義NSL串空間先為串空間中的項代數(shù)增加兩個成員如下。主體標識集Tname：它是T的子集，包含主體的名字，如A、B等。映射Key：Tname→K，這個映射是主體到其公鑰的映射，如主體A的公鑰為Key（A），記作KA。假設(shè)該映射是單射的，即如果KA=KB，則A=B。3定義NSL串空間定義5.6當串空間Σ中只有以下3種串時，稱Σ為NSL串空間。（1）攻擊者串p。（2）發(fā)起方串t∈Init[A,B,Na,Nb]，其跡為<+{Na,A}KB,?{Na,Nb,B}KA,+{Nb}KB>，其中A、B∈Tname，Na、Nb∈T，但Na!∈Tname，串對應的主體是A。（3）響應方串s∈Resp[A,B,Na,Nb]，其跡為<?{Na,A}KB,+{Na,Nb,B}KA,?{Nb}KB>，其中A、B∈Tname，Na、Nb∈T，但Nb!∈Tname，串對應的主體是B。4證明響應方B的認證目標命題5.1設(shè)（1）Σ為NSL串空間，C是Σ中的一個叢，s是一個響應方串，滿足s∈Resp[A,B,Na,Nb]，且高度為3；（2）KA?1!∈KP；（3）Na≠Nb，Nb唯一地產(chǎn)生于Σ。則C中存在一個發(fā)起方串t∈Init[A,B,Na,Nb]，且高度為3。5為了方便，下面記節(jié)點<s,2>（即響應方串的第2個節(jié)點+{Na,Nb,B}KA）為n0；記節(jié)點<s,3>（即?{Nb}KB）為n3；記term(n0)為V0，記term(n3)為V3。后面將附加兩個節(jié)點n1和n2，使得n0<n1<n2<n3。6引理5.1為證明命題5.1，先證明一組引理。引理5.1Nb產(chǎn)生于n0。證明：因為Nb?V0，并且n0的方向為正，根據(jù)對“產(chǎn)生”的定義，只需證明對n0前的節(jié)點n'，都有Nb!?term(n')即可。由于在同一串上，V0前只有<s,1>這個節(jié)點，term(<s,1>)={Na,A}KB，只需檢驗Nb≠Na和Nb≠A即可。前者是命題5.1的假設(shè)，后者則由NSL串空間定義中Nb!∈Tname的假設(shè)直接得出。7引理5.2引理5.2S={n∈C:Nb?term(n)∧V0!?term(n)}有一個極小元n2，n2是正規(guī)節(jié)點并且方向是正的。證明：由于n3∈C，Nb?V3，V0!?V3，所以集合S是非空的，由極小元定理，S至少含有一個極小元n2，由正向定理，該極小元的符號為正。n2是否可能為一個攻擊者節(jié)點？下面用窮舉所有可能攻擊者串的辦法來驗證。對于M串，跡為<+t>，t∈T，若要成為n2，只有t=Nb才可以，但若t=Nb，則Nb產(chǎn)生在這個串上。命題5.1第3條中指出Nb唯一地產(chǎn)生于Σ，引理5.1指明了Nb產(chǎn)生于n0，所以t=Nb不可能成立。8F串缺乏正向的節(jié)點，故而不可能含有n2。T串具有<?g,+g,+g>的形式，其中的正向節(jié)點都不是S的極小元。C串具有<?g,?h,+gh>的形式，同T串一樣，其中的正向節(jié)點不是S的極小元。K串具有<+k0>的形式，k0∈Kp，Nb∈T，故Nb!?k0，所以該情況下不可能含有n2。E串具有<?k0,?h,+{h}k0>的形式，假設(shè)項為+{h}k0這個正向節(jié)點屬于集合S，則有Nb?{h}k0∧V0!?{h}k0,故而可得Nb?h，V0!?h，則?h這一點也屬于集合S，故+{h}k0這個E串中唯一的正向節(jié)點不是極小元。9D串具有<?k0?1，?{h}k0，+h>的形式，如果項為+h的這個節(jié)點是S的極小元，則有：V0!?h并且V0?{h}K0，否則項為?{h}k0的節(jié)點就是極小元了。由完善加密假設(shè)，若V0?{h}K0，則必有h={Na，Nb，B}且K0=KA，故必存在一個節(jié)點m并且term(m)=KA?1（也即D串的第1個節(jié)點），由于KA?1!∈KP，由定理5.5，KA?1產(chǎn)生于正規(guī)節(jié)點，但是，發(fā)起方串和響應方串都沒有產(chǎn)生KA?1，故S的極小元不在D串上。S的極小元不在S串上的證明略。經(jīng)過上述分析，n2并不位于攻擊者節(jié)點上，所以一定在正規(guī)節(jié)點上?！?0引理5.3引理5.3在節(jié)點n2前存在同一個串上的節(jié)點n1，并且term(n1)={Na,Nb,B}KA。證明：由引理5.1可知，Nb產(chǎn)生于n0。由于V0?term(n0)而V0!?term(n2)，所以n2不等于n0，又由于Nb唯一地產(chǎn)生于Σ，故Nb不可能產(chǎn)生于n2，根據(jù)“產(chǎn)生”的定義可知，一定有和n2同一個串上之前節(jié)點的n1，并有Nb?term(n1)。由n2的極小元特性，一定有V0?term（n1），由于沒有一個正規(guī)節(jié)點把加密項作為子項的，所以V0=term(n1)={Na,Nb,B}KA?！?1引理5.4引理5.4包含n1和n2的正規(guī)串是一個發(fā)起方串，并且包含在C中。證明：n2是一個正向的正規(guī)節(jié)點并且在一個形如{*,*,*}K的節(jié)點后，所以只可能是在發(fā)起方串上（因為在響應方串上，跟在形如{*,*,*}K的節(jié)點后的只有一個負向的節(jié)點），并且位于該串的第3個節(jié)點，根據(jù)引理5.2及“從”的定義，該串在C中，高度為3。□由引理5.3和引理5.4，可以直接得到命題5.1的證明。到這里就已經(jīng)證明了非單射一致性目標。12證明單射一致性目標命題5.2如果Σ為NSL串空間，且Na在Σ中被唯一產(chǎn)生，則對于給定的A、B和Nb，Σ中最多只有一個發(fā)起方串t∈Init[A,B,Na,Nb]。證明：如果t∈Init[A,B,Na,Nb]，t的第1個節(jié)點<t,1>是正向的，Na?term<t,1>，所以Na產(chǎn)生在<t,1>。由于Na唯一地產(chǎn)生于Σ，所以最多只可能有一個t。這就證明了NSL的單射一致認證目標。□13如果是對NSPK協(xié)議的分析對于NSPK協(xié)議的單射一致認證目標，證明是類似的，主要的區(qū)別在于引理5.3的表述應該改為：節(jié)點n2前存在同一個串上的節(jié)點n1，并且term(n1)={Na,Nb}KA。這樣的改動，導致無法證明命題5.1中的t∈Init[A,B,Na,Nb]，只能得出存在某個主體C且t∈Init[A,C,Na,Nb]。14證明NSL的保密性先證明隨機數(shù)Nb在協(xié)議運行時保密。命題5.3設(shè)（1）Σ為NSL串空間，C是Σ中的一個叢，s是一個響應方串，滿足s∈Resp[A,B,Na,Nb]；（2）KA?1!∈KP，KB?1!∈KP；（3）Na≠Nb，Nb唯一地產(chǎn)生于Σ。則對于C中的所有滿足Nb?term(m)的節(jié)點m，要么{Na,Nb,B}KA?term(m)，要么{Nb}KB?term(m)，特別地，Nb≠term(m)。15證明：記<s,3>為n3，n3的項記為V3，即V3=term(n3)，考慮集合S：S={n∈C： Nb?term(n)∧V0!?term(n)∧V3!?term(n)}如果能證明S是空集，則命題就可以得證。假設(shè)S非空，則S一定有至少一個極小元，下面引入兩個引理，如果這兩個引理能夠被證明，就可以證明本命題。引理5.5S的極小元不會是正規(guī)節(jié)點。引理5.6S的極小元不會是攻擊者節(jié)點。16引理5.5的證明引理5.5的證明：假設(shè)m是S的極小元，并且是一個正規(guī)節(jié)點，根據(jù)正向定理，m的方向為正。由于響應方串s中只有n0是正向的，但V0=term(n0)，所以n0不可能是m，也即m不會位于s上。m也不可能在其他不等于s的響應方串s'上，這是因為如果m位于s'，則m=<s',2>，所以term(m)={N,N',C}KD，由于Nb?term(m)，所以要么Nb=N，要么Nb=N'。如果Nb=N，則Nb?term(<s',1>)，term(<s',1>)={Nb,D}KC，又由于V0!?{Nb,D}KC，V3!?{Nb,D}KC。所以<s',1>∈S，而<s',1><Cm,這和m是極小元的前提矛盾。如果Nb=N'，則Nb產(chǎn)生于m，又因為Nb產(chǎn)生于n0，與Nb唯一產(chǎn)生于Σ的假設(shè)矛盾。故m不可能位于s'。故m不可能位于任何響應方串上。17現(xiàn)在來看m是否可能位于發(fā)起方串t上，由于m是正向的，所以m要么位于t的第1個節(jié)點，要么位于t的第3個節(jié)點。如果m=<t,1>，由于Nb?term(m)，所以Nb產(chǎn)生于m，這與Nb唯一產(chǎn)生于n0的假設(shè)是矛盾的。如果m位于t的第3個節(jié)點，則term(m)形如{Nb}KC，而且C≠B，因為m作為S中的點，要求滿足V3!?term(m)。那么<t,2>具有{*,Nb,C}K的形式。這樣的話，<t,2>∈S，而<t,2><Cm,這和m是極小元的前提矛盾。所以m不可能位于任何發(fā)起方串上。引理5.5證畢。18引理5.6的證明對于引理5.6的證明，幾乎等同于引理5.2的證明，主要不同的是對于D串的分析，這時需要考慮兩種情況，一種是h=(Na,Nb,B)，K0=KA的情況，一種是h=Nb,K0=KB的情況。19證明隨機數(shù)Na的保密性命題5.4設(shè)（1）Σ為NSL串空間，C是Σ中的一個叢，s是一個發(fā)起方串，滿足s∈Init[A,B,Na,Nb]；（2）KA?1!∈KP，KB?1!∈KP；（3）Na唯一地產(chǎn)生于Σ。則對于C中的所有滿足Na?term(m)的節(jié)點m，要么{Na,A}KB?term(m)，要么{Na，Nb，B}KA?term(m)，特別地，Na≠term(m)。該命題的證明與Nb的保密性證明非常相似。

20發(fā)起方的認證目標命題5.5設(shè)（1）Σ為NSL串空間，C是Σ中的一個叢，s是一個發(fā)起方串，滿足s∈Init[A,B,Na,Nb]，且高度為3；（2）KA?1!∈KP，KB?1!∈KP；（3）Na唯一地產(chǎn)生于Σ。則C中存在一個響應方串t∈Resp[A,B,Na,Nb]，且高度至少為2。21證明思路考慮集合{m∈C:{Na,Nb,B