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

资源描述

《安全协议理论与方法中国科学技术大学.ppt》由会员分享，可在线阅读，更多相关《安全协议理论与方法中国科学技术大学.ppt（102页珍藏版）》请在三一办公上搜索。

1、安全协议理论与方法,基于证明结构性方法,简介,推理结构性方法缺陷：不能解决秘密性，缺乏清晰的语义。攻击结构性方法缺陷：状态空间爆炸，时间与空间资源受限。,简介,Human-readable方法的特点：将重点放在明确区分主体的可信度上。运用强有力的不变式技术和攻击者知识公理使得认证过程类似于基于模型的验证方法。,主体知识及操作,可信主体：A、B、S不可信主体：Z主体间发送的消息可分为：基本消息：包括密钥K和非密钥的数据D。合成消息：包括消息对(C1,C2)和加密消息。对称密钥域记为KS，非对称密钥域记为KA。,主体知识及操作续,K=KA KSC=Ck|(C,C)|BB=K|DK=KA|KS|KS

2、-1S=C S:可被攻击者获取的消息集合。,主体知识及操作续,kK，dD，那么dC,(d,k)C,dkCd(d,k)dk涵盖三个元素知识的S中的一个元素。变量s,s,s,.,s1,s2,在S中赋值。变量k,k,k,.,k1,k2,在K中赋值。变量d,d,d,.,d1,d2,在D中赋值。,主体知识及操作续,五种基本操作：；用一个已知密钥加密一个已知数据。：用一个已知密钥解密一个已知数据。：级联两个已知数据。：分离一个数据对。:生成数据的子集合。,主体知识及操作续,ss=(s,s)|(s,c,k,s=k cs)s=s(c)k ss=(s,s)|(s,c,k,s=k-1(c)ks)s=scss=(s

3、,s)|(s,c,k,s=c1c2s)s=s(c1,c2)ss=(s,s)|(s,c,k,s=(c1,c2)s)s=sc1c2 ss=(s,s)|(s,s1.s=s1s)s=s1数据s可从数据s中生成当且仅当如果存在一个5个基本操作系列使得状态s转换到s,记为 s known_in s。,主体知识及操作续,对于,的任意子集E=x1,xn,记E 为x1xn的自反传递闭包。Known_in s 定义为：S known_in s当且仅当s,主体知识及操作续,引理5.1如果E,那么s,s,s.(sEs)(ssE ss)证明：如果对于已知的数据集合和参数集合基本操作的前置条件是满足的，那么对于s的任意子

4、集也是满足的，并且操作的应用结果是一样的。关系E 对于,的任何子集是具有融合性的，体现在：,主体知识及操作续,1)如果sEs1和sEs2,那么存在s3有sEs3和s2Es3。如果s,s,那么存在s有:s,s,ss。更为一般的，如果对于任何一个非空子集E，如果sEs,那么存在s有s Es和 ss。3)如果sis 和sjs,其中i,j,那么存在S有sjs和sis。,主体知识及操作续,推论5.1如果s,s,那么存在s有s,s 和 s,s。,主体知识及操作续known_in性质,A1c known_in sc known_in s(c,c)known_in sA2(c,c)known_in sc kn

5、own_in s c known_in sA3c known_in sk known_in sck known_in sA4ck known_in sk-1 known_in sc known_in sA5s known_in ss known_in s(ss)known_in sA6(ss)known_in s s known_in ss known_in sA7s known_in sA8 known_in s,主体知识及操作续comp_of性质,B1(c,c)comp_of sc comp_of s c comp_of sB2ck comp_of sk-1 comp_of sc comp

