3 实例分析 3.1 SVO逻辑 SVO逻辑遵从两条推理规则和20条公理.两条规则为:I1:Ψ∧(ΨΦ)┣ Φ I2:┣ ΦP believes Φ 其中Ψ和Φ是公式,P表示主体,┣ Φ表示Φ是一个可由公理推导而来的公式.这里仅列出与证明有关的公理. 相信公理 对于任一主体P和公式Ψ,Φ有:P1:P believes Ψ∧ P believes(ΨΦ)P believesΦP2:P believes ΨP believes (P believesΨ) 主体相信由已有的信任关系逻辑推导出的所有信仰结果. 接收公理 P5:P received(X1,…,Xn)P received XiP6:P received{X}K∧P has K^-1P received X 主体对接收到的一个级联的加密消息可用有效的密钥解密. 看到公理 P7:P received XP sees XP8:P sees (X1,…,Xn) P sees Xi 主体只要接收到一个消息就看到了这个消息,并且看到了这个消息的每一部分. 理解公理 P10:P believes(P sees F(X))P believes(P sees X)P11:P received F(X)∧P believes(P sees X)P believes(P received F (X))如果一个主体理解一个消息,并看到此消息的一个函数,那么它理解它所看到的.F可视为加解密函数,K为参数. 叙述公理 P12:P said(X1,…,Xn)P said Xi∧P sees Xi一个主体说过一个级联消息,那么它一定说过且看到消息的每一部分. 3.2 形式化分析 首先,我们提出非否认协议公平性的定义. 定义3.1 非否认协议的公平性是指从协议执行的开始到协议执行结束的任何一个阶段,通信的双方要么能够同时得到它们所期望的,要么任何一方都得不到有利于自己的信息,从而避免协议的任一方中断执行的协议,或否认其已发生的行为以达成利益不平等的可能.其次,在定义3.1的基础上我们提出下面的定理说明. 第 1 期 范 红:一个非否认协议ZG的形式化分析 电 子 学 报 2005年 定理3.1 一个非否认协议的非否认性是成立的,如果:(1)协议任何一步执行后的中止将不会破坏通信双方主体的地位的公平性;并且,(2)在协议结束时提供主体参与协议行为的有效证据,即证据的有效性.最后,证明ZG协议的非否认性.证明:给出协议的前提或假设 A0基本假设:协议的运行环境是不安全的;A1:每个主体的公钥是公开的;A2:每个主体的私钥仅为其所知;A3:TTP believes S_A;A4:TTP believes S_B;A5:P believes S_TTP;P为参与协议运行的主体.A6:TTP believes (B received C)TTP believes (A said C)A7:A said (A,B,L,Ek(M))∧A said (A,B,L,K) A said M;A8:B received (A,B,L,Ek(M)) ∧ B received (A,B,L,K) B received M;上述的两个假设表示标识L可关联同一轮协议的不同消息.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 XP ftp XP sees X;TTP将其认为是有效的数据放入其公共目录下,并可为任何主体通过ftp操作访问.A11:P believes PK_ó(Q,K)∧ P received {X}K^-1 P believes (Q said X);表示P如果收到一个签名消息,并且P相信这个签名密钥是Q的,那么P相信Q说过X.这个假设是P4的一个扩展.A12:A believes fresh(Na);A13:TTP believesΨΨ. 说明协议目标 根据非否认协议所要达成的公平性和证据有效性,ZG协议的目标描述如下:一般目标:G1 A believes (B received M); G2 B believes (A said M).仲裁目标:G3 J believes (A said M); G4 J believes (B received M). 运用规则和公理进行推证 由消息(1),得:F1:B received SA(f_NRO,B,L,C).由F1,A2,P4,A11得:F2:B believes(A said(f_NRO,B,L,C)).由F2,P5,得:F3:B believes(A said C).同理,对原协议消息(2)的分析只能得到A 相信主体B说过C,而不能得到主体A关于B从A处接收到了C的信仰,故在原协议的NRO与NRR中增加新鲜随机数的挑战-质询,修改如下:(1')A→B:f_NRO,B,L,C,S_A(f_NRO,B,L,Na,C),(2')B→A:f_NRR,A,L,C,S_B(f_NRR,A,L,Na +1,C).对修改后的协议进行分析.由消息(2'),得:F4:A receives S_B(f_NRO,A,L,Na +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),由F6,A2,A3,得:F7:TTP believes (A said (f_NRS,B,L,K))TTP received K根据假设A9,TTP只在确信A已说过C,并且B收到C,以及TTP收到了K,才将K公布到其公开目录中,但在原有协议中,TTP并不能确知B是否已收到了C,因此,A可对NRR进行签名,并将结果发给TTP.对消息(3)修改如下:(3') A→TTP:f_NRS,B,L,K,NRS_-K,S_A(NRR),TTP收到消息(3')后由P5得:F8:TTP received S_A(NRR).由F8,A3,A11,P1得:F9:TTP believed (A said C ∧B received C).由F8,F9,A9,A6,得:F10:TTP says K.由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,得: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.由F14,F16,可得修改后的协议的一般目标是满足的,即协议任何一步执行后通信双方主体的地位是公平的.如果出现主体否认其协议行为,并引发纠纷,双方则可按要求向仲裁J出示证据,通过证明协议仲裁目标的满足与否来检验主体的否认行为的非否认性.我们假设J相信主体A,B,和TTP的签名私钥,并且知道与私钥对应的主体的公钥.协议可能出现的纠纷及解决,分以下两种情况:case1 A否认向B发送了消息M.在这种情况下B可将M,C,K,L,以及NRO,NRD_-K提交给仲裁,仲裁通过以下几步可证明A发送了消息M.(1)检查NRD_-K是用T的私钥对消息(f_NRO,A,B,L,K)的签名;J received S_TTP(f_NRO,A,B,L,K)J believes (TTP says K)J believes (A said K)(2)检查NRO是用A的私钥对消息(f_NRO,B,L,Na,C)的签名;J received S_A(f_NRO,B,L,Na,C)J believes (A said C)(3)如果检查M=D(K:C),则:J believes (A said M)得证G3. case2 B否认收到了消息M.在这种情况下A将M,C,K,L以及NRR,NRD_-K提交给仲裁,仲裁通过以下几步可证明B接收到了消息M.(1)检查NRD_-K是用T的私钥对消息(f_NRO,A,B,L,K)的签名;J received S_TTP(f_NRO,A,B,L,K)J believes (TTP says K)J believes (B received K)(2)检查NRR是用B的私钥对消息(f_NRO,A,L,Na+1,C)的签名;J received S_B(f_NRO,A,L,Na+1,C)J believes (B received C)(3)如果检查M=D(K:C),则:J believes (B received M)得证G4.以上的证明表明ZG协议能够为解决可能出现的纠纷提供有效的证据.修改后的协议为:(1)A→B:f_NRO,B,L,C,S_A(f_NRO,B,L,Na,C)(2)B→A:f_NRR,A,L,C,S_B(f_NRO,A,L,Na +1,C)(3)A→TTP:f_NRS,B,L,K,NRS_-K,S_A(NRR) (4)BTTP:f_NRD,A,B,L,K,NRD_-K(5)ATTP:f_NRD,A,B,L,K,NRD_-K 4 结束语 本文我们运用SVO逻辑对一个非否认协议实例-ZG协议的公平性与证据有效性进行了形式化分析,使非否认协议的多种性质的分析得以在同一形式化验证框架下进行,并修改了ZG协议存在的漏洞.非否认协议具有较大的应用价值,ZG协议为非否认协议的设计提供了一个极好的思路,因此对ZG协议进行严格的形式化分析,验证其正确性是十分必要的.如何建立此类协议的形式化分析工具的良好语义模型,并进行严格的理论推证需要进一步的工作. 参考文献:[1] J Zhen,D Gollmann.A fair non-repudiation protocol.In IEEE Computer Society Symposium on Research in Security and Privacy,1996. [2] M Abadi,A Gordon.A calculus for Cryptographic protocols:The spi calculus.Information and Computation,1998. [3] Schneider S.Verifying Authentication Protocols with CSP,Proceedings of the IEEE Comoputer Security Foundations Workshop X,(1997)3-17,IEEE Computer Society Press. [4] P F Syverson,P C van Oorschot.A Unified Cryptographic Protocol Logics.In Proceedings of the 1994 IEEE Computer Society Press,1994. [5] E F Brickell,D Chaum,I B Damgard,J van de Graaf.Gradual and verifiable release of a secret.Lecture-Notes in Computer Science 293,Advances in Cryptology:Proceedings of Crypto'87,pages 156-166,Santa Barbara,CA Auguest,1987. 作者简介:范 红 女,1969年7月出生于河北保定,博士研究生,研究方向为信息安全,在国内外刊物上发表论文20余篇,专著3本.E-mail:pkfanhong@sina.com 冯登国 男,1965年5月出生,陕西靖边人,研究员,博士导师,中科院信息安全国家重点实验室主任,国家信息安全863项目专家组组长,研究方向为信息安全,在国内外刊物上发表论文近200篇,专著15本.(编 辑:)