安全协议理论与方法课件.ppt

1、安全协议理论与方法基于证明结构性方法简介推理结构性方法缺陷：不能解决秘密性，缺乏清晰的语义。攻击结构性方法缺陷：状态空间爆炸，时间与空间资源受限。简介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|K

2、S-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,s)|(

3、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。2)如果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性质A1 c known_in sc known_in s(c,c)known_in sA2(c,c)known_in sc known_in s c

5、known_in sA3 c known_in sk known_in sck known_in sA4 ck known_in sk-1 known_in sc known_in sA5 s known_in ss known_in s(ss)known_in sA6(ss)known_in s s known_in ss known_in sA7 s known_in sA8 known_in s主体知识及操作续comp_of性质B1(c,c)comp_of sc comp_of s c comp_of sB2 ck comp_of sk-1 comp_of sc comp_of sB3

6、s comp_of ss comp_of s(ss)comp_of sB4(ss)comp_of s s comp_of ss comp_of sB5 s 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(c1,c2)(c

7、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 known_in s)(

8、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)协议形式化分析实例-NS1)AS:A,B2)SA:E(Ks-1:kb,B)3)AB:E(kb:Na,A)4)BS:B,A5)SB:E(ks-1:ka,A)6)BA:E(Ka:Na,Nb)7)AB:E(Kb:Nb)Human-readable证明法对协议的分析1)主体及原子行为的描述。2)认证属性的提出。3)不变式

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

10、action(Ss.at,2s,Ss.at)Sz=Sz(Ss.key(d3),d3)ks-14)action(SA.at,2a,SA.at)(SA.KB,SA.slave)ks-1 known_in Sz5)action(SA.at,3a,SA.at)Sz=Sz(SA.NA,A)SA.KBnew(SA.NA,SZ)6)action(SB.at,3b,SB.at)(SB.NA,SB.master)kB known _in Sz7)action(SB.at,4b,SB.at)Sz=Sz(B,SB.master)8)action(Ss.at,4s,Ss.at)(d4,d5)known_in Sz主体

11、及原子行为的描述续9)action(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 know

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

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的行为。不变式的构造一(1)关于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

14、 known_in(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.

15、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两个行为，并且是以正确的顺序和正确的值进行的。3)引入变量：in_window=false4)证明:如果SA.slave=B 与3a一起执行，3a将置in_window=True;5)如果SA.slave=B 与6a一起执行，6a将置6)in_window=False；认证属性

16、的证明续现在证明如果in_window=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被触发的情况下证明不变式性质的保持时，第二个约束条件被引入。从主体认证属性的证

17、明In_window=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外任何主体都可充当攻击者的角色)。攻击者

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

20、它使用一个窗口不变式：In_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、一个协议应用到另一个协议，因为：1)证明法的主要工作是独立于协议的，因此是可以重用。2)即使是与协议相关的部分，诸如不变式的确定与证明或认证属性的形式化与证明，也不因协议不同而有重大改变，因而也是可以重用的。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 HPaulson归纳法概述续synth H是攻击者通过不断增加主体标识，构造混合消息和用H中的密钥生成加密消息来从H中获得的。Xsynth H,KHCrypt KXsynth HKsynth H

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

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

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

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

29、路径evs 以及S 在一个包含Na和Nb的协议轮中分配会话密钥，那么evs将被下面的事件扩展：Notes Spy Na,Nb,KPaulson归纳法概述-归纳法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扩展后的路径，新的

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

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

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

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

34、ts H X,Yparts H X parts H，Yparts HPaulson归纳法的自动化的理论续Analz H定义为基于下列规则的集合：XH Crypt KXanalz H K-1analz HXanalz H Xanalz H X,Yanalz HX analz H，Yanalz HPaulson归纳法的自动化的理论续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 KXs

35、ynth HPaulson归纳法的自动化的理论续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(1)单调性定律(2)幂等律(3)等价定律Paulson归纳法-操作管理定律续(1)单调性定律(2)如果GH,那么(3)Part

36、s G parts H(4)Analz Ganalz H(5)Synth Gsynth HPaulson归纳法-操作管理定律续(2)幂等律(3)Parts(parts H)=parts H(4)Analz(analz H)=analz H(5)Synth(synth H)=synth HPaulson归纳法-操作管理定律续(3)等价定律(4)Parts(analz H)=parts H(5)Analz(parts H)=parts H(6)Parts(synth H)=parts Hsynth H(7)Analz(synth H)=analz Hsynth H(8)Synth(parts H)

37、不可归约(9)Synth(analz H)不可归约Paulson归纳法-符号评估 partsAgent A,Nonce Na Agent A,Nonce Na,Agent A,Nonce Na它可以处理诸如：Agent A,Xins Agent A,Nonce Na HPaulson归纳法-符号评估续对于消息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