6、_of sB3s comp_of ss comp_of s(ss)comp_of sB4(ss)comp_of s s comp_of ss comp_of sB5s comp_of sB6 comp_of s,主体知识及操作续setofkeys性质,Setofkeys:当且仅当是密钥集合时，setofkeys(s)为真。C1(c comp_of s)(k-1 comp_of s)c ck(c comp_of sck)C2(c comp_of sc)c ck(c comp_of sck)C3(c comp_of s)c d(c comp_of sd)C4(c comp_of sc1c2)c(c

7、1,c2)(c comp_of s(c1,c2)C5(c comp_of)C6(s comp_of s)(s comp_of s)(ss comp_of s)C7 cs setofkeys(s)(c comp_of s)C8 setofkeys(s)setofkeys(s K)C9 setofkeys(),Known_in 和 comp_of 关系,D1(s known_in s)(s comp_of s)D2(b comp_of s)(b known_in s)D3(ck comp_of s)(k comp_of s)(ck known_in s)D4(ck comp_of s)(c kno

8、wn_in s)(ck known_in s)D5(c,c)comp_of s)(c known_in s)(c known_in s)(c,c)known_in s),Known_in 和 comp_of 关系续,D6(s known_in s)(c known_in s)(ss known_in s),协议形式化分析实例-NS,AS:A,BSA:E(Ks-1:kb,B)AB:E(kb:Na,A)BS:B,ASB:E(ks-1:ka,A)BA:E(Ka:Na,Nb)AB:E(Kb:Nb),Human-readable证明法对协议的分析,主体及原子行为的描述。认证属性的提出。不变式的构造。认证

9、属性的验证。,主体及原子行为的描述,SA=slave:PrincipalNA:NonceNB:NonceKB:Kat:Program AddressSB=master:PrincipalNA:NonceNB:NonceKA:Kat:Program Address,主体及原子行为的描述续,Ss=key:Principal Kat:ProgramAddress其中at 用于记录每个主体执行算法的次数。,主体及原子行为的描述续,action(SA.at,1a,SA.at)Sz=Sz(A,SA.slave)action(Ss.at,1s,Ss.at)(d1,d2)known_in Szaction(S

10、s.at,2s,Ss.at)Sz=Sz(Ss.key(d3),d3)ks-1action(SA.at,2a,SA.at)(SA.KB,SA.slave)ks-1 known_in Szaction(SA.at,3a,SA.at)Sz=Sz(SA.NA,A)SA.KBnew(SA.NA,SZ)action(SB.at,3b,SB.at)(SB.NA,SB.master)kB known _in Szaction(SB.at,4b,SB.at)Sz=Sz(B,SB.master)action(Ss.at,4s,Ss.at)(d4,d5)known_in Sz,主体及原子行为的描述续,9)actio

11、n(Ss.at,5s,Ss.at)Sz=Sz(Ss.key(d6),d6)kB-110)action(SB.at,5b,SB.at)(SBKA,B)KB-1 known_in Sz11)action(SB.at,6b,SB.at)Sz=Sz(SB.NA,SB.NB)SB.KAnew(SB.NB,Sz)12)action(SA.at,6a,SA.at)(SA.NA,SA.NB)kA known_in Sz13)action(SA.at,7a,SA.at)Sz=Sz(SA.NB)SA.KB14)action(SB.at,7b,SB.at)(SB.NB)kB known_in Sz,主体及原子行为的

12、描述续,每一种行为刻画了一个可信主体与攻击者之间的通信以及由此引起的两个主体状态变量的同时变化。Sz=SzS,此形式描述可信主体发送消息S给攻击者。S known_in Sz,描述消息S的反方向发送。攻击者发出它已知的消息:刚接收的消息,先前发送的或生成的用于误导其他主体的消息.,认证属性的提出,假设存在一个全局观察者,其任意选择两个可信主体并试图使协议保证不出现下列情况:一个主体相信他已经正确地执行了一个与另一个主体的认证会话,但另一个主体正进行其他事情或进行着完全一致的会话.主主体用A表示，从主体用B表示。,3a,3b,6b,6a,7a,7b,行为执行顺序图,认证属性描述,主主体认证属性描

