安全协议理论与方法(ppt 60页).ppt

1、安全协议理论与方法,基于推理结构性方法,SVO逻辑,Syverson和Oracho提出，建立了用于推证合理性的理论模型。提供独立明确的语义基础。相当详细的模型。消除理解模糊，有助于准确理解消息的真实含义和协议理想化。通用语义，扩展性好，简洁。,SVO逻辑的基本结构,术语集合。推理规则及公理。基于的假设。,SVO术语集合,定义T为初始术语集合,包括互不相交的常量符号集合：主体、共享密钥、公钥、私钥以及序列号等。n维函数表示有n个变量的函数，如加、解密函数等。消息语言MT：满足下列性质的最小语言集合。1)如果XT，则X是消息。2)如果X1,Xn是消息，F是任意一个n维函数,则F(X1,Xn)是消息

2、。3)如果是公式，则是消息。,SVO术语集合续,4.公式语言FT：满足下列性质的最小公式集合。1)如果P是原始命题，则P是公式。如果,是公式，则和是公式。Pbelieves和Pcontrols是公式，其中P是主体，是公式。PseesX,PsaysX,PsaidX,PreceivedX和fresh(X)是公式,其中P是主体,X是消息。Shared(P,K,Q),PK(P,K)和PhasK是公式，其中P是主体，K是消息。,SVO逻辑的推理规则及公理,1.SVO逻辑遵从两条基本推理规则()Pbelieves,SVO逻辑的推理规则及公理续1,SVO逻辑共有20条公理I1相信公理对于任一主体P和公式，有

