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

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

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

2、非对称密钥域记为KA。,主体知识及操作可信主体：A、B、S,主体知识及操作续,K=KA KSC=Ck | (C,C) | BB=K | DK=KA |KS | KS-1S=C S : 可被攻击者获取的消息集合。,主体知识及操作续K=KA KS,主体知识及操作续,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中赋值。,主体知识及操作续kK， dD，那么dC, (d,k),主体知识及操作续,五种基本操作：；用一个已知密钥加密

3、一个已知数据。：用一个已知密钥解密一个已知数据。：级联两个已知数据。：分离一个数据对。:生成数据的子集合。,主体知识及操作续五种基本操作：,主体知识及操作续,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)| (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。,主

4、体知识及操作续ss=(s,s)| (s,c,主体知识及操作续,对于, 的任意子集E=x1,xn, 记E 为x1xn的自反传递闭包。Known_in s 定义为：S known_in s当且仅当s , ,主体知识及操作续对于, 的任意子集E,主体知识及操作续,引理5.1如果E , , 那么s,s,s. (sEs) (ssE ss)证明：如果对于已知的数据集合和参数集合基本操作的前置条件是满足的，那么对于s的任意子集也是满足的，并且操作的应用结果是一样的。 关系E 对于, 的任何子集是具有融合性的，体现在：,主体知识及操作续引理5.1如果E ,主体知识及操作续,1)如果sEs1和sEs2,那么存在

5、s3有sEs3和s2Es3。如果s , s, 那么存在s有: s , s, ss。更为一般的，如果对于任何一个非空子集E，如果sEs, 那么存在s有s Es和 ss。 3) 如果sis 和sjs, 其中i, , j, ,那么存在S有sjs和sis。,主体知识及操作续1)如果sEs1和sEs2,那么存在s,主体知识及操作续,推论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 known_in s c know

6、n_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,主体知识及操作续known_in性质A1c known,主体知识及操作续comp_of性质,B1(c,c) comp_of sc comp_of s c comp_of sB2ck comp_of sk-1

7、 comp_of sc comp_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,主体知识及操作续comp_of性质,主体知识及操作续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