13、述：每次当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的行为。,不变式的构造一,关于S的不变式一攻击者不能获知主体私钥，否则将造成协议缺陷,记为 inv0(Sz)，定义如下:Inv0(Sz)=(KA-1 known_in Sz)(KB-1 known_in Sz)(Ks-1 known_in Sz)Inv1(Sz)=(KA-1 known_in(Szrng(key)(KB-1 known_i

14、n(Szrng(key)(Ks-1 known_in(Szrng(key),不变式的构造二,A和B为他们欲通信的主体使用正确的密钥。首先描述形为(k,d)kB-1的攻击者已知的所有数据：(k,d).(k,d)kB-1 known_in Szk=key(d)则inv2(s)为：(k,d).(k,d)kB-1 known_in Srng(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,6

15、b)So.KB=key(SA.slave)Pre(at,3a)：只有当at在行为可被触发的一个状态中时状态为真。,认证属性的证明,主主体认证属性的证明证明在A的两个连续的行为3a和6a之间，至少有B的一个行为6b。证明在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_wi

16、ndow=True，那么行为6a不可能发生：SA.(SA.NA,SA.NB)KA known_in Sz此性质可用一个不变式描述为：In_window=true n.(SA.NA,n)KA known_in Sz,认证属性的证明续,通过增加SB.masterASA.NASB.NA和b.(SA.NA,b)kB known_in Szb=A当在行为6b由SB.masterA(不变式成立的必要条件是SA.NA与SB.NA不相同)触发的情况下证明不变式性质的保持时，第一个约束条件被引入;当在行为3b被触发的情况下证明不变式性质的保持时，第二个约束条件被引入。,从主体认证属性的证明,In_window=

17、true(SB.NB)kB known_in Sz)增加：SA.slaveBSB.NBSA.NB。例如如果A与其他主体C通信，那么SA.NB将不是B所期待的随机数。与上类似为使行为6a保持不变式，需有：(SA.NA,SB.NB)KA known_in Sz也即:A收到一个消息如果第一部分SA.NA是正确的，那么其第二部分一定不同于SB.NB。,从主体认证属性的证明续,但是如果SA.NA和SB.NB是不同的，那么不变式显然是不成立的。而且根据它的角色，A必须发送(SA.NA,A)kc给C，但根据假设攻击者是知道此消息的(因为除了A,B,S外任何主体都可充当攻击者的角色)。攻击者因此知道了Kc-1

18、和SA.NA,并能够发送(SA.NA,A)kc给B。由此(SA.NA,SB.NB)KA known_in Sz 和 SA.slaveB 及SB.NB=SA.NB都为真，并且7b可由A的一个不正确响应6a所触发。,从主体认证属性的证明续,由上述说明可知，协议是有缺陷的。修改之一：在消息6中增加发送者的标识。第二个约束条件变为：b.(SA.NA,SB.NB,b)kA known_in Szb=B,并行多重会话,崩溃主体在并行会话中扮演多个角色的可能。协议中的S具有这种可能。一旦A已执行了1a后，唯一能执行的行为2a，例如它不能接受3b，这意味着它作为一个从主体为其他进程开始了另一个会话；它也不能执

19、行1a，这意味着它作为主主体开始了另一个会话。它也不能执行1a，这意味着它作为主主体开始了另一个会话。,并行多重会话续,AB:NaBA:E(Kab:Na,Nb)AB:Nb协议的行为包括6步：1a,1b,2b,2a,3a,3b，并可对A、B的状态以及6个行为进行形式化描述，但是：1)断言行为的描述,需考虑新型的序列约束。2)每个主体的状态涉及多个并行会话，因此需要跟踪每个会话的内容。,并行多重会话续,描述主认证属性时仅考虑1a和2a以及B的行为1b和2b。证明不变式(Kab known_in Si)然后用反证法证明行为2b在任一会话中必须出现在由1b和2b界定的窗口内。它使用一个窗口不变式：In

20、_window=truen.(SA.NA,n)Kab known_in Si),并行多重会话续,注意2b的不同情况：2b可被A或B执行。2b由B执行时Sb.master可等价于A或不等价于A，SA.NA也可等价于SB.NA，或者不等价。如果2b由A执行，则存在问题。如果强制执行与前述协议同样的序列约束，认证属性得到满足，否则，如果A可执行并行的多重会话，那么将破坏不变式，作为从主体，A将给攻击者一个答案，即它在等待所涉及的其他并行会话。,Human-readable,若要求更为详细的协议分析时，可与基于模型检测的形式化方法交替使用。其已用于许多认证协议的分析中，验证结论可以从一个协议应用到另一

21、个协议，因为：证明法的主要工作是独立于协议的，因此是可以重用。即使是与协议相关的部分，诸如不变式的确定与证明或认证属性的形式化与证明，也不因协议不同而有重大改变，因而也是可以重用的。,Paulson归纳法,基于协议消息和事件的攻击结构方法注记的结构性证明法。Human-readable：将协议模型为4种主体。Paulson：所有可能事件路径的集合。每条路径是一个包含多轮协议通信的事件序列。主体接收到一个路径，可转发它或根据协议规则进行扩展使消息的真正发送者对此无从可知。它可以模拟所有攻击和密钥丢失。,Paulson归纳法续,秘密性：攻击者不能获知发送给其他主体的消息内容。认证性：如果一个消息表

22、现为发自主体A，那么主体A的确发送了此消息，并且消息内的随机数或事件戳将正确指示其新鲜性。借鉴了状态探测和信仰逻辑的某些方面。借鉴状态探测描述事件，第二种方法给出对所生成的消息的信仰。,Paulson归纳法概述续,协议的非形式化描述：主体A：在协议结束时只有A和B有可能知道会话密钥Kab。主体B：攻击者能得到什么？主体A：在没有A和B的长期密钥的前提下，它是不能读取证书。主体B：攻击者能够欺骗B接收与它共享的密钥？主体A：可识别的随机数的使用可阻止这一行为。,Paulson归纳法概述续,Paulson归纳法为归纳定义,每个定义列出了主体或系统可能的行为。归納规则可用于推理任意长度的有限行为

23、序列的结果。parts:用于生成消息集合的所有部分。Analz:表示使用正确密钥解密之前传递的消息。Synth:表示对消息的伪造。与信仰逻辑不同,协议的归纳验证的证明过程是详细的，协议每个安全属性都能得到证明。,Paulson归纳法概述续,1.消息主体标识：A,B,。随机数:Na,Nb,。密钥:Ka,Kb,Kab,。消息混合X,X。消息的Hash值。加密的消息Crypt KX。,Paulson归纳法概述续,2.Parts,analz 和synth 如果H表示一个主体的初始知识和一条路径中所有发送的消息，那么每个操作可从H的消息中衍生出新的消息以扩充H。Parts H通过不断地增加混合消息和加密

24、消息来从H中获得。Crypt KXparts HXparts HParts Gparts H=parts(GH),Paulson归纳法概述续,analz H通过不断地增加混合消息和可用集合中的密钥解密的消息来从H中获得。Kanalz H,那么通过监听H不能获知K。Crypt KXanalz H:K-1 analz Xanalz HAnalz Ganalz H=analz(GH)Analz Hparts H,Paulson归纳法概述续,synth H是攻击者通过不断增加主体标识，构造混合消息和用H中的密钥生成加密消息来从H中获得的。Xsynth H,KHCrypt KXsynth HKsynth

25、 HKH,Paulson归纳法概述续,3.攻击者：可以观察网络中所有通信。发送从集合synth(analz H)中衍生的欺骗消息。在模型中攻击者被视为参与协议运行的一个诚实的主体，它可以用其长期秘密密钥发送正常的协议消息，以及伪造的消息，使得它能够利用截获的密钥参与协议的运行并因此欺骗其他主体。,Paulson归纳法概述-协议模型,4.协议模型Says A B X：表示A发送消息X给B。Notes A X：表示A内部存储X。除攻击者外,主体只接收发送给它们的消息。,Paulson归纳法概述-协议模型续,Otway-Rees协议AB:M,A,B,E(Kas:Na,M,A,B)BS:M,A,B,E

26、(Kas:Na,M,A,B),E(Kbs:Nb,M,A,B)SB:M,E(Kas:Na,Kab),E(Kbs:Nb,Kab)BA:M,E(Kas:Na,Kab)服务器是常量S，A和B可为任意主体。,Paulson归纳法概述-协议模型续,协议模型化的表示：如果evs是一个路径,Na是一个新鲜的随机数,B是一个不同于S和A的主体,那么evs 将被下面事件扩展。Says AB Na,A,B,Na,A,Bka 如果路径evs包含一个事件:Says AB Na,A,B,X,Paulson归纳法概述-协议模型续,Nb是一个新鲜的随机数,并且BS,那么evs将被下面事件扩展：Says BSNa,A,B,X,

27、Nb,Na,A,Bkb发送者的标记为A,并且未在新事件中使用是因为B不知道是谁发送了消息。,Paulson归纳法概述-协议模型续,如果路径evs包含一个事件:Says BS Na,A,B,Na,A,Bka,Nb,Na,A,BkbKab 是一个新鲜密钥且BS,那么evs将被下面事件扩展：Says SB Na,Na,Kabka,Na,Kabkb服务器S并不知道消息来自何方。如果S可以用标识的主体的密钥解密消息，并得到消息的正确格式，那么它认为消息是有效的并响应B。,Paulson归纳法概述-协议模型续,如果路径evs包含两个事件:Says BSNa,A,B,X,Nb,Na,A,BkbSays SB

28、 Na,X,Nb,Kkb若AB，那么evs将被下面事件扩展:Says BA Na,X主体B收到了一个期望格式的消息,解密相应部分,检查Nb与其先前发送给服务器的随机数是否一致,并将X转发给A。另外A检查它的随即数并确认会话。,Paulson归纳法概述-标准规则,5.标准规则-3个规则：规则一：空链是一个路径。规则二：如果evs是一个路径，Xsynth(analz H)是一个伪造的消息,并且BSpy，那么evs将被下面事件扩展:Says Spy B X其中H包含过去路径中的所有消息以及攻击者的初始状态。,Paulson归纳法概述-标准规则续,规则三：如果路径evs 以及S 在一个包含Na和Nb

29、的协议轮中分配会话密钥，那么evs将被下面的事件扩展：Notes Spy Na,Nb,K,Paulson归纳法概述-归纳法,6.归纳法常规的数学归纳法为:对于每个自然数n，为证明P(n)，需证明P(0)和每个xN，证明P(x)P(suc X)。同样，对于路径集合，归纳法表明：如果P在生成路径的所有规则下是成立的，那么P(evs)对于每个路径是成立的。,Paulson归纳法概述-归纳法续,首先证明：P 是覆盖所有的空路径的。对于其他规则，必须证明断言：P(evs)P(ev#evs)其中事件ev 包含新的消息(ev#evs是用事件ev对事件evs扩展后的路径，新的事件加在一个路径之前)。,Pau

30、lson归纳法概述-规则引理,7.规则引理Xparts H H是可被攻击者获知的所有消息的集合。攻击者永远不可能持有任何主体的长期密钥，除非这些密钥开始就被假定丢失。归纳证明等同于检验协议规则和观察它们没有一个涉及长期密钥的发送。规则引理用part操作说明,易于证明。,Paulson归纳法概述-秘密性定理,8.秘密性定理定理:任何其他主体不能获知会话密钥。如果攻击者持有了一些会话密钥,它不能用它去获知其他的会话密钥。它涉及analz操作。结论：如果攻击者持有了一些会话密钥,它不能用它去获知其他的会话密钥。没有人发送Crypt Kab Kcd的消息。但遗憾的是攻击者不仅可以自己直接发送这样的消息

31、或者导致其他主体发送这样的消息。,Paulson归纳法概述-查找攻击,9.查找攻击例外：服务器可能将密钥误分配给一对不相干的主体。当A收到Otway-Rees协议的第四条消息时，它不能确保此消息来自B，且B是从S处获得。,Paulson归纳法概述-查找攻击续,AZ(B):Na,A,B,E(Kas:Na,A,B)1)ZA:Ni,Z,A,E(Kis:Na,Z,A)2)AZ(S):Ni,Z,A,E(Kis:Ni,Z,A),Na,E(Kas:Ni,Z,A)2)Z(A)S:Ni,Z,A,E(Ki:Ni,Z,A),Na,E(Kas:Ni,Z,A)3)SZ(A):Ni,E(Ki:Ni,Kia),E(Kas:

32、Nb,Kia)4)Z(B)A:Na,E(Kas:Na,Kia),Paulson归纳法概述-查找攻击续,由于Na 是由A原始生成的随机数,因此在消息2中用Na替换Na可导致A视Kia 为用于与B通信的密钥。Otway-Rees使用随机数的作用：保证新鲜性。用于绑定主体的标识。通过证明Na和Nb惟一标识消息的来源并绝对不会重合来验证协议的正确性。,Paulson归纳法的自动化的理论,主体和消息S：服务器Frendi:友好主体Spy:攻击者Datatype agent=Server|Friend nat|Spy,Paulson归纳法的自动化的理论续,Datatype msg=Agent agent|

