安全协议理论与方法

安全协议理论与方法基于推理结构性方法SVO逻辑Syverson和Oracho提出，建立了用于推证合理性的理论模型。1)提供独立明确的语义基础。2)相当详细的模型。消除理解模糊，有助于准确理解消息的真实含义和协议理想化。3)通用语义，扩展性好，简洁。SVO逻辑的基本结构1.术语集合。2.推理规则及公理。3.基于的假设。SVO术语集合1.定义T为初始术语集合,包括互不相交的常量符号集合：主体、共享密钥、公钥、私钥以及序列号等。2.n维函数表示有n个变量的函数，如加、解密函数等。3.消息语言MT：满足下列性质的最小语言集合。1)如果XT，则X是消息。2)如果X1,…,Xn是消息，F是任意一个n维函数,则F(X1,…,Xn)是消息。3)如果是公式，则是消息。SVO术语集合续4.公式语言FT：满足下列性质的最小公式集合。1)如果P是原始命题，则P是公式。2)如果,是公式，则和是公式。3)Pbelieves和Pcontrols是公式，其中P是主体，是公式。4)PseesX,PsaysX,PsaidX,PreceivedX和fresh(X)是公式,其中P是主体,X是消息。5)Shared(P,K,Q),PK(P,K)和PhasK是公式，其中P是主体，K是消息。SVO逻辑的推理规则及公理1.SVO逻辑遵从两条基本推理规则1)()╞2)╞PbelievesSVO逻辑的推理规则及公理续12.SVO逻辑共有20条公理(1)I1相信公理对于任一主体P和公式，有：1)PbelievesPbelieves()Pbelieves2)PbelievesPbelieves(Pbelieves)SVO逻辑的推理规则及公理续2(2)I2源关联公理密钥用于推断消息发送者的身份。1)shared(P,K,Q)Rreceived{XQ}KQsaidX2)(PKÓ(Q,K))Rreceived{X}K-1QsaidXPKÓ(Q,K)表示K是主体Q的数字签名验证密钥。它表明如果主体Q收到一个签名的消息，并且Q知道签名的验证密钥是K，就可以确定发送者身份。SVO逻辑的推理规则及公理续3(3)I3密钥协商公理(PK(P,KP)PK(P,Kq))shared(P,KPq,Q))Kpq=f(Kp,Kq-1)=f(Kp-1,Kq)f为密钥协商函数，比如Diffie-Hellman密钥交换。SVO逻辑的推理规则及公理续4I4接收公理主体对接收到的一个级联的加密消息可用有效的密钥解密。1)Preceived(X1,…,Xn)PreceivedXi2)Preceived{X}KPhasK-1PreceivedXSVO逻辑的推理规则及公理续5(5)I5看到公理1)PreceivedXPseesX2)Psees(X1,…,Xn)PseesXi3)PseesX1…PseesXnPsees(F(X1,…,Xn))主体只要接收到一个消息就看到了这个消息，并且看到了这个消息的每一部分。SVO逻辑的推理规则及公理续6(6)I6理解公理1)Pbelieves(PseesF(X))Pbelieves(PseesX)2)PreceivedF(X)Pbelieves(PseesX)Pbelieves(PreceivedF(X))如果一个主体理解一个消息，并看到此消息的一个函数，那么它理解它所看到的。F可视为加密函数，K为参数。SVO逻辑的推理规则及公理续7(7)I7叙述公理一个主体说过一个级联消息，那么它一定说过且看到消息的每一部分。1)Psaid(X1,…,Xn)PsaidXiPseesXi2)Psays(X1,…,Xn)Psaid(X1,…,Xn)PsaysXiSVO逻辑的推理规则及公理续8(8)仲裁公理PcontrolsPsaysSVO逻辑的推理规则及公理续9(9)I9新鲜公理如果消息的一部分是新鲜的，那么整个消息也是新鲜的。1)fresh(Xi)fresh(X1,…,Xn)2)fresh(X1,…,Xn)fresh(F(X1,…,Xn))3)fresh(X)PsaidXPsaysXSVO逻辑的推理规则及公理续10(10)I10共享密钥的良好对称性公理如果K是P，Q之间的良好密钥当且仅当K是Q，P之间的良好密钥。shared(P,K,Q)shard(Q,K,P)SVO逻辑的推理规则及公理续11(11)I11所有公理PhasKPseesKSVO逻辑语义—计算模型Pe：代表环境,可用于模拟攻击者的任意行为。Si:每个主体Pi有一个局部状态Si。全局状态:n+1维局部状态。主体行为:发送send(X,P)、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)收到的消息集合包括：1)局部消息历史中或t之前出现的received(X)中的X。2)收到的消息的级联。3)P持有所收到的加密消息{X}K的解密密钥，则P可得到X。SVO逻辑语义—计算模型续3主体Pi在协议运行当中某处可看到的消息集合包含：1)主体已收到的消息集。2)主体新近生成消息集。3)主体初始所知的消息集。4)主体通过规则和公理从已知的消息集衍生的消息集。对于主体说过的消息集的定义比此严格。SVO逻辑语义—计算模型续4主体Pi在(r,t)发送的消息集合包括：1)主体对已发送过消息的级联。2)加密密钥为主体所持有的加密消息的非加密部分，且此部分为主体所看到。3)签名密钥为主体所持有的签名消息的非签名部分，且此部分为主体所看到。4)Hash消息中的非Hash部分，且此部分为主体所看到。SVO逻辑语义—公式成立的条件定义：将每一个常量命题pT映射为点集(p),即命题p为真的点。公式在点(r,t)为真记为：(r,t)╞。╞意味着全真。SVO逻辑语义—公式成立的条件1(1)逻辑连接及其原始命题基本逻辑关系：(r,t)╞piff(r,t)(p)。(r,t)╞iff(r,t)╞(r,t)╞。(r,t)╞iff在(r,t)时不成立。SVO逻辑语义—公式成立的条件2(2)原始命题1)接收命题(r,t)╞preceivedX当且仅当X属于主体P在(r,t)时已收消息集合。SVO逻辑语义—公式成立的条件32)看到命题和持有命题(r,t)╞pseesX当且仅当X属于主体P在(r,t)时已看到消息集合。(r,t)╞phasX当且仅当X属于主体P在(r,t)时已收消息集合。SVO逻辑语义—公式成立的条件43)述说命题(r,t)╞psaidX当且仅当对于消息M在协议t时之前，主体P发送过消息M，且X是M的子消息。SVO逻辑语义—公式成立的条件54)仲裁命题(r,t)╞pcontrols，当且仅当(r,t)╞psays且对于所有的t’0,有：(r,t)╞。SVO逻辑语义—公式成立的条件65)新鲜性命题(r,t)╞fresh(X)当且仅当对于所有主体在本轮协议前没有说过X。SVO逻辑语义—公式成立的条件76)四种密钥命题：共享密钥公开加密密钥公开签名密钥公开协商密钥SVO逻辑语义—公式成立的条件8共享密钥？？(r,t’)╞Rreceived{X}K或者R{P,Q}。SVO逻辑语义—公式成立的条件9公开加密密钥(r,t)╞PK(P,K)当且仅当对于所有的t’，若仅有(r,t)╞Qsees{X}K，则Q=P。SVO逻辑语义—公式成立的条件10公开签名密钥(r,t)╞PK(P,K)当且仅当对于所有的t’，(r,t)╞Qreceived{X}K-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逻辑的应用实例1)主体目标相同：密钥分配和认证。则不大可能会出现否认性。2)主体目标不同：电子商务，为了利益需求，可能对已发生行为进行否认。收费后否认收费或者因质量问题而否认发货。解决：收集并持有一个声称事件或行为的不可否认证据，并使之能有效地用于解决由于否认事件或行为而引起的纠纷。SVO逻辑的应用实例续1Schneider在下列文献中运用通信顺序进程CSP对一个不可否认协议实例进行了形式化的描述与分析。SchneiderS.,VerifyingauthenticationprotocolswithCSP.ProceedingsoftheIEEEComputerSecurityFoundationsWorkshopX,IEEEComputerSociety,3-171997。用SVO也可对不可否认性进行分析。SVO逻辑-一个不可否认协议实例不可否认协议的实现：证据的生成证据的交换证据的验证纠纷的解决一是双方进行同时的秘密交换(麻烦，要求协议双方具有同等计算能力不现实)。二是借助一个可信第三方(TTP)。SVO逻辑-不可否认协议实例续两个基本证据：NRO(Non-repudiationofOrigin):发方不可否认。NRR(Non-repudiationofReceipt):收方不可否认。NRS:(Non-repudiationofSubmission):提交不可否认,证明已提交给了TTP，由提交方提供。NRD:(Non-repudiationofDelivery):传递不可否认,证明TTP已交付给了意定接收者，由TTP提供。SVO逻辑-不可否认协议实例续【Zhou和Gollman提出】ZG协议1)AB:fNRO,B,L,C,NRO2)BA:fNRR,A,L,C,NRR3)ATTP:fNRS,B,L,K,NRS_K4)BTTP:fNRD,A,B,L,K,NRD_K5)ATTP:fNRD,A,B,L,K,NRD_KSVO逻辑-不可否认协议实例续: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,K)SVO逻辑-不可否认协议实例分析定义3.1不可否认协议的公平性：是指从协议执行的开始到协议执行结束的任何一个阶段，通信的双方要么能够同时得到它们所期望的，要么任何一方都得不到有利于自己的信息，从而避免协议的任一方中断执行的协议，或否认其已发生的行为以达成利益不平等的可能。SVO逻辑-不可否认协议实例分析定理3.1一个不可否认协议的不可否认性是成立的，如果：1)协议任何一方执行后的中止将不会破坏通信双方主体的地位的公平性。2)在协议结束时提供主体参与协议行为的证据，即证据的有效性。SVO逻辑-不可否认协议ZG证明(1)给出协议的前提或假设(2)说明协议目标(3)运用规则和公理进行推证SVO逻辑-ZG证明假设(1)给出协议的前提或假设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)Asai