不可否认协议分析的增广CSP方法.doc

第10期韩志耕等：不可否认协议分析的增广CSP方法17不可否认协议分析的增广CSP方法韩志耕, 罗军舟, 王良民(东南大学 计算机科学与工程学院, 江苏 南京 210096)摘 要：提出一种适用于不可否认协议分析的增广CSP(communicating sequential processes)方法。检验有效性时使用它分析了Zhou等人于1996年提出的公平不可否认协议及其变体的安全性。结果表明该方法不仅能分析一些其他方法无法描述的协议性质，而且还发现了该协议的一个许多其他方法不能发现的已知缺陷；同时还证明协议变体增强了安全性。最后从语义和理论依赖2个角度讨论了方法正确性，并给出与其他方法相比所具备的优势。关键词：不可否认；增广CSP方法；公平性；时限性；形式化方法中图分类号：TP393 文献标识码：A 文章编号：1000-436X(2008)10-0008-11Extended-CSP based analysis of non-repudiation protocolsHAN Zhi-geng, LUO Jun-zhou, WANG Liang-min(School of Computer Science and Engineering, Southeast University, Nanjing 210096, China)Abstract: A new formal method named extended-CSP approach was proposed for non-repudiation protocols. For checking its validity, both the well-known Zhou-Gollmann fair non-repudiation protocol presented by Zhou et al. in 1996 and one of its variant protocol were analyzed with this method. The result showed that this method not only could be used to analyze some security properties that could not be described by other methods, but also detected a known flaw of the protocol which could not be found by others, and meanwhile proved the variant protocol really enhancing its security. Finally, the correctness of this method was surveyed from the points of both its semantic and theory dependency, and some advantages in comparison with others were also showed together.Key words: non-repudiation; extended-CSP approach; fairness; timeliness; formal method1 引言收稿日期：2008-06-21；修回日期：2008-09-20基金项目：国家自然科学基金资助项目(90604004, 60703115)；江苏省自然科学基金资助项目(BK2007708, BK2008030)；江苏省“网络与信息安全”重点实验室基金资助项目(BM2003201)；科技部国际科技合作项目Foundation Items: The National Natural Science Foundation of China (90604004, 60703115); The Natural Science Foundation of Jiangsu Province (BK2007708, BK2008030); The Key Laboratory of Network and Information Security of Jiangsu Province (BM2003201); International Science and Technology Cooperation Program of China新技术的不断发展，网络系统愈加复杂异构，网络异常及攻击行为日益多样化，服务质量的需求不断演化，这一切使得构建可信可控的网络体系来保障网络的安全性、可信性及可扩展性具有重要的意义。纵观现存的网络体系结构要么是基于边缘论和面向非连接的设计思想，使得分组传输路径不可控，要么是重新设计现有网络的体系结构，代价巨大。认为新体系结构可在不破坏网络现有架构的基础上通过增加一个可信可控的4层逻辑结构来构建，以此确保网络组元及用户行为的可预期、可管理。不可否认服务作为保障该架构正确实施的关键，需要得到安全的不可否认协议的支持。不可否认协议主要用于为网络实体之间的交互行为提供不可抵赖的证据1，通常该类协议必须具备的基本安全性质为不可否认性、公平性和时限性2。形式化方法是确保该类协议正确性与安全性的重要手段，然而目前仍缺少针对它们的有效方法，所有对不可否认协议的分析基本上都是采用已有的安全协议或通信协议的方法进行，包括有限状态分析Mur3、概率模型检查器PRISM4、基于Prolog规则的协议验证工具5,6、博弈论7、定理证明器Isabelle8等。虽然可用于不可否认协议分析的方法很多，但仍没有一种方法能完全描述该类协议的所有性质并保证协议的绝对安全。目前最常用的2类技术(状态检测和逻辑推理)各有利弊，当前的趋势是综合利用多种分析手段，取长补短，发现更多的安全缺陷，以期达到更好的分析效果。本文通过扩展进程代数CSP，将其应用于不可否认协议的描述与分析。一方面，既可以描述并分析许多其他方法无法描述的协议性质，另一方面，又可以为该类协议的分析提供一种新方法。CSP作为用于解决并发现象的代数理论9，也可用于安全协议的描述与分析10。第1个使用CSP对不可否认协议建模与分析的是Schneider，他给出了适用于不可否认协议手工分析的秩函数(rank function)方法11；Evans等人提出了使用PVS自动化分析不可否认协议的扩展秩函数方法12；Wei等人则提出了一种使用FDR对具备时间控制信息的不可否认协议进行自动化验证的方法13。但目前还没有出现使用CSP建模与分析该类协议所有安全性质的公开例子。本文以秩函数理论14,15为基础，通过扩展CSP提出了适用于不可否认协议建模与分析的增广CSP方法。然后使用该方法对Zhou等人于1996年提出的公平不可否认协议(Zhou-Gollmann协议)16及其变体17进行了分析。Zhou-Gollmann协议有一个已知缺陷，即不具备时限性17，虽然Zhou等人使用SvO逻辑18，Schneider基于秩函数方法，Paulson等人使用定理证明器Isabelle19，以及Grgens等人使用异步积自动机和同构验证工具20对其进行过验证，但都没能发现该缺陷，而使用本文给出的新方法则可以检测出此缺陷。本文第2节提出了适用于不可否认协议分析的增广CSP方法，同时还给出了建模与分析该类协议的具体过程。为检验新方法的有效性，第3节和第4节使用其分别对Zhou-Gollmann协议及其变体的安全性进行了分析。第5节讨论了新方法的正确性、与其他方法相比较所具备的特色。第6节为结束语。2 增广CSP方法不可否认协议的目标是维持不同时间上协议实体间协议状态的公平关系21，这表明该类协议对时间敏感，验证它们的安全性须采用具备时间描述与分析能力的形式化工具。CSP对时间的描述能力非常弱，只能通过迹中协议事件出现的顺序来区分它们发生的先后关系，无法描述发生的具体时间；而不可否认协议中影响协议状态公平性的正是协议事件(信息发送和接收)的发生时间。虽然目前存在的两类改善CSP时间描述能力的方法也可用于分析不可否认协议：一类为时控CSP(timed CSP)，将非负实数时间附加到迹中每个事件上22，另一类为非时控CSP，将可在规定时间间隔内发生的额外事件tock添加到字母表中23。但发现：1) 非时控CSP方法无法描述此类协议所关注的连续时间；2) 时控CSP方法虽适合于描述连续时间，却很难将时间敏感与非敏感性质区别对待。为此，本文提出增广CSP方法，一方面，它不但适用于描述与分析不可否认协议所有的安全性质；另一方面，在分析过程中还能依据性质对时间的敏感程度有区别地对待。增广CSP方法的事件定义为c. i. j. m. T，包括信道c、信源i、信宿j、信息m和时间表达式T。时间表达式T用于描述协议事件发生的具体时间，此处采用文献24中的定义：令R+=i | i R i 0 (R为实数集), T为时间表达式当且仅当：1) x是时间常元，如果x R+；2) X是时间变元，如果X是定义域R+上的变元；3) X |TS是时间绑定表达式，如果X是时间变元，且TS R+；4) T是时间表达式，如果M为时间绑定表达式，且T可表示为M。后文中时间常元和时间变元分别用带下标的t和T表示。时间绑定表达式X |TS为时间变元X赋予一个有确定值的时间常元t (t TS)。一旦时间变元被某表达式绑定，到绑定释放前该变元都视为时间常元，且不可再次绑定；规约中时间表达式X |R+缩写为X；当x为时间常元或已绑定值的变元时，x可表示为X |x。分析非时间敏感的性质时，无须关心协议事件中的时间，不会破坏分析结果的正确性。采用Mft1,t2,tn标识添加了时间表达式后的有序集M，此处n为M中事件个数，且有t1t2tn。与本文中协议分析相关的增广CSP部分语法描述如下。1) Stopf为死锁进程。2) 进程(cP)ft1,t2,tn在执行完事件c. i. j. m. t0后表现为进程Pft1,t2,tn。3) 基于初始事件集c. i. j. m. t，外部选择进程(P1P2)fnt1,t2,tn表现为进程(P1)ft11, t12, t1n或(P2)fnt21, t22, t2n；内部选择进程(P1P2)ft1, t2, tn非确定性地表现为进程(P1)ft11, t12, t1n或(P2)ft21, t22, t2n。4) 并发进程(P1|D|P2)ft1, t2, tn是同步于事件集(D)ft1, t2, tn的进程(P1) ft11, t12, t1n与(P2)ft21, t22, t2n的并发执行；进程(P1|P2)ft1, t2, tn标识该并发进程无相应的同步事件。5) 进程(P)fnt1,t2,tn的失效failure (P)ft1,t2,tn)定义为元组(tr)ft11, t12, t1n, (X)ft21, t22, t2n )的集合，其中(tr)ft11, t12, t1n为迹，(X)ft21, t22, t2n标识(P)ft1,t2,tn执行(tr)ft11, t12, t1n之后拒绝执行的事件集。增广CSP方法基于如下4步来建模与分析不可否认协议。第1步：给出建模和分析过程中要用到的时间常元和变元。常量的实际值无须给出，但应指出不同时间常元间的约束关系。第2步：建立增广CSP模型，包括协议整体模型、实体模型，以及信道模型等。第3步：用增广CSP方法描述协议安全性质，其中：1) 安全规约作为迹谓词给出，即若进程(P) ft1,t2,tn的所有迹都满足规约S(tr) ft11, t12, t1n), 则(P)f t1,t2,tn sat S(tr)f t11, t12, t1n) (tr)ft11, t12, t1ntraces(P)ft1,t2,tn) S(tr)f t11, t12, t1n)；2) 活性规约作为失效谓词给出，即若(P)f t1,t2,tn的所有失效都满足S(tr)f t11, t12, t1n, (X)ft21, t22, t2n)，则(P)f t1,t2,tn sat S(tr)f t11, t12, t1n, (X)ft21, t22, t2n) (tr)ft11, t12, t1n, (X)ft21, t22, t2n) failures(P)f t1,t2,tn) S(tr)ft11, t12, t1n, (X)ft21, t22, t2n)。其中相关事件之间的时间约束关系在规约中得到了体现。第4步：验证协议安全性质是否得到满足。安全性和活性主要依靠秩函数和组件活性来保证。在完成时间敏感性质中非时间相关部分的分析后，还需基于初等代数和集合理论分析事件之间的时间约束关系；而在分析非时间敏感性质时则无需该过程。3 Zhou-Gollmann协议的形式化分析协议描述中要用到的部分符号为AB: X表示实体A向实体B发送信息X；AB: X表示实体A从实体B处获取信息X；eK(X)和dK(X)表示用密钥K通过对称加密系统将信息X加/解密；sK(X)表示用私有密钥K对信息X 进行数字签名。协议将待发送的信息M分为2部分：加密密钥K和密文C。首先实体A将C 发送给实体B，B用消息EOR进行响应；接着A将K发送给实体TTP(trusted third party)，TTP 将该密钥发布在公共目录中；之后B能从TTP处获得K，从而可解密C获得M，同时A也能获得证据con_K。协议假设网络非永久不可用，故只要TTP发布了K，B总能在合适的时候获得它。交互步骤为：1) AB: fEOO , B, L, C, EOO2) BA: fEOR , A, L, EOR3) ATTP: fSUB , B, L, K, sub_K4) BTTP: fCON , A, B, L, K, con_K5) ATTP: fCON , A, B, L, K, con_KEOO=sSA (fEOO , B, L, C);EOR=sSB (fEOR , A, L, C);sub_K=sSA (fSUB , B, L, K);con_K=sST (fCON , A, B, L, K);协议执行后，若A否认发送过M给B，B可将证据EOO 和con_K 提交给仲裁者J进行仲裁；若B否认接收过M，A可将证据EOO, EOR和con_K提交给J仲裁。3.1 协议模型分析中要用到的时间常元有 t0, tA和tB, 其中t0表示最长网络不可用时间，tA和tB分别表示A和B发送完一个消息后等待下一消息的最长时间。要用到的时间变元有Ts, Tr, To, TA, TB, Tx, Ty, TFA, TFB。根据协议上下文语义，不可否认性源自仲裁者J的视角，关注纠纷中J对证据的仲裁结果；公平性和时限性源自协议实体的视角，关注实体对有利证据的获取。该协议的增广CSP模型描述如下。1) 信道模型。 空闲时只能接收消息，即MEDIUM(f) = trans? i? j? m. t MEDIUM( i, j, m, t) 非空闲时，可接收消息、递交消息、非确定性地丢失消息，但不可更改消息和误递交消息，即MEDIUM(S) = trans? i? j? m. t MEDIUM(S( i, j, m, t) (i, j, m, t)S rec.j!i!m.tMEDIUM(S(i, j, m, t) (i, j, m, t)S MEDIUM(S(i, j, m, t)2) 协议实体模型。 拥有信息S的实体可发送消息、从信道接收消息、使用ftp-get获取消息、将消息作为证据递交，即AGENTi (S) = jUSER, S (i) m trans. i! j! m. tAGENTi (S) rec.i?j?m.t AGENTi (Sm) ftp.i.TTP?m.t AGENTi (Sm) S (i) m evidence. i! m. t AGENTi (S) 实体与TTP间的弹性信道保证实体总可通过ftp检索到所需的信息，即引理1 AGENTi (S) sat ftp. i. TTP. m. t X。3) TTP行为模型。 TTP接收协议交互步骤3)中的签名消息、或让其余实体从其公共目录中检索消息，即：TTP(S) = rec. TTP? j? sj (fSUB . b. l. k). t TTP(SsT(fCON . j. b. l. k)jUSER, m M ftp. j. TTP. m. t TTP(S) TTP是称职的，它只有在收到sub_K后才会产生证据，且其不会拖延时间。只要TTP发布了证据，任一实体i就可在此后t0时间内收到该证据，即引理2 TTP(f) sat ftp. i. TTP. (sT(fCON . j. b. l. k) ). Tx in trrec. TTP. j. ( sj (fSUB . b. l. k) ). Ty|x|Txt0xTx in tr。 TTP满足活性：实体i从TTP处检索到消息可保证其余实体也可检索到该消息，即引理3 i and i,TTP(S) sat ftp. i. TTP. ( sT(fCON . j. b. l. k) ). Tx in tr ftp. i. TTP. ( sT(fCON . j. b. l. k) ). Ty|x| Tx x X4) 协议整体模型。Zhou-Gollmann协议证据通过数字签名技术构造，确保由si签名的消息必定是由实体i所发送。引理4和引理5给出了证据的2种使用情形(证据提交和消息接收)。引理4 m, $i, ijiTTP, NETWORK sat evidence.j.si(m).Tx in tr i sent si(m) at Ty|x| xTx 。引理5 i, j, m,NETWORK sat j received si(m) at Tx i sent si(m) at Ty|x| xTx 。Where i sent m at Tx=$M: MESSAGE; j: USER trans. i. j. M. Tx in tr M contains m。NETWORK= (|iUSER AGENTi ( INITi ) |ftp| TTP) | trans, rec| MEDIUM(f)。j received m at Tx=$M: MESSAGE; i: USER rec. j. i. M.Tx in tr M contains m.引理4和引理5作为本文核心定理，在附录部分将给出证明。协议中TTP通过ftp服务提供部分证据给其他实体，即引理6 m, $ j, jTTP, NETWORK sat evidence. j. sT(m).Tx in tr$i ftp. i. TTP. sT(fCON . i. j. l. k).Ty|x|xTx in tr。该引理可通过构造合适的秩函数来证明NETWORK满足此规约。此外，由引理2和引理5可得如下推论。推论1 NETWORK sat ftp. i. TTP. sT(fCON . i. j. l. k). Tx in tr i sent si(m) at Ty|x| xTx 3.2 分析不可否认性不可否认性确保协议能在通信事件发生后防止某些实体否认该事件的发生。协议成功运行后，引发的纠纷包括发送否认(B收到M，但A否认发送过该消息)和接收否认(A发送了M，但B否认收到该消息)。确保协议具备不可否认性是纠纷可被成功解决的关键。分析不可否认性时无需关心协议实体是否遵循协议执行。1) 发送不可否认性NRO (non-repudiality of origin)协议认为若B拥有EOO, con_K及L, C, M, K, 则A肯定发送过EOO, sub_K, 即有规约NRO (tr) evidence.B.EOO.TB in tr evidence.B.con_K TB in tr A sent EOO at Tr |x| x TB A sent sub_K at Ts|x| x TB 。此处需要验证NETWORK sat NRO (tr)能否成立。证明 由引理4有NETWORK sat evidence. B.EOO.Tx in trA sent EOO at Ty|x| xTx ；再由引理6和推论1有NETWORK sat evidence.B. con_K. Tx in tr A sent sub_K at Ty|x| xTx 。故有NETWORK sat NRO (tr)，即Zhou-Gollmann协议具备发送不可否认性。2) 接收不可否认性NRR (non-repudiality of receipt)协议认为若A拥有EOR, con_K及L, C, M, K, 那么B必定发送了EOR, 且其可从TTP处获得con_K, 采用规约NRR (tr, X)表示，即 NRR (tr, X)evidence. A. EOR. TA in trevidence. A. con_K. TA in trB sent EOR at Tr |x| xTA ftp. B. TTP. con_K. Ts X. 下面验证NETWORK sat NRR (tr, X) 能否成立。证明 依次应用引理1、引理6和引理3有NETWORK sat evidence. A. con_K. Tx in tr ftp. B. TTP. con_K. Ty X；再由引理4有NETWORK sat evidence. A. EOR. Tx in tr B sent EOR at Tr |x| xTx 。 故有NETWORK sat NRR (tr, X)，即Zhou-Gollmann协议具备接收不可否认性。所以，该协议具备不可否认性。3.3 分析公平性公平性保证在协议执行完后，要么所有实体都能收到所期望的不可抵赖证据，要么都收不到对己有利的证据，从而确保协议中任何实体都无法欺骗其他实体2。分析公平性之前需要指出的是，该协议蕴含这样的事实，即实体永远不可能做对己无利的事，否则其必然会在日后的纠纷处理中处于不利地位；B仅在收到EOO后才发送EOR，A仅在收到EOR后才提交sub_K. 即事实：AGENTA (S) sat trans.A!TTP!(sA (fSUB .i.L.K).Tsrec.A. i.(sB (fEOR .A.L.C).Tr|x|xTs。事实：AGENTB (S) sat trans.B!i! (sB (fEOR .i.L.C).Tr rec.B?i? (si (fEOO .B. L.C).To|x| xTr。协议要求实体仅在遵循协议执行时才能确保公平性。不考虑网络响应速度、TTP特性以及实体数量和自身能力带来的超时问题25，实体A和B正确执行协议的增广CSP模型用进程PROT_AGENTA和PROT_AGENTB表示如下。PROT_AGENTA = trans. A! B! (sA (fEOO . B. L. C). To rec. A. B. ( sB (fEOR . A. L. C). Tr |x| Tox trans. A! TTP!( sA (fSUB . B. L. K). Ts|x| Trx(源于事实) ftp. A. TTP. (sT (fCON . A. B. L. K). TA |x| TsxTs+t0(应用引理2) FINISHEDA (sB (fEOR . A. L. C), sT (fCON . A. B. L. K) at TFA|x|TAx。PROT_AGENTB = rec. B? i? (si (fEOO . B. L. C). To trans. B! i! ( sB (fEOR . i. L. C). Tr |x| To x(源于事实) ftp. B. TTP? (sT (fCON . i. B. L. K). TB |x| TsxTs + t0(应用引理2) FINISHEDB (si (fEOO. B. L. C), sT (fCON . i. B. L. K) at TFB |x|TBx。协议中实体通过ftp方式获得的信息将作为最终证据呈现，采用增广CSP方法描述为AGENTi sat ftp. i. TTP. m. Tx in tr evidence. i. m. Ty |x| Txx X，因此有NETWORK sat ftp. i. TTP. m. Tx in tr evidence. i. m. Ty |x| Txx X。此外，协议还假设TTP不会删除其公共目录中的信息，故实体总能通过ftp获得相关信息，即ftp. i. TTP. m. To X.1) A关注消息接收的公平性(fairness for A concerning message receipt)协议认为若B拥有消息M, 则A必拥有M的接收证据。这是因为：仅A知道K, 且A仅将K提交给TTP一次；当且仅当TTP向其余实体公开K时，B才能获得M。 即有规约FAIR1(tr, X) evidence. B. M. TB in tr ftp. A. TTP. con_K. TAX (evidence. A. EOR. TAX evidence. A. con_K. TAX)。由于A事先无法确保其他实体遵循协议执行，故此处仅需验证(PROT_AGENTA | (| iA AGENTi) |ftp| TTP ) |trans, rec| MEDIUM sat FAIR1(tr, X)。借助3.1节中相关引理很容易证明sat关系成立，具体过程略。2) B获得证据的公平性(fairness for B obtaining evidence)协议认为若A拥有M的接收证据，则B一定能M的发送证据。即有规约FAIR2(tr, X)evidence. A. con_K. TA in trevidence. A. EOR. TA in tr ftp.B.TTP. con_K.TBX (evidence. B. EOO.TB X evidence.B. con_K.TBX). 由于B事先也无法确保其他实体正确执行协议步骤，故此处仅需验证(PROT_AGENTB | (| iB AGENTi) |ftp| TTP ) |trans, rec| MEDIUM sat FAIR2(tr, X)。容易验证，略。3) A获得证据的公平性(fairness for A obtaining evidence)协议认为若B拥有M的发送证据，则A一定能获得M的接收证据。即有规约FAIR3(tr, X)evidence.B. con_K. TB in trevidence.B. EOO. TB in tr ftp.A.TTP. con_K. TAX (evidence.A.EOR. TA Xevidence. A. con_K. TAX). A无法保证其他实体正确执行协议步骤，故此处仅需验证(PROT_AGENTA | (| iA AGENTi) |ftp| TTP ) |trans, rec| MEDIUM sat FAIR3(tr, X)，容易验证，略。以上分析表明该协议具备公平性。3.4 分析时限性时限性保证诚实的协议实体在协议执行的任何阶段都能采取措施在有限时间内结束协议运行，以免实体在不知道协议是否已结束的情况下需要无限期地维持协议状态以获取公平。不可否认协议中影响时限性的关键是协议事件(信息发送和接收)发生的时间，分析协议的时限性分2步完成。1) 协议认为若A收到了TTP发布的证据，它一定是在将sub_K提交给TTP后有限的时间内收到该证据的，而不可能是在证据被删除后收到的(事实上TTP不可能无限期保存证据)；即有规约TIMELINESS1(A) A sent M at Tx A received con_K at Ty |x|Tx x Tx+tA 。下面通过分析(PROT_AGENTA | (| iA AGENTi) |ftp| TTP) |trans, rec| MEDIUM sat TIMELINESS1(A)是否成立来证明该协议能否保证对发送者A公平。证明 根据3.1节中相关引理容易验证(PROT_AGENTA | (| iA AGENTi) |ftp| TTP ) |trans, rec| MEDIUM sat A sent M A received con_K成立，现检验Tyx|TxxTx+tA是否成立。根据3.3节中进程PROT_AGENTA定义，令Tx = max(To, Ts), Ty = TA。因为Ty = TA且TAx|Ts x Ts + t0，有Ts Ty Ts + t0. 又Tx = max(To, Ts) = Ts(To Tr Ts)，故有Tx Ty Tx + t0，所以只要tA t0, 即可保证Tyx|TxxTx+tA。故(PROT_AGENTA|(|iAAGENTi)|ftp|TTP)trans, rec|MEDIUM sat TIMELINESS1(A)。2) 同样，若B收到了TTP发布的证据，它一定是在将EOR提交给A后有限的时间内收到该证据；即有规约TIMELINESS2(B) B received M at Tx B sent EOR at Ty |x|Tx tB xTx。下面通过分析(PROT_AGENTB | (| iB AGENTi) |ftp| TTP ) |trans, rec| MEDIUM sat TIMELINESS2(B)是否成立来证明该协议能否保证对接收者B公平。证明 仅检验时间约束部分Tyx|Tx tB x Tx。由3.3节进程PROT_AGENTB定义，令Tx = max(To, TB), Ty = Tr。因为Tx = max(To, TB)且To Tr Ts TB, 有Tx = TB。又因为TB x|Ts x Ts + t0, 得Ts Tx Ts + t0。考虑到Tr Ts, 有0 Tx Ty Ts + t0 Tr, 即Tx (Ts + t0 Tr) Ty Tx。也就是说，若能保证Ts + t0 TrtB就能有Tx tB Ty Tx。但Ts与Tr间并无约束关系，故无论tB定义为多大, Ts + t0 Tr都可能会大于它，即不会有Ts + t0 Tr tB成立。所以(PROT_AGENTB | (| iB AGENTi) |ftp| TTP ) |trans, rec| MEDIUM sat TIMELINESS2(B)不成立。综上所述，只要A能确保将sub_K发送给TTP后等待的时间长度tA大于网络不可用的最大时间长度t0，他就一定能检索到TTP发布的证据。然而，TIMELINESS2(B)中的时间约束无法得到满足，根源在于TTP发布证据的时间(即A提交sub_K的时间)与B发送EOR的时间间无任何约束关系，致使B等待的时间tB无论多长，A都可在它超时后向TTP发送sub_K，同时也能在TTP发布证据con_K之后及时检索到此证据，以便日后用于证明B获得了M。考虑到B会因为等待超时已将C删除，故即使其能检索到con_K也无法解密出M。所以，这就要求B在发送EOR后，若一直无法检索到con_K，其也不能删除EOO，从而无限期地维持协议轮状态。故Zhou-Gollmann协议无法保证对B公平，因而不具备时限性。4 Kim-Park-Baek协议的形式化分析第3节证明Zhou-Gollmann协议不具备时限性，特定情况下接收者必须永久保存未完成协议轮的相关证据，否则发送者能够获得所有证据，而接收者却无法获得相关的信息和证据。文献17曾通过向协议消息中加入时间限制信息的办法改进过该协议(新协议简称为Kim-Park-Baek协议)。协议中发送者和接收者都有能力限制相关协议信息的发送时间，所有超时后才被接收到的协议信息，都会被相关的协议实体视作无效信息。该文认为只要接收者规定了一个合适的时间限制，就能确保协议公平。交互步骤为：1) AB: fEOO , B, L, T, C, EOO2) BA: fEOR , A, L, T1, EOR3) ATTP: fSUB , B, L, T, K, sub_K4) BTTP: fCON , A, B, L, K, T0, con_K5) ATTP: fCON , A, B, L, K, T0, con_KEOO=sSA (fEOO , B, L, T, C);EOR=sSB (fEOR , A, L, T1, C);sub_K=sSA (fSUB , B, L, T, K);con_K=sST (fCON , A, B, L, T0, K);T是实体能从TTP处检索到con_K的最终期限；T0是TTP发布con_K的具体时间；T1是B规定A必须提交K给TTP的最迟时间；T, T1和T0间约束关系为T0T1T；协议执行后，A和B收集到的证据与原协议相同。类似于第3节，容易验证该协议具备不可否认性和公平性。下面重点验证其是否弥补了原协议固有的时限性缺陷。所需时间常元有t, t1, t0, tA和tB，其中t和t1分别为协议消息中相应的时间控制信息T和T1，约束关系为t1 t；t0, tA和tB同第3节；所需时间变元有Ts, Tr, To, TA, TB, Tx, Ty, TFA, TFB 。该协议的增广CSP模型与3.1节基本相同。此外还存在这样的事实：若A同意B规定的期限T1，其须在T1之前向TTP发送sub_K，否则将会在以后的纠纷中处于劣势(其一，J能验证出B持有的证据有效，其二，J会检测到A发送sub_K的具体时间与EOR中的T1不相符，从而认为A持有的证据无效)，即。事实：$i, ijiTTP, AGENTi (S) sat trans. i! TTP!( si (fSUB . j. l. t. k). Ts|x| xt1 in trX.A和B正确执行协议的增广CSP模型仍用PROT_AGENTA和PROT_AGENTB表示：PROT_AGENTA = trans. A! B! (sA (fEOO . B. L. T. C). To rec. A. B.( sB (fEOR . A. L. T1. C). Tr |x| To x trans. A! TTP!( sA (fSUB . B. L. T. K). Ts|x| Trxt1(源于事实) ftp. A. TTP. (sT (fCON . A. B. L. T0. K). TA |x| TsxTs + t0(应用引理2) FINISHEDA (sB (fEOR . A. L. T1. C), sT (fCON . A. B. L. T0. K) at TFA|x|TAx。PROT_AGENTB = rec. B? i? (si (fEOO . B. L. T. C). To trans. B! i! ( sB (fEOR . i. L. T1. C). Tr |x| To x ftp. B. TTP? (sT (fCON . i. B. L. T0. K). TB |x| TsxTs + t0 (应用引理2) FINISHEDB (si (fEOO. B. L. T. C), sT (fCON . i. B. L. T0. K) at TFB |x|TBx。时限性分析仍由2步完成。1) 协议认为若A收到了TTP发布的con_K, 它一定是在将sub_K提交给TTP之后和期限T之前收到的；即有规约TIMELINESS1(A) A sent M at Tx A received con_K at Ty |x| Tx x t . 下面通过分析(PROT_AGENTA | (| iA AGENTi) |ftp| TTP ) |trans, rec| MEDIUM sat TIMELINESS1(A) 是否成立来证明该协议能否保证对A公平。证明 重点检验Tyx| Tx x t 是否成立。根据PROT_AGENTA，令Tx = max(To, Ts)，Ty = TA。因TA x | Ts x Ts + t0, 所以Ts Ty Ts + t0。又因为To Tr Ts, 所以Tx Ty Ts + t0。所以，只要将Ts选定在Ts min(t1, tt0) 即可得Tx Ty t。2) 同样，若B 收到了TTP发布的con_K, 它一定是发送EOR之后和期限T之前收到的，且等待时间从T1开始；即有规约TIMELINESS2(B) B received M at Tx B sent EOR at Ty |x| xTx t1+tB t. 下面通过分析(PROT_AGENTB | (| iB AGENTi) |ftp| TTP ) |trans, rec| MEDIUM sat TIMELINESS2(B)是否成立来证明该协议能否保证对B公平。证明 仅验证时间约束部分Tyx| x Tx t1+tB t。根据PROT_AGENTB，令Tx = max(To, TB), Ty = Tr。待证Ty Tx t1 +tB t因为Tx = max(To, TB), 且To Tr Ts TB, 所以Tx = TB。又TB x | Ts x Ts + t0, 所以Ts Tx Ts + t0。再由Ty = Tr Ts得Ty Tx Ts + t0。最后由Ts t1, 有Ty Tx t1 + t0。因此只需要将时间常元的值定义为t0 tB t t1，即可得到Ty Tx t1+tB t。上述分析表明A总能保证在提交sub_K之后与TTP保存证据期限T之前的合适时机收取TTP发布的con_K。同时只要B在发送EOR时确保T1到T间的间隔足够大(大于t0)，其就可以只等待有限的时间(到期限T为止)便能检索到相应的证据。若T之后B还没收到con_K，其就可将EOO安全地删除，因此Kim-Park-Baek协议具有时限性。这也充分说明了文献17通过向协议消息中加入时间限制信息的办法的确弥补了原协议固有的时限性缺陷。5 进一步讨论5.1 方法的正确性新方法发现了Zhou-Gollmann协议存在一个许多其他方法无法发现的已知缺陷，而且还证明了向协议消息中加入时间限制信息可以弥补该缺陷，但这并不能保证该方法是合理的，仍然需要对其正确性进行分析。新方法对CSP所做的扩展主要为1) 向事件定义中加入时间信息以描述事件发生的具体时间，并给出协议分析的具体步骤；2) 基于秩函数理论，给出使用该方法建模协议事件之间约束关系的引理与推论；3) 提出基于初等代数与集合论来分析事件间时间约束关系。下面从3个角度逐个分析该方法的正确性。首先，分析新方法语义正确性。CSP将单个进程表示成事件组合或由诸如前缀、选择、并行等操作符作用后的进程组合。新方法只是将CSP所含语义在语法上进行了显式表达，每个增广CSP进程都可由相应的CSP进程构造，描述如下：1) Stop为死锁进程，因此n0，则有Stop=Stopf.2) 进程c. i. j. mP表示执行事件c后其行为表现为P，则必$ t0,t0ti,i1,2,n且t1t2tn，使得(cP) fnt1,t2,tn=c. i. j. m. t0Pft1,t2,tn.3) 依赖于环境初始事件集c. i. j. m，外部选择进程P1P2