33、Number nat(*guessable*)|Number nat(*non-guessable*)|Key key|Mapir msg msg|Hash msg|Crypt key msg,Paulson归纳法的自动化的理论续,Crypt KX=Crypt KX K=k X=X不同消息集合是不相交的。SFriend ISSpySpy Friend IFriend i Friend j当且仅当X=X时,Hash X=Hash X,Paulson归纳法的自动化的理论续,Parts的定义XH Crypt KXparts HXParts H Xparts H X,Yparts H X parts

34、H，Yparts H,Paulson归纳法的自动化的理论续,Analz H定义为基于下列规则的集合：XH Crypt KXanalz H K-1analz HXanalz H Xanalz H X,Yanalz HX analz H，Yanalz H,Paulson归纳法的自动化的理论续,synth H定义为基于下列规则的集合：Ageny Asynth H Number Nsynth H XH Xsynth HXsynth H Hash Xsynth HXsynth H,Ysynth H Xsynth H,KH X,Y synth H Crypt KXsynth H,Paulson归纳法的自动

35、化的理论续,Isabelle 说明 analz 的语法描述：Consts analz:msg setmsg setInductive“analz H”IntrsInj”XH Xanalz H”Fst“X,Yanalz HXanalz H,Yanalz H”Decrypt“Crypt KXanalz H;Key(invKey K)analz HXanalz H”,Paulson归纳法-操作管理定律,Ins X H 表示集合 set X H单调性定律幂等律等价定律,Paulson归纳法-操作管理定律续,单调性定律如果GH,那么Parts G parts HAnalz Ganalz HSynth G