8、s)c d (c comp_of sd)C4 (c comp_of sc1c2)c(c1,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(),主体知识及操作续setofkeys性质Setofkeys:,Known_in 和 comp_of 关系,D1(s known_in s) (s comp_of s)D2(b comp_of

9、 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) (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 关系D1(s k,Known_in 和 comp_of 关系续,D6 ( s known_in s) (c known_in s) (ss known_in s),Known_in 和 comp_of 关

10、系续,协议形式化分析实例-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),协议形式化分析实例-NSAS:A,B,Human-readable证明法对协议的分析,主体及原子行为的描述。认证属性的提出。不变式的构造。认证属性的验证。,Human-readable证明法对协议的分析,主体及原子行为的描述,SA= slave: PrincipalNA:NonceNB:NonceKB:Kat:Program AddressSB= master: PrincipalNA:No

11、nceNB:NonceKA:Kat:Program Address,主体及原子行为的描述SA= slave: Princip,主体及原子行为的描述续,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(Ss.at, 2s, Ss.at)Sz=Sz(Ss.key(d3),d3)ks-1action(SA.a

12、t, 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,主体及原子行为的描述续action(SA.at, 1a, S,主体及原子行为的描述续,9)action(Ss.at,

13、 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,主体

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

15、进行着完全一致的会话.主主体用A表示，从主体用B表示。,认证属性的提出假设存在一个全局观察者,其任意选择两个可信主体,3a,3b,6b,6a,7a,7b,行为执行顺序图,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的行为。,认证属性描述主主体认证属性描述：,不变式的构造一,关于S的不变式一攻击者不能获知主体私钥，

16、否则将造成协议缺陷,记为 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_in (Szrng(key)(Ks-1 known_in (Szrng(key),不变式的构造一关于S的不变式一,不变式的构造二,A和B为他们欲通信的主体使用正确的密钥。首先描述形为(k,d)kB-1的攻击者已知的所有数据：(k,d).(k,d)kB-1 known_in Szk=key(d)则inv2(s)为：(k

17、,d).(k,d)kB-1 known_in Srng(key)k=key(d),不变式的构造二A和B为他们欲通信的主体使用正确的密钥。首先描,关于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在行为可被触发的一个状态中时状态为真。,关于A和B的不变式主体A(或B)必须使用正确的从主体(主主体,认证属性的证明,主主体认证属性的证明证

18、明在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_window=True，那么行为6a不可能发生：SA.(SA.NA, SA.NB)KA known_in Sz此性

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

20、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。,从主体认证属性的证明In_window=true(SB,从主体认证属性的证明续,但是如果SA.NA和SB.NB是不同的，那么不变式显然是不成立的。而且根据它的角色，A必须发送(SA.NA, A)kc给C，但根据假设攻击者是知道此消息的(因

21、为除了A,B,S外任何主体都可充当攻击者的角色)。攻击者因此知道了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所触发。,从主体认证属性的证明续但是如果SA.NA和SB.NB是不同的,从主体认证属性的证明续,由上述说明可知，协议是有缺陷的。修改之一：在消息6中增加发送者的标识。第二个约束条件变为：b.(SA.NA, SB.NB, b)kA known_in Szb=B,从主体认证属性的证明续由上述说明可知，协议是有缺陷的。,并行多

22、重会话,崩溃主体在并行会话中扮演多个角色的可能。协议中的S具有这种可能。一旦A已执行了1a后，唯一能执行的行为2a，例如它不能接受3b，这意味着它作为一个从主体为其他进程开始了另一个会话；它也不能执行1a，这意味着它作为主主体开始了另一个会话。它也不能执行1a，这意味着它作为主主体开始了另一个会话。,并行多重会话崩溃主体在并行会话中扮演多个角色的可能。协议中的,并行多重会话续,AB:NaBA:E(Kab: Na, Nb)AB:Nb协议的行为包括6步：1a,1b,2b,2a,3a,3b，并可对A、B的状态以及6个行为进行形式化描述，但是：1)断言行为的描述,需考虑新型的序列约束。2)每个主体的状

23、态涉及多个并行会话，因此需要跟踪每个会话的内容。,并行多重会话续AB:Na,并行多重会话续,描述主认证属性时仅考虑1a和2a以及B的行为1b和2b。证明不变式 (Kab known_in Si)然后用反证法证明行为2b在任一会话中必须出现在由1b和2b界定的窗口内。它使用一个窗口不变式：In_window=truen.(SA.NA,n)Kab known_in Si),并行多重会话续描述主认证属性时仅考虑1a和2a以及B的行为1,并行多重会话续,注意2b的不同情况：2b可被A或B执行。2b由B执行时Sb.master可等价于A或不等价于A，SA.NA也可等价于SB.NA，或者不等价。如果2b由

24、A执行，则存在问题。如果强制执行与前述协议同样的序列约束，认证属性得到满足，否则，如果A可执行并行的多重会话，那么将破坏不变式，作为从主体，A将给攻击者一个答案，即它在等待所涉及的其他并行会话。,并行多重会话续注意2b的不同情况：,Human-readable,若要求更为详细的协议分析时，可与基于模型检测的形式化方法交替使用。其已用于许多认证协议的分析中，验证结论可以从一个协议应用到另一个协议，因为：证明法的主要工作是独立于协议的，因此是可以重用。即使是与协议相关的部分，诸如不变式的确定与证明或认证属性的形式化与证明，也不因协议不同而有重大改变，因而也是可以重用的。,Human-readabl

25、e若要求更为详细的协议分析时，可与,Paulson归纳法,基于协议消息和事件的攻击结构方法注记的结构性证明法。Human-readable：将协议模型为4种主体。Paulson：所有可能事件路径的集合。每条路径是一个包含多轮协议通信的事件序列。主体接收到一个路径，可转发它或根据协议规则进行扩展使消息的真正发送者对此无从可知。它可以模拟所有攻击和密钥丢失。,Paulson归纳法基于协议消息和事件的攻击结构方法注记的结,Paulson归纳法续,秘密性：攻击者不能获知发送给其他主体的消息内容。认证性：如果一个消息表现为发自主体A，那么主体A的确发送了此消息，并且消息内的随机数或事件戳将正确指示其新鲜

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

27、用于推理任意长度的有限行为序列的结果。parts:用于生成消息集合的所有部分。Analz:表示使用正确密钥解密之前传递的消息。Synth:表示对消息的伪造。与信仰逻辑不同, 协议的归纳验证的证明过程是详细的，协议每个安全属性都能得到证明。,Paulson归纳法概述续Paulson归纳法为归纳定义,Paulson归纳法概述续,1.消息主体标识：A,B,。随机数:Na,Nb,。密钥:Ka,Kb,Kab,。消息混合X,X。消息的Hash值。加密的消息Crypt KX。,Paulson归纳法概述续1.消息,Paulson归纳法概述续,2. Parts, analz 和synth 如果H表示一个主体的初

28、始知识和一条路径中所有发送的消息，那么每个操作可从H的消息中衍生出新的消息以扩充H。Parts H通过不断地增加混合消息和加密消息来从H中获得。Crypt KXparts HXparts HParts Gparts H = parts(GH),Paulson归纳法概述续2. Parts, analz 和,Paulson归纳法概述续,analz H通过不断地增加混合消息和可用集合中的密钥解密的消息来从H中获得。Kanalz H ,那么通过监听H不能获知K。Crypt KXanalz H:K-1 analz Xanalz HAnalz Ganalz H=analz(GH)Analz Hparts

29、H,Paulson归纳法概述续analz H通过不断地增加混合消,Paulson归纳法概述续,synth H是攻击者通过不断增加主体标识，构造混合消息和用H中的密钥生成加密消息来从H中获得的。Xsynth H, KHCrypt KXsynth HKsynth HKH,Paulson归纳法概述续synth H是攻击者通过不断增加,Paulson归纳法概述续,3. 攻击者：可以观察网络中所有通信。发送从集合synth (analz H)中衍生的欺骗消息。在模型中攻击者被视为参与协议运行的一个诚实的主体，它可以用其长期秘密密钥发送正常的协议消息，以及伪造的消息，使得它能够利用截获的密钥参与协议的运行

30、并因此欺骗其他主体。,Paulson归纳法概述续3. 攻击者：,Paulson归纳法概述-协议模型,4. 协议模型Says A B X：表示A发送消息X给B。Notes A X：表示A内部存储X。除攻击者外,主体只接收发送给它们的消息。,Paulson归纳法概述-协议模型4. 协议模型,Paulson归纳法概述-协议模型续,Otway-Rees协议AB:M,A,B,E(Kas: Na ,M, A, B)BS: M,A,B,E(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,

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

32、Na, A,Bkb发送者的标记为A, 并且未在新事件中使用是因为B不知道是谁发送了消息。,Paulson归纳法概述-协议模型续Nb是一个新鲜的随机数,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包

33、含一个事,Paulson归纳法概述-协议模型续,如果路径evs包含两个事件:Says BSNa, A,B,X, Nb, Na, A, BkbSays SB Na, X, Nb, Kkb若AB，那么evs将被下面事件扩展:Says BA Na, X主体B收到了一个期望格式的消息,解密相应部分,检查Nb与其先前发送给服务器的随机数是否一致,并将X转发给A。另外A检查它的随即数并确认会话。,Paulson归纳法概述-协议模型续如果路径evs包含两个事,Paulson归纳法概述-标准规则,5. 标准规则-3个规则：规则一：空链 是一个路径。规则二：如果evs是一个路径，Xsynth(analz H)是

34、一个伪造的消息,并且BSpy，那么evs将被下面事件扩展: Says Spy B X其中H包含过去路径中的所有消息以及攻击者的初始状态。,Paulson归纳法概述-标准规则5. 标准规则-3个,Paulson归纳法概述-标准规则续,规则三：如果路径evs 以及S 在一个包含Na和Nb的协议轮中分配会话密钥，那么evs将被下面的事件扩展： Notes Spy Na, Nb, K,Paulson归纳法概述-标准规则续规则三：如果路径evs,Paulson归纳法概述-归纳法,6. 归纳法 常规的数学归纳法为:对于每个自然数n，为证明P(n)，需证明P(0)和每个xN，证明P(x)P(suc X)。同

35、样，对于路径集合，归纳法表明：如果P在生成路径的所有规则下是成立的，那么P(evs)对于每个路径是成立的。,Paulson归纳法概述-归纳法6. 归纳法,Paulson归纳法概述-归纳法续,首先证明： P 是覆盖所有的空路径的。对于其他规则，必须证明断言：P(evs) P(ev#evs)其中事件ev 包含新的消息 (ev#evs是用事件ev对事件evs扩展后的路径，新的事件加在一个路径之前)。,Paulson归纳法概述-归纳法续首先证明：,Paulson归纳法概述-规则引理,7. 规则引理Xparts H H是可被攻击者获知的所有消息的集合。攻击者永远不可能持有任何主体的长期密钥，除非这些密钥

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

37、son归纳法概述-查找攻击,9. 查找攻击例外：服务器可能将密钥误分配给一对不相干的主体。当A收到Otway-Rees协议的第四条消息时，它不能确保此消息来自B，且B是从S处获得。,Paulson归纳法概述-查找攻击9. 查找攻击,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:N

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

39、t=Server|Friend nat | Spy,Paulson归纳法的自动化的理论主体和消息,Paulson归纳法的自动化的理论续,Datatype msg= Agent agent| Number nat (*guessable *)| Number nat (*non-guessable *)| Key key|Mapir msg msg|Hash msg|Crypt key msg,Paulson归纳法的自动化的理论续Datatype ms,Paulson归纳法的自动化的理论续,Crypt KX= Crypt KX K=k X=X不同消息集合是不相交的。SFriend ISSpySp

40、y Friend IFriend i Friend j当且仅当X=X时, Hash X=Hash X,Paulson归纳法的自动化的理论续Crypt KX= C,Paulson归纳法的自动化的理论续,Parts的定义XH Crypt KXparts HXParts H Xparts H X, Yparts H X parts H， Yparts H,Paulson归纳法的自动化的理论续Parts的定义,Paulson归纳法的自动化的理论续,Analz H定义为基于下列规则的集合：XH Crypt KXanalz H K-1analz HXanalz H Xanalz H X, Yanalz H

41、X analz H， Yanalz H,Paulson归纳法的自动化的理论续Analz 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归纳法的自动化的理论续synth H定义为基,Paulson归纳法的自动化的理论续,Isabelle 说明 analz 的语法描述：Consts analz:

42、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归纳法的自动化的理论续Isabelle 说明,Paulson归纳法-操作管理定律,Ins X H 表示集合 set X H单调性定律幂等律等价定律,Paulson归纳法-操作管理定律Ins X H 表示集合,Paulson归纳法-操作管理定律续,单调性定律如果GH, 那么Parts G parts

43、 HAnalz Ganalz HSynth Gsynth H,Paulson归纳法-操作管理定律续单调性定律,Paulson归纳法-操作管理定律续,幂等律Parts(parts H) = parts HAnalz(analz H)=analz HSynth(synth H)=synth H,Paulson归纳法-操作管理定律续幂等律,Paulson归纳法-操作管理定律续,等价定律Parts(analz H) = parts HAnalz(parts H)=parts HParts(synth H)=parts Hsynth HAnalz(synth H)=analz Hsynth HSynth

44、(parts H)不可归约Synth(analz H) 不可归约,Paulson归纳法-操作管理定律续等价定律,Paulson归纳法-符号评估,artsAgent A, Nonce Na Agent A, Nonce Na, Agent A, Nonce Na它可以处理诸如：Agent A, Xins Agent A, Nonce Na H,Paulson归纳法-符号评估,Paulson归纳法-符号评估续,对于消息X，考虑子目标：parts(ins XH)analz(ins XH)例如：Nonce Na, Agent A, Agent B, CryptKanone Na, Agent A, A

45、gent B则:parts(ins XH) 扩展为包括所有从Nonce Na和Agent A到X的插入集合parts H中的新元素的一个表达式。,Paulson归纳法-符号评估续对于消息X，考虑子目标：,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)P

46、arts(ins(Crypt KX)H)=ins(Crypt KX)(parts(ins XH)Parts(Crypt KXH)=Crypt KXparts(XH),Paulson归纳法-符号评估续完成符号评估的规则：,Paulson归纳法-符号评估续,Analz 的符号评估：keyFor H = K-1|X.Crypt KXH如果密钥不是用于解密的，则KkeyFor(analz H) analz(ins(Key K)H)=ins(Key K)(analz H),Paulson归纳法-符号评估续Analz 的符号评估：,Paulson归纳法-符号评估续,用于恢复在情况分析中加密消息的规则为：

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

48、h符号集由于结果的无,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归纳法-事件和攻击者知识Says ABX,Paulson归纳法-事件和攻击者知识续,函数spies 表示攻

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

50、evsinitState 用于说明主体的初始知识。,Paulson归纳法-事件和攻击者知识续集合 used ev,归纳法对一个递归协议的分析,扩展的Otway-Rees 协议：任意数目的主体，例如A与B建立连接后如果B与认证服务器连接则为Otway-Rees协议。但B也可能选择与其他主体如C等连接一个任意长的主体链。服务器生成新鲜的会话密钥Kab和kbc给每两个连接的主体。每个会话密钥封装在两个证书中发送给各主体。,归纳法对一个递归协议的分析扩展的Otway-Rees 协议：,A,B,C,S,A,B,Na,A,B,NaB,C Nb,A,B,NaB,C NbC,S Nc,Kcs,S,NckcKb