3、：PbelievesPbelieves()PbelievesPbelievesPbelieves(Pbelieves),SVO逻辑的推理规则及公理续2,(2)I2源关联公理密钥用于推断消息发送者的身份。shared(P,K,Q)RreceivedXQKQsaidX(PK(Q,K)RreceivedXK-1QsaidXPK(Q,K)表示K是主体Q的数字签名验证密钥。它表明如果主体Q收到一个签名的消息，并且Q知道签名的验证密钥是K，就可以确定发送者身份。,SVO逻辑的推理规则及公理续3,I3密钥协商公理(PK(P,KP)PK(P,Kq)shared(P,KPq,Q)Kpq=f(Kp,Kq-1)=f

4、(Kp-1,Kq)f为密钥协商函数，比如Diffie-Hellman密钥交换。,SVO逻辑的推理规则及公理续4,I4接收公理主体对接收到的一个级联的加密消息可用有效的密钥解密。Preceived(X1,Xn)PreceivedXiPreceivedXKPhasK-1PreceivedX,SVO逻辑的推理规则及公理续5,I5看到公理PreceivedXPseesXPsees(X1,Xn)PseesXiPseesX1PseesXnPsees(F(X1,Xn)主体只要接收到一个消息就看到了这个消息，并且看到了这个消息的每一部分。,SVO逻辑的推理规则及公理续6,I6理解公理Pbelieves(Pse

5、esF(X)Pbelieves(PseesX)PreceivedF(X)Pbelieves(PseesX)Pbelieves(PreceivedF(X)如果一个主体理解一个消息，并看到此消息的一个函数，那么它理解它所看到的。F可视为加密函数，K为参数。,SVO逻辑的推理规则及公理续7,I7叙述公理一个主体说过一个级联消息，那么它一定说过且看到消息的每一部分。Psaid(X1,Xn)PsaidXiPseesXiPsays(X1,Xn)Psaid(X1,Xn)PsaysXi,SVO逻辑的推理规则及公理续8,仲裁公理PcontrolsPsays,SVO逻辑的推理规则及公理续9,I9新鲜公理如果消息的

6、一部分是新鲜的，那么整个消息也是新鲜的。fresh(Xi)fresh(X1,Xn)fresh(X1,Xn)fresh(F(X1,Xn)fresh(X)PsaidXPsaysX,SVO逻辑的推理规则及公理续10,I10共享密钥的良好对称性公理如果K是P，Q之间的良好密钥当且仅当K是Q，P之间的良好密钥。shared(P,K,Q)shard(Q,K,P),SVO逻辑的推理规则及公理续11,(11)I11所有公理PhasKPseesK,SVO逻辑语义计算模型,Pe：代表环境,可用于模拟攻击者的任意行为。Si:每个主体Pi有一个局部状态Si。全局状态:n+1维局部状态。主体行为:发送send(X,P)

7、、receive()和generate(X)，但只能生成集合T0中的元素,SVO逻辑语义计算模型续1,每一个行为导致状态的一次迁移。r:一轮协议r是一个由整数时间索引的全局变量的有限集合。r(t)：协议中的t时记为r(t)。ri(t):对应的主体Pi的局部变量记为ri(t)。环境状态：全局历史、环境有效迁移集合和用于保存发给主体P而P还未收到的消息的消息缓冲区。,SVO逻辑语义计算模型续2,主体Pi在(r,t)收到的消息集合包括：局部消息历史中或t之前出现的received(X)中的X。收到的消息的级联。P持有所收到的加密消息XK的解密密钥，则P可得到X。,SVO逻辑语义计算模型续3,主体Pi

8、在协议运行当中某处可看到的消息集合包含：主体已收到的消息集。主体新近生成消息集。主体初始所知的消息集。主体通过规则和公理从已知的消息集衍生的消息集。对于主体说过的消息集的定义比此严格。,SVO逻辑语义计算模型续4,主体Pi在(r,t)发送的消息集合包括：主体对已发送过消息的级联。加密密钥为主体所持有的加密消息的非加密部分，且此部分为主体所看到。签名密钥为主体所持有的签名消息的非签名部分，且此部分为主体所看到。Hash消息中的非Hash部分，且此部分为主体所看到。,SVO逻辑语义公式成立的条件,定义：将每一个常量命题pT映射为点集(p),即命题p为真的点。公式在点(r,t)为真记为：(r,t)。

9、意味着全真。,SVO逻辑语义公式成立的条件1,逻辑连接及其原始命题基本逻辑关系：(r,t)piff(r,t)(p)。(r,t)iff(r,t)(r,t)。(r,t)iff在(r,t)时不成立。,SVO逻辑语义公式成立的条件2,原始命题接收命题(r,t)preceivedX当且仅当X属于主体P在(r,t)时已收消息集合。,SVO逻辑语义公式成立的条件3,看到命题和持有命题(r,t)pseesX当且仅当X属于主体P在(r,t)时已看到消息集合。(r,t)phasX当且仅当X属于主体P在(r,t)时已收消息集合。,SVO逻辑语义公式成立的条件4,3)述说命题(r,t)psaidX当且仅当对于消息M在

10、协议t时之前，主体P发送过消息M，且X是M的子消息。,SVO逻辑语义公式成立的条件5,4)仲裁命题(r,t)pcontrols，当且仅当(r,t)psays且对于所有的t0,有：(r,t)。,SVO逻辑语义公式成立的条件6,5)新鲜性命题(r,t)fresh(X)当且仅当对于所有主体在本轮协议前没有说过X。,SVO逻辑语义公式成立的条件7,四种密钥命题：共享密钥公开加密密钥公开签名密钥公开协商密钥,SVO逻辑语义公式成立的条件8,共享密钥？(r,t)RreceivedXK或者RP,Q。,SVO逻辑语义公式成立的条件9,公开加密密钥(r,t)PK(P,K)当且仅当对于所有的t，若仅有(r,t)Q

11、seesXK，则Q=P。,SVO逻辑语义公式成立的条件10,公开签名密钥(r,t)PK(P,K)当且仅当对于所有的t，(r,t)QreceivedXK-1，则表明(r,t)PsaidX。,SVO逻辑语义公式成立的条件11,公开协商密钥(r,t)PK(P,K)当且仅当对于所有的t：对于某些Q，Kpq=f(K-1,PK(Q)且(r,t)goodkey(P,Kpq,Q)对于所有R，Kpr=f(K-1,PK(R)以及(r,t)goodkey(P,Kpr,R)且对于所有U，Kur=f(PK-1(U),PK-1(R)且(r,t)goodkey(U,Kur,R)。,SVO逻辑的应用实例,主体目标相同：密钥分

12、配和认证。则不大可能会出现否认性。主体目标不同：电子商务，为了利益需求，可能对已发生行为进行否认。收费后否认收费或者因质量问题而否认发货。解决：收集并持有一个声称事件或行为的不可否认证据，并使之能有效地用于解决由于否认事件或行为而引起的纠纷。,SVO逻辑的应用实例续1,Schneider在下列文献中运用通信顺序进程CSP对一个不可否认协议实例进行了形式化的描述与分析。SchneiderS.,VerifyingauthenticationprotocolswithCSP.ProceedingsoftheIEEEComputerSecurityFoundationsWorkshopX,IEEECo

13、mputerSociety,3-171997。用SVO也可对不可否认性进行分析。,SVO逻辑-一个不可否认协议实例,不可否认协议的实现：证据的生成证据的交换证据的验证纠纷的解决一是双方进行同时的秘密交换(麻烦，要求协议双方具有同等计算能力不现实)。二是借助一个可信第三方(TTP)。,SVO逻辑-不可否认协议实例续,两个基本证据：NRO(Non-repudiationofOrigin):发方不可否认。NRR(Non-repudiationofReceipt):收方不可否认。NRS:(Non-repudiationofSubmission):提交不可否认,证明已提交给了TTP，由提交方提供。NRD

14、:(Non-repudiationofDelivery):传递不可否认,证明TTP已交付给了意定接收者，由TTP提供。,SVO逻辑-不可否认协议实例续,【Zhou和Gollman提出】ZG协议AB:fNRO,B,L,C,NROBA:fNRR,A,L,C,NRRATTP:fNRS,B,L,K,NRS_KBTTP:fNRD,A,B,L,K,NRD_KATTP:fNRD,A,B,L,K,NRD_K,SVO逻辑-不可否认协议实例续,:ftp操作符。NRO=SA(fNRO,B,L,C)NRR=SB(fNRR,A,L,C)NRS_K=SA(fNRS,B,L,K)NRD_K=STTP(fNRD,A,B,L,

15、K),SVO逻辑-不可否认协议实例分析,定义3.1不可否认协议的公平性：是指从协议执行的开始到协议执行结束的任何一个阶段，通信的双方要么能够同时得到它们所期望的，要么任何一方都得不到有利于自己的信息，从而避免协议的任一方中断执行的协议，或否认其已发生的行为以达成利益不平等的可能。,SVO逻辑-不可否认协议实例分析,定理3.1一个不可否认协议的不可否认性是成立的，如果：协议任何一方执行后的中止将不会破坏通信双方主体的地位的公平性。在协议结束时提供主体参与协议行为的证据，即证据的有效性。,SVO逻辑-不可否认协议ZG证明,给出协议的前提或假设说明协议目标运用规则和公理进行推证,SVO逻辑-ZG证明

16、假设,给出协议的前提或假设A0:协议的运行环境是不安全的(基本假设)。A1:每个主体的公钥是公开的。A2:每个主体的私钥仅为其所知。A3:TTPbelievesSAA4:TTPbelievesSBA5:PbelievesSTTP:P为参与协议运行的主体A6:TTPbelieves(BreceivedC)TTPbelieves(AsaidC),SVO逻辑-ZG证明假设续,A7:Asaid(A,B,L,Ek(M)Asaid(A,B,L,K)AsaidMA8:Breceived(A,B,L,Ek(M)Breceived(A,B,L,K)BreceivedMA9:TTPbelieves(AsaidCB

17、receivedCTTPreceivedK)TTPsaysK表示TTP只有在确信A已说过C，并且B已收到了C，以及TTP收到了K，才将K公布到其公开目录中。A10：TTPsaysXPftpXPseesXTTP将其认为是有效的数据放入到其公共目录下，并可为任何主体通过ftp操作访问。,SVO逻辑-ZG证明假设续,A11:PbelievesPK(Q,K)PreceivedXK-1Pbelieves(QsaidX)表示如果P收到一个签名消息，并且P相信这个签名密钥是Q的，那么P相信Q说过X。A12:Abelivevesfresh(Na)A13:TTPbelieves,SVO逻辑-ZG证明协议目标,一

18、般目标：G1Abelieves(BreceivedM)G2Bbelieves(AsaidM)仲裁目标G3Jbelieves(AsaidM)G4Jbelieves(BreceivedM),SVO逻辑-ZG证明运用规则和公理进行推证,由消息1),得：F1:BreceivedSA(fNRO,B,L,C)由F1,A2,P4,A11,得：(P4:PK(A,K)BreceivedXK-1AsaidX)(A11:BbelievesPK(A,K)BreceivedXK-1)Bbelieves(AsaidX)得F2:Bbelieves(Asaid(fNRO,B,L,C),SVO逻辑-ZG证明运用规则和公理进行推

19、证续,由F2,P5(是哪一个？)得：F3:Bbelieves(AsaidC)同理，对原协议消息2)的分析只能得到Abelieves(BsaidC)，但无法得到Abelieves(BreceivedC),原协议修改为1)AB:fNRO,B,L,C,SA(fNRO,B,L,Na,C)2)BA:fNRR,A,L,C,SA(fNR,A,L,Na+1,C),SVO逻辑-ZG证明运用规则和公理进行推证续,对修改后的协议进行分析得：F4:AreceivesSB(FNRR,A,L,Na+1,C)由F4,A2,P4,A11,A12,得：F5:Abelieves(Breceived(fNRO,B,L,Na,C)A

20、believes(BreceivedC)由消息3)得：F6:TTPreceivedSA(FNRS,B,L,K),SVO逻辑-ZG证明运用规则和公理进行推证续,由F6,A2,A3得：F7:TTPbelieves(Asaid(fNRS,B,L,K)TTPreceivedK根据假设A9，TTP只有确信A已说过C，并且B收到C，以及TTP收到了K，才将K公布到其公开目录中，但在原有协议中，TTP并不能确知B是否已收到了C，因此，A可对NRR进行签名，并将结果发给TTP。对消息3)修改如下：,SVO逻辑-ZG证明运用规则和公理进行推证续,3)ATTP:fNRS,B,L,K,NRS_K,SA(NRR)TT

21、P收到消息3)后由P5得：F8:TTPreceivedSA(NRR)由F8,A3,A11,P1,得：F9:TTPbelieved(AsaidCBreceivedC)由F8,F9,A9,A6,得：F10:TTPsaysK,SVO逻辑-ZG证明运用规则和公理进行推证续,由F10,A10，消息4)得：F11:Breceived(fNRD,A,B,L,K,STTP(fNRO,A,B,L,K)由F11,P5,A13,得：F12:(BreceivedKBreceivedC)BreceivedM由F12,P6,A7,消息5)得：F13:Areceived(fNRD,A,B,L,K,STTP(fNRO,A,B

22、,L,K)由F10,F12,F13,A5,A11,P5,P7,P10,得：,SVO逻辑-ZG证明运用规则和公理进行推证续,F14:Abelieves(TTPsaysK)Abelieves(BseesK)Abelieves(BreceivedM)G1由F7,F11,A5,得：F15:Bbelieves(TTPsaysK)Bbelieves(AsaidK)由F3,F15,得：F16:Bbelieves(AsaidM)-G2,SVO逻辑-ZG证明运用规则和公理进行推证续,协议可能出现的纠纷及解决Case1A否认向B发送了消息M。在这种情况下B可将M,C,K,L以及NRO,NRD_K提交给仲裁，仲裁通过以下几步可证明A发送了消息M。检查NRD_K是用T的私钥对消