摘  要： 綜合Kailar邏輯和SVO邏輯兩種協議分析方法的優點，借助SVO邏輯的思想對Kailar邏輯進行了改進，使其更好地應用于不可否認協議的可追究性分析和設計。同時，將改進后的Kailar邏輯應用在類NG協議的分析中，分析結果證明了該協議可追究方面的安全性質。
關鍵詞： 邏輯系統；Kailar邏輯；SVO邏輯；安全協議

　協議的安全性分析在安全協議的設計中起著重要的作用，Kailar邏輯的提出主要是針對電子商務協議的可追究性，但它不能分析簽名的密文，對協議的證明不嚴格。SVO邏輯也可用于電子商務協議的形式化分析，它集成了BAN、GNY、AT等邏輯的優點，具有很好的擴展能力。本文針對Kailar邏輯的不足，借助SVO邏輯的分析思想對Kailar邏輯進行了改進和完善，使得新的Kailar邏輯能分析簽名密文，嚴格推證協議是否具有不可否認性。
1 Kailar邏輯的基本架構
　Kailar邏輯的基本架構包含基本語句、分析假設和推理原則，限于篇幅，本文只對涉及的語句、推理原則進行說明，其他的不一一列舉。

　

　圖1中的符號含義為：A、B為協議參與雙方，TTP為可信第三方。L為協議輪標志。Na、Nb為新的隨機數。SA、SB為A、B的私鑰。SAT、SBT分別為A、T間共享密鑰，B、T間共享密鑰。Kx為A產生的消息密鑰。C=（m）Kx-1，m為發送的消息原語。此協議中A發送給B一個由Kx加密的消息C后通過第三方TTP傳遞Kx給B。此協議具有實現A、B、TTP間的消息可追究性的性質。
　（1）協議的前提和假設
　假設1：A Can prove（KB Authenticates B）；
　假設2：B Can prove（KA Authenticates A）；
　假設3：Shared（A，KAT，TTP）；
　假設4：Shared（B，KBT，TTP）；
　假設5：A Believe TTP；
　假設6：B Believe TTP。
　（2）說明協議目標
　G1：A Believe（B Received m）；
　G2：B Believe（A Sent m）；
　G3：TTP Believe（A Sent m）；
　G4：TTP Believe （B Received m）。
　（3）運用規則和公理進行推證協議理想化描述為：
　（M1）B Received（（B，L，Na，C）Signedwith KA-1）
　（M2）A Received（（A，L，Na+1，C）Signedwith KB-1）
　（M3）TTP Received（（Kx，C）Signedwith KAT）
　（M4）TTP Received（C Signedwith KBT）
　（M5）B Received（（Kx，Nb）Signedwith KBT）
　（M6）TTP Received（（Kx，Nb+1）Signedwith KBT）
　（4）協議分析
　①由協議描述（M2）知A Received（C Signedwith KB-1）（規則P14）。結合假設1可得結論1：A Can prove（B Says C）（規則P4）。由原則P1和P2可得結論2：A Can prove（B Sent C）。再結合已知 A Sent（Na∧C）和A Received（Na’∧C），根據原則P10可得結論3：A Can prove（B Received C）。其中，C=（m）Kx-1，即有結論4：A Can prove（B Received m Sighned with Kx-1） 。
　由協議描述（M6）知TTP Received（（Kx）Signedwith KBT）（規則P14），而由假設4，基于原則P6有結論5：TTP Can prove（B Says Kx），根據原則P1和P2有結論6：TTP Can prove（A Sent Kx）。由結論6結合已知TTP Sent（Nb∧Kx）和TTP Received（Nb’∧Kx），運用原則10可得出結論7：TTP Can prove（B Received Kx），結合假設5和結論7，運用原則P6可得結論8：A Can prove（B Received Kx）。結合結論4，應用原則P8可推出結論9：A Can prove（B Received m），進而應用原則P13可得結論10：A Believe（B Received m），此結論即為要達成的協議目標G1。
　②由協議描述（M1）基于規則P14知B Received （C Signedwith KA-1），而由假設2，運用原則P4可得結論11：B Can prove（A says C），進一步運用原則P1和P2可得結論12：B Can prove（A Sent C），而C=（m） Kx-1，即有結論13：B Can prove（A Sent m Sighned with Kx-1）。
由描述（M3）知TTP Received（Kx Signedwith KAT），結合假設3和規則P4有結論14：TTP Can prove（A Says Kx），進一步結合假設6，應用規則P5有結論15：B Can prove（A Says Kx）。而結論11為B Can prove（A says C），即B Can prove（A Says m Sighned with Kx-1），應用原則P9可得結論16：B Can prove（A Says m）。進一步根據原則P1和P2有結論17：B Can prove（A Sent m），再根據原則P12可得結論18：B Believe（A Sent m）。該結論即為要達成的協議目標G2。
　③基本推理規則P14，由協議描述（M3）知TTP Received（C Signedwith KAT），結合假設3和規則P7有結論19：TTP Can prove（A Says C），而已有結論14為TTP Can prove（A Says Kx），已知C=（m）Kx-1，故由P9可得結論20：TTP Can prove（A Says m），進一步應用P1和P2原則有結論21：TTP Can prove（A Sent m），  再基于原則P12可得結論22：TTP Believe（A Sent m）。結論22即為要達成的目標G3。
　④由協議描述（M4）、假設4、結論19和原則P11可得結論23：TTP Can prove（B Received C），結合已知C=（m）Kx-1和結論7，基于原則P8可得結論24：TTP Can prove（B Received m），進一步基于基本推理原則P13得出結論25：TTP Believe（B Received m），結論25即為要達成的目標G4。
　由上述分析可知，該協議的4個目標都可滿足，協議的各方的信任都可以建立，具有不可否認的性質，協議具有追究性。
　基于推理結構性方法體系通常由一些命題和推理公理組成，命題表示了主體對消息的信仰或知識，運用推理公理可以從已知的知識和信仰推導出新的知識和信仰。其中，Kailar邏輯和SVO邏輯是最重要的兩種方法，各具優點和不足。針對Kailar邏輯的不足，本文借助SVO邏輯的思想對其進行了改進和完善，使得它能更好地應用于協議的不可否認性和可追究性的分析。將擴展了的Kailar邏輯應用于類NG協議的可追究性的分析，證明了該協議可追究方面的安全性質。該協議分析方法簡單、語義明確，為電子商務類協議的分析提供了強有力的工具。但是還有一些需要改進的地方，例如如何應用它來分析協議的公平性，如何引入恰當的初始化假設等。
參考文獻
[1] 范紅，馮登國.安全協議形式化分析的研究現狀與有關問題[J].網絡安全技術與應用，2001（8）：12-15.
[2] KAILAR  R. Accountabitity in electronic commerce protocols[J]. IEEE Transactions on Software Engineering， 1996，22（5）：313-328.
[3] ZHEN J， GOLLMANN D. A fair non-repudiation protocol[J]. IEEE Computer Society Symposium on Research in Security and Privacy，1996.
[4] 范紅，馮登國.安全協議理論與方法[M].北京：科學出版社，2003.
[5] ZHOU J， GOLLMAN D. A fair non-repudiation protocol[C].Proceeding of 1996 IEEE Symposium on Security and Privacy， 1996：55-61.
[6] 周典萃，卿斯漢，周展飛.Kailar ：邏輯的缺陷[J].軟件學報，1999，10（12）：1238-1245.
[7] 卿斯漢，常曉林，章江.安全電子商務協議iKP I的設計和實現[C].信息和通信安全——CC ICS’99：第一屆中國信息和通信安全學術會議，2000.230-239.
[8] ISO/IEC 1388822， Information technology security techniques non-repudiation part2： mechanisms using symmetrical techniques[S]. International Organization for Standardization， 1998.