安全协议理论与方法---中国科学技术大学市公开课特等奖市赛课微课一等奖课件.pptx

单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,*,*,安全协议理论与方法,基于证实结构性方法,第1页,介绍,推理结构性方法缺点：,不能处理秘密性，缺乏清楚语义。,攻击结构性方法缺点：,状态空间爆炸，时间与空间资源受限。,第2页,介绍,Human-readable,方法特点：,将重点放在明确区分主体可信度上。,利用强有力不变式技术和攻击者知识公理使得认证过程类似于基于模型验证方法。,第3页,主体知识及操作,可信主体：,A,、,B,、,S,不可信主体：,Z,主体间发送消息可分为：,基本消息：包含密钥,K,和非密钥数据,D,。,合成消息：包含消息对,(C1,C2),和加密消息。,对称密钥域记为,KS,，非对称密钥域记为,KA,。,第4页,主体知识及操作续,K=K,A,K,S,C=C,k,|,(C,C)|B,B=K|D,K=K,A,|K,S,|K,S,-1,S=C S:,可被攻击者获取消息集合。,第5页,主体知识及操作续,kK,，,dD,，那么,dC,(d,k)C,dkC,d(d,k)dk,涵盖三个元素知识,S,中一个元素,。,变量,s,s,s,.,s1,s2,在,S,中赋值。,变量,k,k,k,.,k1,k2,在,K,中赋值。,变量,d,d,d,.,d1,d2,在,D,中赋值。,第6页,主体知识及操作续,五种基本操作：,；,用一个已知密钥加密一个已知数据。,：,用一个已知密钥解密一个已知数据。,：,级联两个已知数据。,：,分离一个数据对。,:,生成数据子集合。,第7页,主体知识及操作续,s,s,=(s,s)|(s,c,k,s=k cs)s=s(c),k,s,s,=(s,s)|(s,c,k,s=k,-1,(c),k,s)s=sc,s,s,=(s,s)|(s,c,k,s=c1c2s)s=s(c1,c2),s,s,=(s,s)|(s,c,k,s=(c1,c2)s)s=sc1c2,s,s,=(s,s)|(s,s1.s=s1s)s=s1,数据,s,可从数据,s,中生成当且仅当假如存在一个,5,个基本操作系列使得状态,s,转换到,s,记为,s known_in s,。,第8页,主体知识及操作续,对于,任意子集,E=x,1,x,n,记,E,为,x1,xn,自反传递闭包。,Known_in s,定义为：,S known_in s,当且仅当,s,第9页,主体知识及操作续,引理,5.1,假如,E,那么,s,s,s.(s,E,s,)(ss,E,s,s),证实,：假如对于已知数据集合和参数集合基本操作前置条件是满足，那么对于,s,任意子集也是满足，而且操作应用结果是一样。,关系,E,对于,任何子集是含有融合性，表达在：,第10页,主体知识及操作续,1),假如,s,E,s1,和,s,E,s2,那么存在,s3,有,s,E,s3,和,s2,E,s3,。,假如,s,s,那么存在,s,有,:,s,s,s,s,。更为普通，假如对于任何一个非空子集,E,，假如,s,E,s,那么存在,s,有,s,E,s,和,s,s,。,3),假如,s,i,s,和,s,j,s,其中,i,j,那么存在,S,有,s,j,s,和,s,i,s,。,第11页,主体知识及操作续,推论,5.1,假如,s,s,那么存在,s,有,s,s,和,s,s,。,第12页,主体知识及操作续,known_in,性质,A1c known_in s,c known_in s(c,c)known_in s,A2(c,c)known_in s,c known_in s c known_in s,A3,c known_in s,k known_in sck known_in s,A4ck known_in s,k,-1,known_in sc known_in s,A5s known_in s,s known_in s(ss)known_in s,A6,(ss),known_in s,s known_in s,s known_in s,A7s known_in s,A8,known_in s,第13页,主体知识及操作续,comp_of,性质,B1(c,c)comp_of s,c comp_of s c comp_of s,B2ck comp_of s,k,-1,comp_of sc comp_of s,B3s comp_of s,s comp_of s(ss)comp_of s,B4,(ss)comp_of,s,s comp_of s,s comp_of s,B5s comp_of s,B6,comp_of s,第14页,主体知识及操作续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 comp_of s(c1,c2),C5,(c comp_of ),C6,(s comp_of s)(s comp_of s)(ss comp_of s),C7 c,s setofkeys(s)(c comp_of s),C8 setofkeys(s),setofkeys(s K),C9 setofkeys(,),第15页,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),(ck known_in s),D5,(c,c)comp_of s)(c known_in s)(c known_in s),(c,c)known_in s),第16页,Known_in,和,comp_of,关系续,D6,(s known_in s)(c known_in s),(ss known_in s),第17页,协议形式化分析实例,-NS,A,S:A,B,SA:E(Ks,-1,:kb,B),AB:E(kb:Na,A),B,S:B,A,SB:E(ks,-1,:ka,A),BA:E(Ka:Na,Nb),AB:E(Kb:Nb),第18页,Human-readable,证实法对协议分析,主体及原子行为描述。,认证属性提出。,不变式结构。,认证属性验证。,第19页,主体及原子行为描述,S,A,=slave:Principal,N,A,:Nonce,N,B,:Nonce,K,B,:K,at:Program Address,S,B,=master:Principal,N,A,:Nonce,N,B,:Nonce,K,A,:K,at:Program Address,第20页,主体及原子行为描述续,Ss=,key:Principal,K,at:ProgramAddress,其中,at,用于统计每个主体执行算法次数。,第21页,主体及原子行为描述续,action(S,A,.at,1a,S,A,.at),Sz=Sz(A,S,A,.slave),action(Ss.at,1s,Ss.at),(d1,d2)known_in Sz,action(Ss.at,2s,Ss.at),Sz=Sz(Ss.key(d3),d3)ks,-1,action(S,A,.at,2a,S,A,.at),(S,A,.K,B,S,A,.slave)ks,-1,known_in Sz,action(S,A,.at,3a,S,A,.at),S,z,=S,z,(S,A,.N,A,A)S,A.KB,new(S,A,.N,A,S,Z,),action(S,B,.at,3b,S,B,.at),(S,B,.N,A,S,B,.master)k,B,known _in S,z,action(S,B,.at,4b,S,B,.at),S,z,=S,z,(B,S,B,.master),action(Ss.at,4s,Ss.at),(d4,d5)known_in S,z,第22页,主体及原子行为描述续,9)action(S,s,.at,5s,S,s,.at),S,z,=Sz(Ss.key(d6),d6)k,B,-1,10,)action(S,B,.at,5b,S,B,.at),(S,B,K,A,B)K,B,-1,known_in Sz,11)action(S,B,.at,6b,S,B,.at),Sz=Sz(S,B,.N,A,S,B,.N,B,)S,B,.K,A,new(S,B,.N,B,Sz),12)action(S,A,.at,6a,S,A,.at),(S,A,.N,A,S,A,.N,B,)k,A,known_in Sz,13)action(S,A,.at,7a,S,A,.at),Sz=Sz(S,A,.N,B,)S,A,.K,B,14)action(S,B,.at,7b,S,B,.at),(S,B,.N,B,)k,B,known_in Sz,第23页,主体及原子行为描述续,每一个行为刻画了一个可信主体与攻击者之间通信以及由此引发两个主体状态变量同时改变。,Sz=Sz,S,此形式描述可信主体发送消息,S,给攻击者。,S known_in Sz,描述消息,S,反方向发送。攻击者发出它已知消息,:,刚接收消息,先前发送或生成用于误导其它主体消息,.,第24页,认证属性提出,假设存在一个全局观察者,其任意选择两个可信主体并试图使协议确保不出现以下情况,:,一个主体相信他已经正确地执行了一个与另一个主体认证会话,但另一个主体正进行其它事情或进行着完全一致会话,.,主主体用,A,表示，从主体用,B,表示。,第25页,3a,3b,6b,6a,7a,7b,行为执行次序图,第26页,认证属性描述,主主体认证属性描述：,每次当,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,行为。,第27页,不变式结构一,关于,S,不变式一,攻击者不能获知主体私钥，不然将造成协议缺点,记为,inv0(Sz),，定义以下,:,Inv0(Sz)=(K,A,-1,known_in Sz)(K,B,-1,known_in Sz)(K,s,-1,known_in Sz),Inv1(Sz)=(K,A,-1,known_in(Szrng(key)(K,B,-1,known_in(Szrng(key)(K,s,-1,known_in(Szrng(key),第28页,不变式结构二,A,和,B,为他们欲通信主体使用正确密钥。首先描述形为,(k,d)k,B,-1,攻击者已知全部数据：,(k,d).(k,d)k,B,-1,known_in Szk=key(d),则,inv2(s),为：,(k,d).(k,d)k,B,-1,known_in Srng(key)k=key(d),第29页,关于A和B不变式,主体,A(,或,B),必须使用正确从主体,(,主主体,),密钥，而且不能是攻击者可用于误导主体密钥。,1A:,(pre(S,A,.at,3a),pre(S,A,.at,7a),),S,o,.kB=key(S,A,.slave),1B,:(pre(S,B,.at,6b),S,o,.K,B,=key(S,A,.slave),Pre(at,3a),：只有当,at,在行为可被触发一个状态中时状态为真。,第30页,认证属性证实,主主体认证属性证实,证实在,A,两个连续行为,3a,和,6a,之间，最少有,B,一个行为,6b,。,证实在,3a,和,6b,之间存在一个对应持有与,3a,一样消息,3b,。这证实了,B,最少进行了,3b,和,6b,两个行为，而且是以正确次序和正确值进行。,引入变量：,in_window=false,证实,:,假如,S,A,.slave=B,与,3a,一起执行，,3a,将置,in_window=True;,假如,S,A,.slave=B,与,6a,一起执行，,6a,将置,in_window=False,；,第31页,认证属性证实续,现在证实假如,in_window=True,，那么行为,6a,不可能发生：,S,A,.(S,A,.N,A,S,A,.N,B,)K,A,known_in Sz,此性质可用一个不变式描述为：,In_window=true,n.(S,A,.N,A,n)K,A,known_in Sz,第32页,认证属性证实续,经过增加,S,B,.masterA,S,A,.N,A,S,B,.N,A,和,b.(S,A,.N,A,b)k,B,known_in Szb=A,当在行为,6b,由,S,B,.masterA(,不变式成立必要条件是,S,A,.N,A,与,S,B,.N,A,不相同,),触发情况下证实不变式性质保持时，第一个约束条件被引入,;,当在行为,3b,被触发情况下证实不变式性质保持时，第二个约束条件被引入。,第33页,从主体认证属性证实,In_window=true,(S,B,.N,B,),kB,known_in Sz),增加：,S,A,.slaveBS,B,.N,B,S,A,.N,B,。,比如假如,A,与其它主体,C,通信，那么,S,A,.N,B,将不是,B,所期待随机数。,与上类似为使行为,6a,保持不变式，需有：,(S,A,.N,A,S,B,.N,B,),KA,known_in Sz,也即,:A,收到一个消息假如第一部分,S,A,.N,A,是正确，那么其第二部分一定不一样于,S,B,.N,B,。,第34页,从主体认证属性证实续,不过假如,S,A,.N,A,和,S,B,.N,B,是不一样，那么不变式显然是不成立。而且依据它角色，,A,必须发送,(S,A,.N,A,A),kc,给,C,，但依据假设攻击者是知道此消息,(,因为除了,A,B,S,外任何主体都可充当攻击者角色,),。攻击者所以知道了,Kc,-1,和,S,A,.N,A,并能够发送,(S,A,.N,A,A),kc,给,B,。由此,(S,A,.N,A,S,B,.N,B,),KA,known_in Sz,和,S,A,.slaveB,及,S,B,.N,B,=S,A,.N,B,都为真，而且,7b,可由,A,一个不正确响应,6a,所触发。,第35页,从主体认证属性证实续,由上述说明可知，协议是有缺点。,修改之一：在消息,6,中增加发送者标识。,第二个约束条件变为：,b.(S,A,.N,A,S,B,.N,B,b)k,A,known_in Szb=B,第36页,并行多重会话,瓦解主体在并行会话中饰演多个角色可能。协议中,S,含有这种可能。,一旦,A,已执行了,1a,后，唯一能执行行为,2a,，比如它不能接收,3b,，这意味着它作为一个从主体为其它进程开始了另一个会话；它也不能执行,1a,，这意味着它作为主主体开始了另一个会话。它也不能执行,1a,，这意味着它作为主主体开始了另一个会话。,第37页,并行多重会话续,A,B:Na,B,A:E(Kab:Na,Nb),AB:Nb,协议行为包含,6,步：,1a,1b,2b,2a,3a,3b,，并可对,A,、,B,状态以及,6,个行为进行形式化描述，不过：,1),断言行为描述,需考虑新型序列约束。,2),每个主体状态包括多个并行会话，所以需要跟踪每个会话内容。,第38页,并行多重会话续,描述主认证属性时仅考虑,1a,和,2a,以及,B,行为,1b,和,2b,。,证实不变式,(Kab known_in Si),然后用反证法证实行为,2b,在任一会话中必须出现在由,1b,和,2b,界定窗口内。它使用一个窗口不变式：,In_window=truen.(S,A,.N,A,n)K,ab,known_in Si),第39页,并行多重会话续,注意,2b,不一样情况：,2b,可被,A,或,B,执行。,2b,由,B,执行时,Sb.master,可等价于,A,或不等价于,A,，,SA.NA,也可等价于,SB.NA,，或者不等价。,假如,2b,由,A,执行，则存在问题。假如强制执行与前述协议一样序列约束，认证属性得到满足，不然，假如,A,可执行并行多重会话，那么将破坏不变式，作为从主体，,A,将给攻击者一个答案，即它在等候所包括其它并行会话。,第40页,Human-readable,若要求更为详细协议分析时，可与基于模型检测形式化方法交替使用。其已用于许多认证协议分析中，验证结论能够从一个协议应用到另一个协议，因为：,证实法主要工作是独立于协议，所以是能够重用。,即使是与协议相关部分，诸如不变式确实定与证实或认证属性形式化与证实，也不因协议不一样而有重大改变，因而也是能够重用。,第41页,Paulson归纳法,基于协议消息和事件攻击结构方法注记结构性证实法。,Human-readable,：将协议模型为,4,种主体。,Paulson,：全部可能事件路径集合。每条路径是一个包含多轮协议通信事件序列。主体接收到一个路径，可转发它或依据协,议规则进行扩展使消息真正发送者对此无从可知。它能够模拟全部攻击和密钥丢失。,第42页,Paulson归纳法续,秘密性：攻击者不能获知发送给其它主体消息内容。,认证性：假如一个消息表现为发自主体,A,，那么主体,A,确实发送了此消息，而且消息内随机数或事件戳将正确指示其新鲜性。,借鉴了状态探测和信仰逻辑一些方面。借鉴状态探测,描述事件,，第二种方法给出对所生成消息,信仰,。,第43页,Paulson,归纳法概述续,协议非形式化描述：,主体,A,：在协议结束时只有,A,和,B,有可能知道会话密 钥,Kab,。,主体,B,：攻击者能得到什么？,主体,A,：在没有,A,和,B,长久密钥前提下，它是不 能读取证书。,主体,B,：攻击者能够坑骗,B,接收与它共享密钥？,主体,A,：可识别随机数使用可阻止这一行为。,第44页,Paulson归纳法概述续,Paulson,归纳法为归纳定义,每个定义列出了主体或系统可能行为。归納规则可用于推理任意长度有限行为序列结果。,parts:,用于生成消息集合全部部分。,Analz:,表示使用正确密钥解密之前传递消息。,Synth:,表示对消息伪造。,与信仰逻辑不一样,协议归纳验证证实过程是详细，协议每个安全属性都能得到证实。,第45页,Paulson归纳法概述续,1.,消息,主体标识：,A,B,。,随机数,:Na,Nb,。,密钥,:Ka,Kb,Kab,。,消息混合,X,X,。,消息,Hash,值。,加密消息,Crypt KX,。,第46页,Paulson归纳法概述续,2.Parts,analz,和,synth,假如,H,表示一个主体初始知识和一条路径中全部发送消息，那么每个操作可从,H,消息中衍生出新消息以扩充,H,。,Parts H,经过不停地增加,混合,消息和,加密,消息来从,H,中取得。,Crypt KX,parts HXparts H,Parts G,parts H=parts(GH),第47页,Paulson归纳法概述续,analz H,经过不停地增加,混合,消息和可用集合中,密钥解密消息,来从,H,中取得。,K,analz H,那么经过监听,H,不能获知,K,。,Crypt KX,analz H:K,-1,analz Xanalz H,Analz Ganalz H=analz(GH),Analz Hparts H,第48页,Paulson归纳法概述续,synth H,是攻击者经过不停增加,主体标识,，,结构混合消息,和用,H,中,密钥生成加密消息,来从,H,中取得。,X,synth H,KHCrypt KXsynth H,K,synth HKH,第49页,Paulson归纳法概述续,3.,攻击者：,能够观察网络中全部通信。,发送从集合,synth(analz H),中衍生坑骗消息。,在模型中攻击者被视为参加协议运行一个老实主体，它能够用其长久秘密密钥发送正常协议消息，以及伪造消息，使得它能够利用截获密钥参加协议运行并所以坑骗其它主体。,第50页,Paulson归纳法概述-协议模型,4.,协议模型,Says A B X,：表示,A,发送消息,X,给,B,。,Notes A X,：表示,A,内部存放,X,。,除攻击者外,主体只接收发送给它们消息。,第51页,Paulson归纳法概述-协议模型续,Otway-Rees,协议,A,B:M,A,B,E(Kas:Na,M,A,B),B,S:,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,Kab),服务器是常量,S,，,A,和,B,可为任意主体。,第52页,Paulson归纳法概述-协议模型续,协议模型化表示：,假如,evs,是一个路径,Na,是一个新鲜随机数,B,是一个不一样于,S,和,A,主体,那么,evs,将被下面事件扩展。,Says AB Na,A,B,Na,A,B,ka,假如路径,evs,包含一个事件,:,Says AB Na,A,B,X,第53页,Paulson归纳法概述-协议模型续,Nb,是一个新鲜随机数,而且,BS,那么,evs,将被下面事件扩展：,Says BSNa,A,B,X,Nb,Na,A,Bkb,发送者标识为,A,而且未在新事件中使用是因为,B,不知道是谁发送了消息。,第54页,Paulson归纳法概述-协议模型续,假如路径,evs,包含一个事件,:,Says BS Na,A,B,Na,A,B,ka,Nb,Na,A,B,kb,Kab,是一个新鲜密钥且,BS,那么,evs,将被下面事件扩展：,Says SB Na,Na,Kab,ka,Na,Kab,kb,服务器,S,并不知道消息来自何方。假如,S,能够用标识主体密钥解密消息，并得到消息正确格式，那么它认为消息是有效并响应,B,。,第55页,Paulson归纳法概述-协议模型续,假如路径,evs,包含两个事件,:,Says BSNa,A,B,X,Nb,Na,A,B,kb,Says SB Na,X,Nb,K,kb,若,AB,，那么,evs,将被下面事件扩展,:,Says BA Na,X,主体,B,收到了一个期望格式消息,解密对应部分,检验,Nb,与其先前发送给服务器随机数是否一致,并将,X,转发给,A,。另外,A,检验它随即数并确认会话。,第56页,Paulson归纳法概述-标准规则,5.,标准规则,-3,个规则：,规则一,：空链,是一个路径。,规则二,：假如,evs,是一个路径，,X,synth(analz H),是一个伪造消息,而且,BSpy,，那么,evs,将被下面事件扩展,:,Says Spy B X,其中,H,包含过去路径中全部消息以及攻击者初始状态。,第57页,Paulson归纳法概述-标准规则续,规则三：假如路径,evs,以及,S,在一个包含,Na,和,Nb,协议轮中分配会话密钥，那么,evs,将被下面事件扩展：,Notes Spy Na,Nb,K,第58页,Paulson归纳法概述-归纳法,6.,归纳法,常规数学归纳法为,:,对于每个自然数,n,，为证实,P(n),，需证实,P(0),和每个,x,N,，证实,P(x)P(suc X),。,一样，对于路径集合，归纳法表明：假如,P,在生成路径全部规则下是成立，那么,P(evs),对于每个路径是成立。,第59页,Paulson归纳法概述-归纳法续,首先证实：,P,是覆盖全部空路径。,对于其它规则，必须证实断言：,P(evs),P(ev#evs),其中事件,ev,包含新消息,(ev#evs,是用事件,ev,对事件,evs,扩展后路径，新事件加在一个路径之前,),。,第60页,Paulson归纳法概述-规则引理,7.,规则引理,X,parts H,H,是可被攻击者获知全部消息集合。,攻击者永远不可能持有任何主体长久密钥，除非这些密钥开始就被假定丢失。,归纳证实等同于检验协议规则和观察它们没有一个包括长久密钥发送。,规则引理用,part,操作说明,易于证实。,第61页,Paulson归纳法概述-秘密性定理,8.,秘密性定理,定理,:,任何其它主体不能获知会话密钥。假如攻击者持有了一些会话密钥,它不能用它去获知其它会话密钥。它包括,analz,操作。,结论：假如攻击者持有了一些会话密钥,它不能用它去获知其它会话密钥。没有些人发送,Crypt Kab Kcd,消息。但遗憾是攻击者不但能够自己直接发送这么消息或者造成其它主体发送这么消息。,第62页,Paulson,归纳法概述,-,查找攻击,9.,查找攻击,例外：服务器可能将密钥误分配给一对不相干主体。当,A,收到,Otway-Rees,协议第四条消息时，它不能确保此消息来自,B,，且,B,是从,S,处取得。,第63页,Paulson,归纳法概述,-,查找攻击续,A,Z(B):Na,A,B,E(Kas:Na,A,B),1)Z,A: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:Nb,Kia),4)Z(B)A:Na,E(Kas:Na,Kia),第64页,Paulson归纳法概述-查找攻击续,因为,Na,是由,A,原始生成随机数,所以在消息,2,中用,Na,替换,Na,可造成,A,视,Kia,为用于与,B,通信密钥。,Otway-Rees,使用随机数作用：,确保新鲜性。,用于绑定主体标识。,经过证实,Na,和,Nb,惟一标识消息起源并绝对不会重合来验证协议正确性。,第65页,Paulson,归纳法自动化理论,主体和消息,S,：服务器,Frendi:,友好主体,Spy:,攻击者,Datatype agent=Server|Friend nat|Spy,第66页,Paulson,归纳法自动化理论续,Datatype msg=Agent agent,|Number nat(*guessable*),|Number nat(*non-guessable*),|Key key,|Mapir msg msg,|Hash msg,|Crypt key msg,第67页,Paulson,归纳法自动化理论续,Crypt KX=Crypt KX,K=k X=X,不一样消息集合是不相交。,SFriend I,SSpy,Spy Friend I,Friend i Friend j,当且仅当,X=X,时,Hash X=Hash X,第68页,Paulson,归纳法自动化理论续,Parts,定义,X,H,Crypt KXparts H,XParts H,Xparts H,X,Yparts H,X parts H,，,Yparts H,第69页,Paulson,归纳法自动化理论续,Analz H,定义为基于以下规则集合：,X,H,Crypt KXanalz H K,-1,analz H,Xanalz H,Xanalz H,X,Yanalz H,X analz H,，,Yanalz H,第70页,Paulson,归纳法自动化理论续,synth H,定义为基于以下规则集合：,Ageny A,synth H,Number Nsynth H,XH,Xsynth H,Xsynth H,Hash Xsynth H,Xsynth H,Ysynth H,Xsynth H,KH,X,Y synth H,Crypt KXsynth H,第71页,Paulson,归纳法自动化理论续,Isabelle,说明,analz,语法描述：,Consts analz:msg set,msg set,Inductive“analz H”,Intrs,Inj”XH Xanalz H”,Fst“X,Yanalz HXanalz H,Yanalz H”,Decrypt“Crypt KXanalz H;Key(invKey K)analz HXanalz H”,第72页,Paulson,归纳法,-,操作管理定律,Ins X H,表示集合,set X,H,单调性定律,幂等律,等价定律,第73页,Paulson,归纳法,-,操作管理定律续,单调性定律,假如,G,H,那么,Parts G parts H,Analz Ganalz H,Synth Gsynth H,第74页,Paulson,归纳法,-,操作管理定律续,幂等律,Parts(parts H)=parts H,Analz(analz H)=analz H,Synth(synth H)=synth H,第75页,Paulson,归纳法,-,操作管理定律续,等价定律,Parts(analz H)=parts H,Analz(parts H)=parts H,Parts(synth H)=parts H,synth H,Analz(synth H)=analz Hsynth H,Synth(parts H),不可归约,Synth(analz H),不可归约,第76页,Paulson,归纳法,-,符号评定,partsAgent A,Nonce Na,Agent A,Nonce Na,Agent A,Nonce Na,它能够处理诸如：,Agent A,X,ins Agent A,Nonce Na H,第77页,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,中新元素一个表示式。,第78页,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 KX,H,)=Crypt KX,parts(XH),第79页,Paulson,归纳法,-,符号评定续,Analz,符号评定：,keyFor H=K,-1,|,X.Crypt KXH,假如密钥不是用于解密，则,K,keyFor(analz H),analz(ins(Key K)H)=ins(Key K)(analz H),第80页,Paulson,归纳法,-,符号评定续,用于恢复在情况分析中加密消息规则为：,analz(ins(Crypt KX)H)=,ins(Crypt KX)(analz(ins XH)K,-1,analz H,ins(Crypt KX)(analz H)otherwise,第81页,Paulson,归纳法,-,符号评定续,Synth,符号集因为结果无限性不能被评定。,分析,X,synth H,假设，并假定随机数和密钥为不可猜测。,Nonce Nsynth HNonce NH,Key K synth HKey KH,假如,Crypt KXsynth H,那么有,Crypt KXH,，,Xsynth H,和,KH,第82页,Paulson,归纳法,-,事件和攻击者知识,Says ABX,或,Notes AX,Isabelle,描述为：,Datatype event=Says agent agent msg,|Notes agent msg,initState S=all lon-term keys,iniState(Friend i)=Key(shrK(Friend i),iniState Spy=Key(shrK(A)|A,bad,其中,shrK,为每个主体,A,与服务器共享长久密钥。,第83页,Paulson,归纳法,-,事件和攻击者知识续,函数,spies,表示攻击者在路径中能够看到消息,。,Spies=initState Spy,Spies(Says ABX)#evs)=X,spies evs,Xspies evs if Abad,Spies(Notes AX)#evs)=,spies evs otherwise,第84页,Paulson,归纳法,-,事件和攻击者知识续,集合,used evs,形式化描述了新鲜性,used=,B.parts(initState B),used(Says ABX)#evs)=partsXused evs,used(Notes AX)#evs)=partsXused evs,initState,用于说明主体初始知识。,第85页,归纳法对一个递归协议分析,扩展,Otway-Rees,协议：,任意数目标主体，比如,A,与,B,建立连接后假如,B,与认证服务器连接则为,Otway-Rees,协议。但,B,也可能选择与其它主体如,C,等连接一个任意长主体链。,服务器生成新鲜会话密钥,Kab,和,kbc,给每两个连接主体。,每个会话密钥封装在两个证书中发送给各主体。,第86页,A,B,C,S,A,B,Na,A,B,Na,B,C Nb,A,B,Na,B,C Nb,C,S Nc,Kcs,S,Nckc,Kbc,B,Nckc,Kbc,C,Nbkb,Kab,A,Nbkb,Kab,B,NaKa,Kbc,C,Nbkb,Kab,A,Nbkb,Kab,B,NaKa,Kab,B,NaKa,三个客户递归协议,第87页,John Bull,提出递归协议,A,B:Hash,ka,A,B,Na,-,B,C:Hash,kb,B,C,Nb,Hash,ka,A,B,Na,-,2),能够重复很屡次，每一步都有新消息加入，直到某个主体与服务器,S,执行了步骤,2),。标志,-,表示请求结束。,第88页,John Bull,提出递归协议续,若申请者次序为,A,、,B,和,C,那么响应为,:,Hash,Kc,C,S,Nc,Hash,Kb,B,C,Nb,Hash,Ka,A,B,Na,-,S,响应给,C5,个证书：,3)S,C:,Kcs,S,Nc,kc,Kbc,B,Nc,kc,Kbc,C,Nb,kb,Kab,A,Nb,kb,Kab,B,Na,Ka,第89页,John Bull,提出递归协议续,4)C,B:,Kbc,C,Nb,kb,Kab,A,Nb,kb,Kab,B,Na,Ka,4)B,A:,Kab,B,Na,Ka,第90页,John Bull,递归,协议模型,Isabelle,对协议实例描述包括：,Nil:,空路径。,Fake:,伪造消息。,RA1-4:,协议步骤。,Oops:,会话密钥丢失偶然事件。,Recur:,路径集合。,第91页,John Bull,递归,协议模型续,Nil,recur,Fake|evsrecur;BSpy;XSynth(analz(spies evs)|Says Spy B X#evs recur,RA1,|evs1recur;AB;AServer;Nonce NA used evs1|Says A B(HashKey(shrK A),|Agent A,Agent B,Nonce NA,