Kailar邏輯的改進及應用*

翁艷琴 ，石曙東 ，解顏銘

（1.湖北師范學院 數學與統計學院，湖北 黃石 435000；2.湖北師范學院 計算機科學與技術學院，湖北 黃石 435000）

協議的安全性分析在安全協議的設計中起著重要的作用，Kailar邏輯的提出主要是針對電子商務協議的可追究性，但它不能分析簽名的密文，對協議的證明不嚴格。SVO邏輯也可用于電子商務協議的形式化分析，它集成了BAN、GNY、AT等邏輯的優點，具有很好的擴展能力。本文針對Kailar邏輯的不足，借助SVO邏輯的分析思想對Kailar邏輯進行了改進和完善，使得新的Kailar邏輯能分析簽名密文，嚴格推證協議是否具有不可否認性。

1 Kailar邏輯的基本架構

Kailar邏輯的基本架構包含基本語句、分析假設和推理原則，限于篇幅，本文只對涉及的語句、推理原則進行說明，其他的不一一列舉。

（1）基本語句A，B，C……為參與協議的主體，通常用P指代。TTP專指可信的第三方。m為一個主體給另一個主體發送的原子消息。C為原子消息外的消息。Ki為主體i的公開密鑰。Ki-1為與Ki對應的秘密私鑰。x，y……為命題。

（2）基本推理原則為以下3個：

2 可追究原則的改進

本文假定發送者為A，接收者為B，可信第三方為TTP，其他符號含義同上。在Kailar邏輯中，只是涉及了接收方對發送方的主體簽名的追究性，沒有涉及發送方對接收方的簽名的追究性，同時對第三方TTP對參與協議的其他方的追究性也沒有明確的推理規則。本文借助SVO邏輯的思想，對Kailar邏輯進行了完善，改進后的推理原則如下：

（1）發送方的簽名追究性

（2）接收方的簽名追究性兩方間：

三方間：

3 應用Kailar邏輯進行協議分析

不可否認協議（類NG協議）的交互過程如圖1所示。

圖1 類NG協議交互圖

圖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（KBAuthenticates B）；

假設 2：B Can prove（KAAuthenticates A）；

假設 3：Shared（A，KAT，TTP）；

假設 4：Shared（B，KBT，TTP）；

假設 5：A Believe TTP；

假設 6：B Believe TTP。

（2）說明協議目標

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 SaysC）（規則 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（KxSignedwith 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 of1996 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.