38、中的新元素的一个表达式。Paulson归纳法-符号评估续完成符号评估的规则：Parts =Parts(ins(Agent A)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归纳法

39、-符号评估续Analz 的符号评估：keyFor H=K-1|X.Crypt KXH如果密钥不是用于解密的，则KkeyFor(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)otherwisePaulson归纳法-符号评估续Synth符号集由于结果的无限性不能被评估。分析Xsynth H的假设，并假定随机数和密钥为不可猜测

40、的。Nonce Nsynth HNonce NHKey K synth HKey KH如果Crypt KXsynth H,那么有Crypt KXH，Xsynth H和KHPaulson归纳法-事件和攻击者知识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与服务器共享的

41、长期密钥。Paulson归纳法-事件和攻击者知识续函数spies 表示攻击者在路径中能够看到的消息。Spies=initState SpySpies(Says ABX)#evs)=Xspies evs Xspies evs if AbadSpies(Notes AX)#evs)=spies evs otherwisePaulson归纳法-事件和攻击者知识续集合 used evs 形式化描述了新鲜性 used=B.parts(initState B)used(Says ABX)#evs)=partsXused evsused(Notes AX)#evs)=partsXused evsinitSt

42、ate 用于说明主体的初始知识。归纳法对一个递归协议的分析扩展的Otway-Rees 协议：任意数目的主体，例如A与B建立连接后如果B与认证服务器连接则为Otway-Rees协议。但B也可能选择与其他主体如C等连接一个任意长的主体链。服务器生成新鲜的会话密钥Kab和kbc给每两个连接的主体。每个会话密钥封装在两个证书中发送给各主体。ABCSA,B,NaA,B,NaB,C NbA,B,NaB,C NbC,S NcKcs,S,NckcKbc,B,NckcKbc,C,NbkbKab,A,NbkbKab,B,NaKaKbc,C,NbkbKab,A,NbkbKab,B,NaKaKab,B,NaKa三个客

43、户的递归协议John Bull 提出的递归协议1)AB:HashkaA,B,Na,-2)BC:HashkbB,C,Nb,HashkaA,B,Na,-3)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,NaKaJohn Bull 提出的递归协议续4)CB:Kbc,C

44、,Nbkb,Kab,A,NbkbKab,B,NaKa4)BA:Kab,B,NaKaJohn 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,

45、Agent B,Nonce NA,Agent Server#evs1 recurRA2|evs2recur;BC;Nonce NB used evs2;John Bull递归协议模型续 Says A B PAset evs2|Says BC(HashKey(shrk B)|Agent A,Agent C,Nonce NB,PA|)#evs2 recurRA3|evs3recur;BServer;Says B Server PBset evs3;(PB,RB,K)respond evs3|Says Server B RB#evs3recurJohn Bull递归协议模型续RA4|evs4recu

46、r;AB;Says BC|XH,Agent B,Agent C,Nonce NB,XA,Agent A,Agent B,Nonce NA,P|set evs4;Says CB|Crypt(shrKB)|Key KBC,Agent C,Nonce NB|,Crypt(shrk B)|Key KAB,Agent A,Nonce NB|,RA|evs4|Says B A RA#evs4recurJohn Bull递归协议模型解释1)如果在当前路径中，Na是一个新鲜的随机数以及B是一个不同于A和S的主体，那么可增加事件：2)Says A B(HashshrKAA,B,Na,-)3)A的长期密钥为 sh

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

48、主体而不仅仅是主体B。4)如果当前路径包含两个事件：5)Says BC(HashshrKBB,C,Nb,Pa)6)Says CB Crypt(shrKB)Kbc,C,Nb,Crypt(shrKB)Kab,A,Nb,R7)以及AB，那么可增加事件：8)Says B A R9)B解密两个证书，将其中的随机数与Nb进行比较，并转发其余证书(R)。John Bull递归协议-服务器模型One|AServer;Key KABused evs|(HashKey(shrKA)|Agent A,Agent B,Nonce NA,Agent Server|),|Crypt(shrKA)|Key KAB,Agen

49、t B,Nonce NA|,Agent Server|,KAB)respond evsCons|(PA,RA,KAB)respond evs;Key KBCused evs;Key KBCpartsRA;John Bull递归协议-服务器模型续PA=HashKey(shrKA)|Agent A,Agent B,Nonce NA,P|；BServer|(HashKey(shrKB)|Agent A,Agent C,Nonce NB,PA|,Crypt(shrKB)|Key KBC,Agent C,Nonce NB|,Crypt(shrK B)|Key KAB,Agent A,Nonce NB|,

50、RA|,KBC)respond evsJohn Bull递归协议-服务器模型续上面的归纳定义包含：1)如果Kab 是一个新鲜的密钥，那么，2)Crypt(shrKA)Kab,B,Na,-Kabrespond evs2)如果(Pa,Ra,Kab)respond evs以及Kbc是新鲜的，并且Pa=HashshrKAA,B,Na,P,那么，3)(HashshrKBB,C,Nb,Pa,)4)Crypt(shrKB)Kbc,C,Nb,5)Crypt(shrKB)Kab,A,Nb,Ra,Kbc)respond evsJohn Bull递归协议-服务器模型续Isabelle 自动验证工具检查此协议发现有漏