安全协议理论与方法

单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,*,*,安全协议理论与方法,基于推理结构性方法,1,SVO,逻辑,Syverson,和,Oracho,提出，建立了用于推证合理性的理论模型。,提供独立明确的语义基础。,相当详细的模型。消除理解模糊，有助于准确理解消息的真实含义和协议理想化。,通用语义，扩展性好，简洁。,2,SVO,逻辑的基本结构,术语集合。,推理规则及公理。,基于的假设。,3,SVO,术语集合,定义,T,为初始术语集合,包括互不相交的常量符号集合：主体、共享密钥、公钥、私钥以及序列号等。,n,维函数表示有,n,个变量的函数，如加、解密函数等,。,消息语言,M,T,：,满足下列性质的最小语言集合。,1),如果,X,T,，则,X,是消息。,2),如果,X,1,X,n,是消息，,F,是任意一个,n,维函数,则,F(X,1,X,n,),是消息。,3),如果是公式，则是消息。,4,SVO,术语集合续,4.,公式语言,F,T,：,满足下列性质的最小公式集合。,1),如果,P,是原始命题，则,P,是公式。,如果,是公式，则和是公式。,P,believes,和,P controls,是公式，其中,P,是主体， 是公式。,P sees X, P says X, P said X, P received X,和,fresh(X),是公式,其中,P,是主体,X,是消息。,Shared(P,K,Q),PK(P,K),和,P has K,是公式，其中,P,是主体，,K,是消息。,5,SVO,逻辑的推理规则及公理,1.,SVO,逻辑遵从两条基本推理规则,(,), ,P believes,6,SVO,逻辑的推理规则及公理续,1,SVO,逻辑共有,20,条公理,I1,相信公理,对于任一主体,P,和公式,，有：,P believes, ,P believes(,),P believes,P believes, ,P believes ( P believes,),7,SVO,逻辑的推理规则及公理续,2,(2) I2,源关联公理,密钥用于推断消息发送者的身份。,shared(P,K,Q),R received X,Q,K,Q said X,(PK,(Q,K)R received X,K,-1,Q said X,PK,(Q,K),表示,K,是主体,Q,的数字签名验证密钥。,它表明如果主体,Q,收到一个签名的消息，并且,Q,知道签名的验证密钥是,K,，就可以确定发送者身份。,8,SVO,逻辑的推理规则及公理续,3,I3,密钥协商公理,(PK(P, K,P,),PK(P, K,q,),shared(P,K,Pq,Q),K,pq,= f(K,p, K,q,-1,) = f(K,p,-1, K,q,) f,为密钥协商函数，比如,Diffie-Hellman,密钥交换。,9,SVO,逻辑的推理规则及公理续,4,I4,接收公理,主体对接收到的一个级联的加密消息可用有效的密钥解密。,P received(X,1, , X,n,), P received X,i,P received X,K, P has K,-1, P received X,10,SVO,逻辑的推理规则及公理续,5,I5,看到公理,P received X, P sees X,P sees (X,1,X,n,) P sees X,i,P sees X,1,P sees X,n, P sees (F(X,1,X,n,),主体只要接收到一个消息就看到了这个消息，,并且看到了这个消息的每一部分。,11,SVO,逻辑的推理规则及公理续,6,I6,理解公理,P believes (P sees F(X), P believes (P sees X),P received F(X) P believes (P sees X), P believes (P received F(X),如果一个主体理解一个消息，并看到此消息,的一个函数，那么它理解它所看到的。,F,可视为加密函数，,K,为参数。,12,SVO,逻辑的推理规则及公理续,7,I7,叙述公理,一个主体说过一个级联消息，那么它一定说,过且看到消息的每一部分。,P said(X,1,X,n,), P said X,i, P sees X,i,P says (X,1,X,n,) P said (X,1,X,n,) P,says,X,i,13,SVO,逻辑的推理规则及公理续,8,仲裁公理,P,controls, ,P,says ,14,SVO,逻辑的推理规则及公理续,9,I9,新鲜公理,如果消息的一部分是新鲜的，那么整个消息,也是新鲜的。,fresh(X,i,),fresh(X,1,X,n,),fresh(X,1,X,n,)fresh(F(X,1,X,n,),fresh(X) P said X P says X,15,SVO,逻辑的推理规则及公理续,10,I10,共享密钥的良好对称性公理,如果,K,是,P,，,Q,之间的良好密钥当且仅当,K,是,Q,，,P,之间的良好密钥。,shared(P,K,Q),shard(Q,K,P),16,SVO,逻辑的推理规则及公理续,11,(11) I11,所有公理,P,has K, P sees K,17,SVO,逻辑语义,计算模型,Pe,：,代表环境,可用于模拟攻击者的任意行为,。,Si:,每个主体,Pi,有一个局部状态,Si,。,全局状态,:,n+1,维局部状态。,主体行为,:,发送,send(X,P),、,receive(),和,generate(X),，但只能生成集合,T0,中的元素,18,SVO,逻辑语义,计算模型续,1,每一个行为导致状态的一次迁移。,r:,一轮协议,r,是一个由整数时间索引的全局变量的有限集合。,r(t),：协议中的,t,时记为,r(t),。,ri(t):,对应的主体,Pi,的局部变量记为,ri(t),。,环境状态：全局历史、环境有效迁移集合和用于保存发给主体,P,而,P,还未收到的消息的消息缓冲区。,19,SVO,逻辑语义,计算模型续,2,主体,Pi,在,(r,t),收到的消息集合包括：,局部消息历史中或,t,之前出现的,received(X),中的,X,。,收到的消息的级联。,P,持有所收到的加密消息,X,K,的解密密钥，则,P,可得到,X,。,20,SVO,逻辑语义,计算模型续,3,主体,Pi,在协议运行当中某处可看到的消息集合包含,：,主体已收到的消息集。,主体新近生成消息集。,主体初始所知的消息集。,主体通过规则和公理从已知的消息集衍生的消息集。,对于主体说过的消息集的定义比此严格。,21,SVO,逻辑语义,计算模型续,4,主体,Pi,在,(r,t),发送的消息集合包括：,主体对已发送过消息的级联。,加密密钥为主体所持有的加密消息的非加密部分，且此部分为主体所看到。,签名密钥为主体所持有的签名消息的非签名部分，且此部分为主体所看到。,Hash,消息中的非,Hash,部分，且此部分为主体所看到。,22,SVO,逻辑语义,公式成立的条件,定义：,将每一个常量命题,pT,映射为点集,(p),即命题,p,为真的点。,公式在点,(r,t),为真记为：,(r,t),。,意味着,全真。,23,SVO,逻辑语义,公式成立的条件,1,逻辑连接及其原始命题,基本逻辑关系：,(r,t), p iff(r,t) (p),。,(r,t), iff(r,t) (r,t) ,。,(r,t), iff,在,(r,t),时不成立。,24,SVO,逻辑语义,公式成立的条件,2,原始命题,接收命题,(r,t), p,received X,当且仅当,X,属于主体,P,在,(r,t),时已收消息集合。,25,SVO,逻辑语义,公式成立的条件,3,看到命题和持有命题,(r,t), p,sees X,当且仅当,X,属于主体,P,在,(r,t),时已看到消息集合。,(r,t), p,has,X,当且仅当,X,属于主体,P,在,(r,t),时已收消息集合。,26,SVO,逻辑语义,公式成立的条件,4,3),述说命题,(r,t), p said X,当且仅当对于消息,M,在协议,t,时之前，主体,P,发送过消息,M,，且,X,是,M,的子消息。,27,SVO,逻辑语义,公式成立的条件,5,4),仲裁命题,(r,t), p controls,，,当且仅当,(r,t), p says,且对于所有的,t0,有：,(r,t) ,。,28,SVO,逻辑语义,公式成立的条件,6,5),新鲜性命题,(r,t), fresh(X),当且仅当对于所有主体在本轮协议前没有说过,X,。,29,SVO,逻辑语义,公式成立的条件,7,四种密钥命题：,共享密钥,公开加密密钥,公开签名密钥,公开协商密钥,30,SVO,逻辑语义,公式成立的条件,8,共享密钥？,(r,t), R receivedXK,或者,R,P,Q,。,31,SVO,逻辑语义,公式成立的条件,9,公开加密密钥,(r,t), PK,(P,K),当且仅当对于所有的,t,，若仅有,(r,t), Q sees X,K,，则,Q=P,。,32,SVO,逻辑语义,公式成立的条件,10,公开签名密钥,(r,t), PK,(P,K),当且仅当对于所有的,t,，,(r,t), Q received X,K,-1,，则表明,(r,t),P,said X,。,33,SVO,逻辑语义,公式成立的条件,11,公开协商密钥,(r,t), PK,(P,K),当且仅当对于所有的,t,：,对于某些,Q,，,K,pq,=f(K,-1, PK,(Q),且,(r,t) goodkey(P,K,pq,Q),对于所有,R,，,K,pr,=f(K,-1, PK,(R),以及,(r,t) ,goodkey(P,K,pr,R),且对于所有,U,，,Kur=f(PK,-1,(U), PK,-1,(R),且,(r,t) ,goodkey(U,K,ur,R),。,34,SVO,逻辑的应用实例,主体目标相同：密钥分配和认证。则 不大可能会出现否认性。,主体目标不同：电子商务，为了利益需求，可能对已发生行为进行否认。收费后否认收费或者因质量问题而否认发货。,解决：收集并持有一个声称事件或行为的不可否认证据，并使之能有效地用于解决由于否认事件或行为而引起的纠纷。,35,SVO,逻辑的应用实例续,1,Schneider,在下列文献 中运用通信顺序进程,CSP,对一个 不可否认协议实例进行了形式化的描述与分析。,Schneider S., Verifying authentication protocols with CSP. Proceedings of the IEEE Computer Security Foundations Workshop X, IEEE Computer Society, 3-17 1997,。,用,SVO,也可对不可否认性进行分析。,36,SVO,逻辑,-,一个不可否认协议实例,不可否认协议的实现：,证据的生成,证据的交换,证据的验证,纠纷的解决,一是双方进行同时的秘密交换,(,麻烦，要求协议双方具有同等计算能力不现实,),。,二是借助一个可信第三方,(TTP),。,37,SVO,逻辑,-,不可否认协议实例续,两个基本证据：,NRO(Non-repudiation of Origin):,发方不可否认。,NRR(Non-repudiation of Receipt):,收方不可否认。,NRS:(Non-repudiation of Submission):,提交不可否认,证明已提交给了,TTP,，由提交方提供。,NRD:(Non-repudiation of Delivery):,传递不可否认,证明,TTP,已交付给了意定接收者，由,TTP,提供。,38,SVO,逻辑,-,不可否认协议实例续,【Zhou,和,Gollman,提出,】ZG,协议,A,B:f,NRO, B,L,C, NRO,BA:f,NRR, A,L,C, NRR,ATTP: f,NRS, B,L,K, NRS_K,B,TTP: f,NRD, A,B,L,K, NRD_K,A,TTP: f,NRD, A,B,L,K, NRD_K,39,SVO,逻辑,-,不可否认协议实例续,:ftp,操作符。,NRO= S,A,(f,NRO,B,L,C),NRR= S,B,(f,NRR,A,L,C),NRS_K= S,A,(f,NRS,B,L,K),NRD_K= S,TTP,(f,NRD,A,B,L,K),40,SVO,逻辑,-,不可否认协议实例分析,定义,3.1,不可否认协议的公平性：,是指从协议执行的开始到协议执行结束的任何一个阶段，通信的双方要么能够同时得到它们所期望的，要么任何一方都得不到有利于自己的信息，从而避免协议的任一方中断执行的协议，或否认其已发生的行为以达成利益不平等的可能。,41,SVO,逻辑,-,不可否认协议实例分析,定理,3.1,一个不可否认协议的不可否认性是成立的，如果,：,协议任何一方执行后的中止将不会破坏 通信双方主体的地位的公平性。,在协议结束时提供主体参与协议行为的证据，即证据的有效性。,42,SVO,逻辑,-,不可否认协议,ZG,证明,给出协议的前提或假设,说明协议目标,运用规则和公理进行推证,43,SVO,逻辑,-ZG,证明假设,给出协议的前提或假设,A0:,协议的运行环境是不安全的,(,基本假设,),。,A1:,每个主体的公钥是公开的。,A2:,每个主体的私钥仅为其所知。,A3:TTP believes SA,A4:TTP believes SB,A5:P believes STTP:P,为参与协议运行的主体,A6:,TTP believes (B received C),TTP believes (A said C),44,SVO,逻辑,-ZG,证明假设续,A7:,A,said (A,B,L,E,k,(M), A said (A,B,L,K) A said M,A8:,B,received (A,B,L,E,k,(M) B received(A,B,L,K) B received M,A9:TTP believes (A said C B received C TTP received K) TTP says K,表示,TTP,只有在确信,A,已说过,C,，并且,B,已收到了,C,，以及,TTP,收到了,K,，才将,K,公布到其公开目录中。,A10,：,TTP says XP ftp X P sees X,TTP,将其认为是有效的数据放入到其公共目录下，并可为任何主体通过,ftp,操作访问。,45,SVO,逻辑,-ZG,证明假设续,A11:P,believes,PK,(Q,K), P received X,K,-1, P believes (Q said X),表示如果,P,收到一个签名消息，并且,P,相信这个签名密钥是,Q,的，那么,P,相信,Q,说过,X,。,A12:A,beliveves,fresh(Na),A13:TTP believes ,46,SVO,逻辑,-ZG,证明协议目标,一般目标：,G1A,believes (B received M),G2B believes (A said M),仲裁目标,G3J believes (A said M),G4J believes (B received M),47,SVO,逻辑,-ZG,证明运用规则和公理进行推证,由 消息,1),得：,F1:B received,S,A,(f,NRO,B,L,C),由,F1,A2,P4,A11,得：,(,P4:,PK,(A,K), B received X,K,-1, A said X),(,A11,: B believes,PK,(A,K), B received X,K,-1,) B believes (A said X),得,F2: B,believes (A said,(f,NRO,B,L,C),),48,SVO,逻辑,-ZG,证明运用规则和公理进行推证续,由,F2,P5(,是哪一个？,),得：,F3:B believes (A said C),同理，对原协议消息,2),的分析只能得到,A believes (B said C),，但无法 得到,A believes (B received C),原协议修改为,1)A,B:fNRO,B,L,C,SA(fNRO,B,L,Na,C),2)BA:fNRR,A,L,C,SA(fNR,A,L,Na+1,C),49,SVO,逻辑,-ZG,证明运用规则和公理进行推证续,对修改后的协议进行分析得：,F4:A receives S,B,(F,NRR,A,L,N,a,+1,C),由,F4,A2,P4,A11,A12,得：,F5:,A,believes,(B received (f,NRO, B,L,Na,C),A believes (B received C),由消息,3),得：,F6: TTP received S,A,(F,NRS, B,L,K),50,SVO,逻辑,-ZG,证明运用规则和公理进行推证续,由,F6, A2,A3,得：,F7:TTP believes (A said (fNRS,B,L,K), TTP received K,根据假设,A9,，,TTP,只有确信,A,已说过,C,，并且,B,收到,C,，以及,TTP,收到了,K,，才将,K,公布到其公开目录中，但在原有协议中，,TTP,并不能确知,B,是否已收到了,C,，因此，,A,可对,NRR,进行签名，并将结果发给,TTP,。对消息,3),修改如下：,51,SVO,逻辑,-ZG,证明运用规则和公理进行推证续,3)A,TTP: f,NRS, B,L,K,NRS_K, S,A,(NRR),TTP,收到消息,3),后由,P5,得：,F8:TTP received SA(NRR),由,F8,A3,A11,P1,得：,F9:TTP believed (A said C, B received C,),由,F8,F9,A9,A6,得：,F10:TTP says K,52,SVO,逻辑,-ZG,证明运用规则和公理进行推证续,由,F10,A10,，消息,4),得：,F11:,B received (f,NRD, A,B,L,K,S,TTP,(f,NRO, A,B,L,K),由,F11,P5,A13,得：,F12:(B received K, B received C,), B received M,由,F12,P6, A7,消息,5),得：,F13:A received (f,NRD,A,B,L,K,S,TTP,(f,NRO, A,B,L,K),),由,F10,F12,F13,A5,A11,P5,P7,P10,得：,53,SVO,逻辑,-ZG,证明运用规则和公理进行推证续,F14:A believes (TTP says K),A believes(B sees K), A believes (B received M)G1,由,F7,F11,A5,得：,F15:B believes(TTP says K) B believes (A said K),由,F3,F15,得：,F16: B believes (A said M)-G2,54,SVO,逻辑,-ZG,证明运用规则和公理进行推证续,协议可能出现的纠纷及解决,Case 1,A,否认向,B,发送了消息,M,。在这种情况下,B,可将,M,C,K,L,以及,NRO,NRD_K,提交给仲裁，仲裁通过以下几步可证明,A,发送了消息,M,。,检查,NRD_K,是用,T,的私钥对消息,(f,NRD,A,B,L,K),的签名。,J received S,TTP,(f,NRD, A,B,L,K), J believes (TTP says K), J believes (A said K),55,SVO,逻辑,-ZG,证明运用规则和公理进行推证续,2),检查,NRO,是用,A,的私钥对消息,(f,NRO,B,L,Na,C),的签名。,J received S,A,(f,NRO, B,L,N,a,C), J believes (A said C),如果检查,M=D(K,C),则：,J,believes,(A said M),得证,G3,。,56,SVO,逻辑,-ZG,证明运用规则和公理进行推证续,Case 2 B,否认收到了消息,M,。在这种情况下,A,将,M,C,K,L,以及,NRR,NRD_K,提交给仲裁，仲裁通过以下几步可证明,B,接收到了消息,M,。,检查,NRD_K,是用,T,的私钥对消息,(f,NRD,A,B,L,K),的签名。,J received S,TTP,(f,NRD, A,B,L,K),J believes (TTP says K),J believes(B received K),57,SVO,逻辑,-ZG,证明运用规则和公理进行推证续,2),检查,NRR,是用,B,的私钥对消息,(f,NRO,A,L,N,a,+1,C),的签名。,J received S,B,(f,NRO, A,L,N,a,+1,C), J believes (B received C),如果检查,M=D(K,C),则：,J,believes,(B received M),得证,G4,。,58,SVO,逻辑,-ZG,证明运用规则和公理进行推证续,修改后的协议为：,A,B:f,NRO, B,L,C, S,A,(f,NRO,B,L,Na,C),BA:f,NRR, A,L,C, S,B,(f,NRR,A,L,Na+1,C),ATTP: f,NRS, B,L,K, NRS_K,S,A,(NRR),B,TTP: f,NRD, A,B,L,K, NRD_K,A,TTP: f,NRD, A,B,L,K, NRD_K,59,