安全协议理论与方法-中国科学技术大学.ppt

安全协议理论与方法,基于推理结构性方法,Kailar逻辑,可追究性的分析。内容：某个主体要向第三方证明另一方对某个公式负有责任。,Kailar逻辑的基本结构,术语集合(基本语句)。推理规则及公理。基于的假设。,Kailar术语集合,A,B,C:协议主体。M：由一个主体发送给另一个主体的消息。TTP:可信第三方。Ki:主体i的公开密钥。Ki-1:与K对应的主体i的秘密密钥。x,y:为命题。,Kailar术语集合续,Kailar逻辑的基本语句如下：强证明弱证明签名认证消息解释声明断言签名消息的接收信任,Kailar术语集合续,(1).强证明：ACanProofx如果对于任一主体B,A执行一系列操作之后没有向B泄漏任何秘密消息y(y不等于x)并且能够使B相信x，则称主体A能够证明命题x。包括以下两种情况：可传递的证明不可传递的证明,Kailar术语集合续,可传递的证明如果A可向B证明x之后，B可向其他主体证明x的成立，则称A对于x的证明是可传递给B的。2）不可传递的证明如果B在A向其证明了x之后，并不能够向其他主体证明x是成立的，则称A对于x的证明是不可传递给B的。,Kailar术语集合续,(2)弱证明：ACanProofxtoB主体A可在不泄漏任何秘密的前提下向一个特定主体B证明x的成立。可传递证明不可专递证明,Kailar术语集合续,签名认证Ka可用于认证A对消息的签名，而且毫无疑问地可以将A与用Ka-1加密的消息相联系。消息解释xinmx为m中的可被理解的一个域或联合域。通常可被理解的域指明文或主体拥有密钥的加密域。,Kailar术语集合续,声明断言：Asaysx主体A声明x并对x及其所能够推导的公式负责，而且如果A对一个消息串负责，那么A也对每一个子消息负责，即：Asays(X,Y)=Asaysx,Kailar术语集合续,签名消息的接收：AReceivedmSignedWithK-1AReceivedmSignedWithK-1:xinmAReceivedxSignedWithK-1,Kailar术语集合续,信任:AIsTrustedOnxA对公式x具有管辖权。信任可分为两个级别：全局信任：如果A是全局可信的,那么对于所有主体有AIsTrustedOnx。2)非全局信任：如果A是非全局可信的,那么对于所有主体有AIsTrustedOnxbyB。,Kailar分析假设,数字签名算法诚实性消息完整性服务器的有效性,Kailar分析假设,数字签名算法假设算法是完美的，不会被破解，可提供消息源的认证、消息内容的完整性和消息发送者的不可否认性。诚实性在非对称密码体制中，主体不会将其私钥泄漏给其他人而在对称密码体制中，主体不会伪装成与其共享密钥的主体。,Kailar分析假设,(3)消息完整性不可能用其他消息部分伪造签名消息或者计算出主体的私钥密钥并进而伪造签名。服务器的有效性语句ACanProofx表明，在未来某个时间A可以发送一些消息来证明x，而一旦出现拒绝服务问题使得A无法发送消息以证明x的成立，那么此类问题将被消除以保证服务器的有效性。,Kailar基本推理规则,一般规则1)联接2)蕴含3)信仰关系4)强弱证明关系5)全局与非全局的可信性可追究性规则1)签名2)信任,Kailar基本推理规则,一般规则联接Conj:ACanProvex;ACanProveyACanProof(xy)蕴含Inf:ACanProvex;xyACanProvey,Kailar基本推理规则,信仰关系(ABlievesx)iff(ACanProvextoA)A相信x,当且仅当A能够对其自己证明x是成立的。强弱证明关系(S:CCanProvey)(ACanProvex)(S:CCanProveytoB)(ACanProvextoB),Kailar基本推理规则,全局与非全局的可信性(S:CIsTrustedOny)(ACanProvex)(S:CIsTrustedOnybyB)(ACanProvextoB)解释：如果C是为y所信任的，能够导致A能证明x,那么，在同样条件下，C通过B为y所信任可导致A能向B证明x的成立。,Kailar基本推理规则,可追究性规则签名当一个主体对一个消息签名之后，则签名消息就与主体进行了绑定并具有可追究性。Sign:AReceives(mSignedWithK-1);xinm;ACanProve(KAuthenticatesB)ACanProve(BSaysx),Kailar基本推理规则,信任Trust:ACanProve(BSaysx);ACanProve(BIsTrustedOnx)ACanProvex如果A能够证明B声明了x,并且能够证明B对公式有管辖权，那么A能够证明公式x成立。,Kailar逻辑的应用实例,明确协议的可追究性目标。说明协议语句，并将其转化为逻辑公式。(关注签名)初始化协议假设条件。运用推理规则对形式化分析协议是否达成可追究性目标。如果未达成则意味着协议有漏洞。,Kailar逻辑的应用实例续,CMP1协议(电子邮件的不可否认性)AB:A,B,S,h(M),Kks,A,B,S,Mka-1kBS:A,B,S,h(M)kb-1,Kks,A,B,S,Mka-1kSB:A,B,S,Mka-1ks-1SA:A,B,S,h(M)kb-1,B,Mks-1本协议将反复执行3)4)步，以保证A和B都能收到相应的消息。,Kailar逻辑的应用实例续,CMP1协议的目标形式化描述为：(G1)ACanProve(BreceivedM)(G2)BCanProve(ASentM),Kailar逻辑的应用实例续,协议语句的形式化：2)SReceivesh(M)SignedWithkb-12”)SReceivesh(M)SignedWithka-13)BReceivesh(M)SignedWithka-1)SignedWithks-14)AReceives(h(M)SignedWithkb-1SignedWithks-14”)AReceives(B,M)SignedWithks-1,Kailar逻辑的应用实例续,协议的初始假设I1:A,BCanProve(KsAuthenticatesS)I2:A,SCanProve(KbAuthenticatesB)I3:B,SCanProve(KaAuthenticatesA)I4:A,BCanProve(SIsTrusted(Ssay)I5:ASaysMASentMI6:BSaysh(M)BReceivedh(M),Kailar逻辑的应用实例续,I7:SSay(B,M)SSay(MhadbeensenttoB)I8:BReceivesh(M)MhadbeensenttoBBReceivedM前四条是基本假设。后四条是扩展假设，合理性需要推敲。,Kailar逻辑的应用实例续,逻辑分析：1.由公式2)和初始假设I2，应用签名规则可得：公式2)SReceivesh(M)SignedWithkb-1初始假设A,SCanProve(KbAuthenticatesB)AReceives(mSignedWithK-1);xinm;ACanProve(KAuthenticatesB)ACanProve(BSaysx)结论：SCanProve(BSaysh(M),Kailar逻辑的应用实例续,2.由上述结论和初始假设I6,应用蕴含规则可得：I6:BSaysh(M)BReceivedh(M)蕴含规则：Inf:ACanProvex;xyACanProvey结论：SCanProve(BReceivedh(M),Kailar逻辑的应用实例续,3.由公式2”)和初始假设I3,应用签名规则可得：公式2)SReceivesh(M)SignedWithka-1I3:B,SCanProve(KaAuthenticatesA)结论：SCanProve(ASaysM),Kailar逻辑的应用实例续,4.由上述结论和初始假设I5，应用蕴含规则可得：初始假设I5:ASaysMASentMSCanProve(ASentM),Kailar逻辑的应用实例续,5.由公式3)和初始假设I1,应用签名规则可得：3)BReceivesh(M)SignedWithka-1)SignedWithks-1I1:A,BCanProve(KsAuthenticatesS)结论：BCanProve(SSays(MSignedWIthks-1),Kailar逻辑的应用实例续,由上述结论和初始假设I4,应用信任规则可得：信任规则：Trust:ACanProve(BSaysx);ACanProve(BIsTrustedOnx)ACanProvexI4:A,BCanProve(SIsTrusted(Ssay)结论：BCanProve(MSignedWithKs-1),Kailar逻辑的应用实例续,7.对上述结论再次应用签名规则可得：结论：BCanProve(ASaysM)8.由上述结论和初始假设I5,应用蕴含规则可得：结论：(G2)BCanProve(ASentM),Kailar逻辑的应用实例续,证明G11.同理，由公式4)和初始假设I1、I4和I6，应用签名、信任和蕴含规则可得：结论：ACanProve(BReceivesh(M),Kailar逻辑的应用实例续,2.由公式4”)和初始假设I1,应用签名规则可得：公式4”)AReceives(B,M)SignedWithks-1结论：ACanProve(SSays(B,M),Kailar逻辑的应用实例续,3.对以上结果和初始假设I7，应用蕴含规则可得：I7:SSay(B,M)SSays(MhadbeensenttoB)结论：ACanProveSSays(MhadbeensenttoB),Kailar逻辑的应用实例续,4.对以上结果和初始假设I4,应用信任规则可得：I4:A,BCanProve(SIsTrusted(Ssay)信任规则：Trust:ACanProve(BSaysx);ACanProve(BIsTrustedOnx)ACanProvex结论：ACanProve(MhadbeensenttoB),Kailar逻辑的应用实例续,由前述结论ACanProve(BReceivesh(M)ACanProve(Mhadbeens