36、synth H,Paulson归纳法-操作管理定律续,幂等律Parts(parts H)=parts HAnalz(analz H)=analz HSynth(synth H)=synth H,Paulson归纳法-操作管理定律续,等价定律Parts(analz H)=parts HAnalz(parts H)=parts HParts(synth H)=parts Hsynth HAnalz(synth H)=analz Hsynth HSynth(parts H)不可归约Synth(analz H)不可归约,Paulson归纳法-符号评估,partsAgent A,Nonce Na Age

37、nt A,Nonce Na,Agent A,Nonce Na它可以处理诸如：Agent A,Xins Agent A,Nonce Na H,Paulson归纳法-符号评估续,对于消息X，考虑子目标：parts(ins XH)analz(ins XH)例如：Nonce Na,Agent A,Agent B,CryptKanone Na,Agent A,Agent B则:parts(ins XH)扩展为包括所有从Nonce Na和Agent A到X的插入集合parts H中的新元素的一个表达式。,Paulson归纳法-符号评估续,完成符号评估的规则：Parts=Parts(ins(Agent A)

38、H)=ins(Agent A)(parts H)Parts(ins(Nonce N)H)=ins(Nonce N)(parts H)Parts(ins(Key K)H)=ins(Key K)(parts H)Parts(insX,YH)=insX,Y(parts(insX(ins YH)Parts(ins(Crypt KX)H)=ins(Crypt KX)(parts(ins XH)Parts(Crypt KXH)=Crypt KXparts(XH),Paulson归纳法-符号评估续,Analz 的符号评估：keyFor H=K-1|X.Crypt KXH如果密钥不是用于解密的，则KkeyFo

39、r(analz H)analz(ins(Key K)H)=ins(Key K)(analz H),Paulson归纳法-符号评估续,用于恢复在情况分析中加密消息的规则为：analz(ins(Crypt KX)H)=ins(Crypt KX)(analz(ins XH)K-1analz Hins(Crypt KX)(analz H)otherwise,Paulson归纳法-符号评估续,Synth符号集由于结果的无限性不能被评估。分析Xsynth H的假设，并假定随机数和密钥为不可猜测的。Nonce Nsynth HNonce NHKey K synth HKey KH如果Crypt KXsynt

40、h H,那么有Crypt KXH，Xsynth H和KH,Paulson归纳法-事件和攻击者知识,Says ABX 或 Notes AXIsabelle描述为：Datatype event=Says agent agent msg|Notes agent msginitState S=all lon-term keysiniState(Friend i)=Key(shrK(Friend i)iniState Spy=Key(shrK(A)|Abad其中shrK为每个主体A与服务器共享的长期密钥。,Paulson归纳法-事件和攻击者知识续,函数spies 表示攻击者在路径中能够看到的消息。Spi

41、es=initState SpySpies(Says ABX)#evs)=Xspies evs Xspies evs if AbadSpies(Notes AX)#evs)=spies evs otherwise,Paulson归纳法-事件和攻击者知识续,集合 used evs 形式化描述了新鲜性 used=B.parts(initState B)used(Says ABX)#evs)=partsXused evsused(Notes AX)#evs)=partsXused evsinitState 用于说明主体的初始知识。,归纳法对一个递归协议的分析,扩展的Otway-Rees 协议：任意数

42、目的主体，例如A与B建立连接后如果B与认证服务器连接则为Otway-Rees协议。但B也可能选择与其他主体如C等连接一个任意长的主体链。服务器生成新鲜的会话密钥Kab和kbc给每两个连接的主体。每个会话密钥封装在两个证书中发送给各主体。,A,B,C,S,A,B,Na,A,B,NaB,C Nb,A,B,NaB,C NbC,S Nc,Kcs,S,NckcKbc,B,NckcKbc,C,NbkbKab,A,NbkbKab,B,NaKa,Kbc,C,NbkbKab,A,NbkbKab,B,NaKa,Kab,B,NaKa,三个客户的递归协议,John Bull 提出的递归协议,AB:HashkaA,B,

43、Na,-BC:HashkbB,C,Nb,HashkaA,B,Na,-2)可以重复很多次，每一步都有新的消息加入，直到某个主体与服务器S执行了步骤2)。标志-表示请求的结束。,John Bull 提出的递归协议续,若申请者顺序为A、B和C,那么响应为:HashKcC,S,Nc,HashKbB,C,Nb,HashKaA,B,Na,-S响应给C5个证书：3)SC:Kcs,S,Nckc,Kbc,B,NckcKbc,C,Nbkb,Kab,A,NbkbKab,B,NaKa,John Bull 提出的递归协议续,4)CB:Kbc,C,Nbkb,Kab,A,NbkbKab,B,NaKa4)BA:Kab,B,N

44、aKa,John Bull递归协议模型,Isabelle对协议实例的描述涉及：Nil:空路径。Fake:伪造的消息。RA1-4:协议步骤。Oops:会话密钥丢失的偶然事件。Recur:路径集合。,John Bull递归协议模型续,Nil recurFake|evsrecur;BSpy;XSynth(analz(spies evs)|Says Spy B X#evs recurRA1|evs1recur;AB;AServer;Nonce NA used evs1|Says A B(HashKey(shrK A)|Agent A,Agent B,Nonce NA,Agent Server#evs1

47、A,B,Na,P,Nb是一个新鲜随机数，且BC,那么可增加事件：,John Bull递归协议模型解释续,Says BC(HashshrKBB,C,Nb,Pa)变量Xa是B看到的A的hash值，它没有验证密钥。如果A发起了一轮协议或与Pa格式相同，那么P为(-)。主体C可为服务器或其他主体。如果当前路径包含事件Says BS Pb,BS，而且如果服务器可通过请求Pb建立响应Rb，那么可增加事件：Says S B RbRb包括验证Pb的完整性，此过程是递归的，,John Bull递归协议模型解释续,服务器可将响应发给任何主体而不仅仅是主体B。如果当前路径包含两个事件：Says BC(Hashshr

50、义包含：如果Kab 是一个新鲜的密钥，那么，Crypt(shrKA)Kab,B,Na,-Kabrespond evs如果(Pa,Ra,Kab)respond evs以及Kbc是新鲜的，并且Pa=HashshrKAA,B,Na,P,那么，(HashshrKBB,C,Nb,Pa,)Crypt(shrKB)Kbc,C,Nb,Crypt(shrKB)Kab,A,Nb,Ra,Kbc)respond evs,John Bull递归协议-服务器模型续,Isabelle 自动验证工具检查此协议发现有漏洞，因为在协议的第二步中，主体B无法确知主体A的消息是新鲜的，因此协议结束时，B没有获得A在场的事实。由于攻击

展开阅读全文