安全协议理论与方法-中国科学技术大学

安全协议理论与方法基于证明结构性方法简介推理结构性方法缺陷：不能解决秘密性，缺乏清晰的语义。攻击结构性方法缺陷：状态空间爆炸，时间与空间资源受限。简介Human-readable方法的特点：1.将重点放在明确区分主体的可信度上。2.运用强有力的不变式技术和攻击者知识公理使得认证过程类似于基于模型的验证方法。主体知识及操作可信主体：A、B、S不可信主体：Z主体间发送的消息可分为：1)基本消息：包括密钥K和非密钥的数据D。2)合成消息：包括消息对(C1,C2)和加密消息。3)对称密钥域记为KS，非对称密钥域记为KA。主体知识及操作续K=KAKSC=Ck|(C,C)|BB=K|DK=KA|KS|KS-1S=CS:可被攻击者获取的消息集合。主体知识及操作续kK，dD，那么dC,(d,k)C,dkCd(d,k)dk涵盖三个元素知识的S中的一个元素。变量s,s’,s’’,..,s1,s2,…在S中赋值。变量k,k’,k’’,..,k1,k2,…在K中赋值。变量d,d’,d’’,..,d1,d2,…在D中赋值。主体知识及操作续五种基本操作：；用一个已知密钥加密一个已知数据。’：用一个已知密钥解密一个已知数据。：级联两个已知数据。’：分离一个数据对。:生成数据的子集合。主体知识及操作续ss’={(s,s’)|(s’’,c,k,s=kcs’’)s’=s(c)k}s’s’={(s,s’)|(s’’,c,k,s=k-1(c)ks’’)s’=sc}ss’={(s,s’)|(s’’,c,k,s=c1c2s’’)s’=s(c1,c2)}s’s’={(s,s’)|(s’’,c,k,s=(c1,c2)s’’)s’=sc1c2}ss’={(s,s’)|(s’’,s1.s=s1s’’)s’=s1数据s’可从数据s中生成当且仅当如果存在一个5个基本操作系列使得状态s转换到s’,记为s’known_ins。主体知识及操作续对于{,’,,’,}的任意子集E={x1,…,xn},记E为x1…xn的自反传递闭包。Known_ins定义为：S’known_ins当且仅当s{,’,,’,}主体知识及操作续引理5.1如果E{,’,,’,},那么s,s’,s’’.(sEs’)(ss’’Es’s’’)证明：如果对于已知的数据集合和参数集合基本操作的前置条件是满足的，那么对于s的任意子集也是满足的，并且操作的应用结果是一样的。关系E对于{,’,,’,}的任何子集是具有融合性的，体现在：主体知识及操作续1)如果sEs1和sEs2,那么存在s3有sEs3和s2Es3。2)如果s{,’,,’,}s’,那么存在s’’有:s{,’,,’,}s’’,s’’{}s’。更为一般的，如果对于任何一个非空子集E，如果sE{}s’,那么存在s’’有sEs’’和s’’{}s’。3)如果sis’’和s’’js’,其中i{,},j{’,’},那么存在S’’’有s{j}s’’’和s’’’is’。主体知识及操作续推论5.1如果s{,’,,’,}s’,那么存在s’’有s{’,’}s’’和s’’{,’}s’。主体知识及操作续—known_in性质A1cknown_insc’known_ins(c,c’)known_insA2(c,c’)known_inscknown_insc’known_insA3cknown_inskknown_insckknown_insA4ckknown_insk-1known_inscknown_insA5s’known_inss’’known_ins(s’s’’)known_insA6(s’s’’)known_inss’known_inss’’known_insA7sknown_insA8known_ins主体知识及操作续—comp_of性质B1(c,c’)comp_ofsccomp_ofsc’comp_ofsB2ckcomp_ofsk-1comp_ofsccomp_ofsB3s’comp_ofss’’comp_ofs(s’s’’)comp_ofsB4(s’s’’)comp_ofss’comp_ofss’’comp_ofsB5scomp_ofsB6comp_ofs主体知识及操作续setofkeys性质Setofkeys:当且仅当是密钥集合时，setofkeys(s)为真。C1(ccomp_ofs)(k-1comp_ofs)cck’(ccomp_ofsck’)C2(ccomp_ofsc’)cck’(ccomp_ofsck’)C3(ccomp_ofs)cd(ccomp_ofsd)C4(ccomp_ofsc1c2)c(c1,c2)(ccomp_ofs(c1,c2))C5(ccomp_of)C6(s’comp_ofs)(s’’comp_ofs)(s’s’’comp_ofs)C7cssetofkeys(s)(ccomp_ofs)C8setofkeys(s)setofkeys(sK)C9setofkeys()Known_in和comp_of关系D1(s’known_ins)(s’comp_ofs)D2(bcomp_ofs)(bknown_ins)D3(ckcomp_ofs)(kcomp_ofs)(ckknown_ins)D4(ckcomp_ofs)(cknown_ins)(ckknown_ins)D5((c,c’)comp_ofs)((cknown_ins)(c’known_ins))((c,c’)known_ins)Known_in和comp_of关系续D6(sknown_ins’’)(c’known_ins’’))(ss’known_ins’’)协议形式化分析实例-NS1)AS:A,B2)SA:E(Ks-1:kb,B)3)AB:E(kb:Na,A)4)BS:B,A5)SB:E(ks-1:ka,A)6)BA:E(Ka:Na,Nb)7)AB:E(Kb:Nb)Human-readable证明法对协议的分析1)主体及原子行为的描述。2)认证属性的提出。3)不变式的构造。4)认证属性的验证。主体及原子行为的描述SA=slave:PrincipalNA:NonceNB:NonceKB:Kat:ProgramAddressSB=master:PrincipalNA:NonceNB:NonceKA:Kat:ProgramAddress主体及原子行为的描述续Ss=key:PrincipalKat:ProgramAddress其中at用于记录每个主体执行算法的次数。主体及原子行为的描述续1)action(SA.at,1a,S’A.at)S’z=Sz(A,S’A.slave)2)action(Ss.at,1s,Ss’.at)(d1,d2)known_inSz3)action(Ss.at,2s,S’s.at)S’z=Sz(Ss.key(d3),d3)ks-14)action(SA.at,2a,S’A.at)(S’A.KB,SA.slave)ks-1known_inSz5)action(SA.at,3a,S’A.at)S’z=Sz(S’A.NA,A)SA.KBnew(S’A.NA,SZ)6)action(SB.at,3b,S’B.at)(S’B.NA,S’B.master)kBknown_inSz7)action(SB.at,4b,S’B.at)Sz’=Sz(B,SB.master)8)action(Ss.at,4s,S’s.at)(d4,d5)known_inSz主体及原子行为的描述续9)action(Ss.at,5s,S’s.at)S’z=Sz(Ss.key(d6),d6)kB-110)action(SB.at,5b,S’B.at)(S’BKA,B)KB-1known_inSz11)action(SB.at,6b,S’B.at)Sz’=Sz(SB.NA,S’B.NB)SB.KAnew(S’B.NB,Sz)12)action(SA.at,6a,S’A.at)(SA.NA,S’A.NB)kAknown_inSz13)action(SA.at,7a,S’A.at)Sz’=Sz(SA.NB)SA.KB14)action(SB.at,7b,S’B.at)(SB.NB)kBknown_inSz主体及原子行为的描述续每一种行为刻画了一个可信主体与攻击者之间的通信以及由此引起的两个主体状态变量的同时变化。1)Sz’=SzS,此形式描述可信主体发送消息S给攻击者。2)Sknown_inSz,描述消息S的反方向发送。攻击者发出它已知的消息:刚接收的消息,先前发送的或生成的用于误导其他主体的消息.认证属性的提出假设存在一个全局观察者,其任意选择两个可信主体并试图使协议保证不出现下列情况:一个主体相信他已经正确地执行了一个与另一个主体的认证会话,但另一个主体正进行其他事情或进行着完全一致的会话.主主体用A表示，从主体用B表示。3a3b6b6a7a7b行为执行顺序图认证属性描述主主体认证属性描述：每次当A执行完一轮会话3a,6a,7a时，B必须完成3b,6b以及此后的7b,且其对应的值与3a,6a,7a一致。及行为的次序为：3a,3b,6b,6a,7a,7b。从主体认证属性描述：每次当B执行完一轮会话3b,6b,7b时，A必须完成3a,6a以及7a的行为。不变式的构造一(1)关于S的不变式一攻击者不能获知主体私钥，否则将造成协议缺陷,记为inv0(Sz)，定义如下:Inv0(Sz)=(KA-1known_inSz)(KB-1known_inSz)(Ks-1known_inSz)Inv1(Sz)=(KA-1known_in(Szrng(key)))(KB-1known_in(Szrng(key)))(Ks-1known_in(Szrng(key)))不变式的构造二A和B为他们欲通信的主体使用正确的密钥。首先描述形为(k,d)kB-1的攻击者已知的所有数据：(k,d).(k,d)kB-1known_inSzk=key(d)则inv2(s)为：(k,d).(k,d)kB-1known_inSrng(key))k=key(d)关于A和B的不变式主体A(或B)必须使用正确的从主体(主主体)的密钥，并且不能是攻击者可用于误导主体的密钥。1A:(pre(SA.at,3a)pre(SA.at,7a))So.kB=key(SA.slave)1B:(pre(SB.at,6b)So.KB=key(SA.slave)Pre(at,3a)：只有当at在行为可被触发的一个状态中时状态为真。认证属性的证明(1)主主体认证属性的证明1)证明在A的两个连续的行为3a和6a之间，至少有B的一个行为6b。2)证明在3a和6b之间存在一个对应的持有与3a同样消息的3b。这证明了B至少进行了3b和6b两个行为，并且是以正确的顺序和正确的值进行的。引入变量：in_window=false证明:如果SA.slave=B与3a一起执行，3a将置in_window=True;如果SA.slave=B与6a一起执行，6a将置in_window=False；认证属性的证明续现在证明如果in_window=True，那么行为6a不可能发生：S’A.(SA.NA,S’A.NB)KAknown_inSz此性质可用一个不变式描述为：In_window=truen..(SA.NA,n)KAknown_inSz认证属性的证明续通过增加SB