Kailar邏輯的改進(jìn)及應(yīng)用*

翁艷琴 ，石曙東 ，解顏銘

（1.湖北師范學(xué)院 數(shù)學(xué)與統(tǒng)計(jì)學(xué)院，湖北 黃石 435000；2.湖北師范學(xué)院 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，湖北 黃石 435000）

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

1 Kailar邏輯的基本架構(gòu)

Kailar邏輯的基本架構(gòu)包含基本語(yǔ)句、分析假設(shè)和推理原則，限于篇幅，本文只對(duì)涉及的語(yǔ)句、推理原則進(jìn)行說(shuō)明，其他的不一一列舉。

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

（2）基本推理原則為以下3個(gè)：

2 可追究原則的改進(jìn)

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

（1）發(fā)送方的簽名追究性

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

三方間：

3 應(yīng)用Kailar邏輯進(jìn)行協(xié)議分析

不可否認(rèn)協(xié)議（類NG協(xié)議）的交互過(guò)程如圖1所示。

圖1 類NG協(xié)議交互圖

圖1中的符號(hào)含義為：A、B為協(xié)議參與雙方，TTP為可信第三方。L為協(xié)議輪標(biāo)志。Na、Nb為新的隨機(jī)數(shù)。SA、SB為 A、B 的私鑰。 SAT、SBT分別為 A、T間共享密鑰，B、T間共享密鑰。Kx為 A產(chǎn)生的消息密鑰。C=（m）Kx-1，m為發(fā)送的消息原語(yǔ)。此協(xié)議中A發(fā)送給B一個(gè)由Kx加密的消息C后通過(guò)第三方TTP傳遞Kx給B。此協(xié)議具有實(shí)現(xiàn)A、B、TTP間的消息可追究性的性質(zhì)。

（1）協(xié)議的前提和假設(shè)

假設(shè) 1：A Can prove（KBAuthenticates B）；

假設(shè) 2：B Can prove（KAAuthenticates A）；

假設(shè) 3：Shared（A，KAT，TTP）；

假設(shè) 4：Shared（B，KBT，TTP）；

假設(shè) 5：A Believe TTP；

假設(shè) 6：B Believe TTP。

（2）說(shuō)明協(xié)議目標(biāo)

G2：B Believe（A Sent m）；

G3：TTP Believe（A Sent m）；

G4：TTP Believe （B Received m）。

（3）運(yùn)用規(guī)則和公理進(jìn)行推證協(xié)議理想化描述為：

（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）協(xié)議分析

①由協(xié)議描述（M2）知 A Received（C Signedwith KB-1）（規(guī)則 P14）。結(jié)合假設(shè) 1可得結(jié)論 1：A Can prove（B SaysC）（規(guī)則 P4）。 由原則 P1和 P2可 得 結(jié)論 2：A Can prove（B Sent C）。 再結(jié)合已知 A Sent（Na∧C）和A Received（Na’∧C），根據(jù)原則 P10 可得結(jié)論 3：A Can prove（B Received C）。其中，C=（m）Kx-1，即有結(jié)論 4：A Can prove（B Received m Sighned with Kx-1）。

由協(xié)議描述 （M6）知 TTP Received（（Kx）Signedwith KBT）（規(guī)則 P14）， 而由假設(shè) 4， 基于原則 P6有結(jié)論 5：TTP Can prove（B Says Kx），根據(jù)原則 P1 和 P2 有結(jié)論6：TTP Can prove（A Sent Kx）。 由結(jié)論 6 結(jié)合已知 TTP Sent（Nb∧Kx）和 TTP Received（Nb’∧Kx），運(yùn) 用 原 則 10可得出結(jié)論 7：TTP Can prove（B Received Kx），結(jié)合假設(shè) 5和結(jié)論 7，運(yùn)用原則 P6可得結(jié)論 8：A Can prove（B Received Kx）。結(jié)合結(jié)論 4，應(yīng)用原則 P8可推出結(jié)論 9：A Can prove（B Received m），進(jìn)而應(yīng)用原則P13可得結(jié)論 10：A Believe（B Received m），此結(jié)論即為要達(dá)成的協(xié)議目標(biāo)G1。

②由協(xié)議描述 （M1）基于規(guī)則 P14知 B Received（C Signedwith KA-1），而由假設(shè) 2，運(yùn)用原則 P4可得結(jié)論 11：B Can prove（A says C），進(jìn)一步運(yùn)用原則 P1 和P2 可得結(jié)論12：B Can prove （A Sent C）， 而 C=（m）Kx-1，即有結(jié)論 13：B Can prove（A Sent m Sighned with Kx-1）。

由 描 述 （M3）知 TTP Received（KxSignedwith KAT），結(jié)合假設(shè) 3和規(guī) 則 P4有結(jié)論 14：TTP Can prove（A Says Kx），進(jìn)一步結(jié)合假設(shè) 6，應(yīng)用規(guī)則 P5有結(jié)論 15：B Can prove（A Says Kx）。 而結(jié)論 11 為 B Can prove（A says C），即 B Can prove （A Says m Sighned with Kx-1），應(yīng)用原則 P9可得結(jié)論 16：B Can prove（A Says m）。進(jìn)一步根據(jù)原則 P1和 P2有結(jié)論 17：B Can prove（A Sent m）， 再根據(jù)原則 P12可得結(jié)論 18：B Believe（A Sent m）。該結(jié)論即為要達(dá)成的協(xié)議目標(biāo)G2。

③基本推理規(guī)則 P14，由協(xié)議描述 （M3）知 TTP Received（C Signedwith KAT），結(jié)合假設(shè) 3和規(guī)則 P7有結(jié)論 19：TTP Can prove（A Says C）， 而已有結(jié)論 14為TTP Can prove（A Says Kx），已 知 C=（m）Kx-1，故 由 P9可得結(jié)論 20：TTP Can prove（A Says m），進(jìn)一步應(yīng)用P1和 P2原則有結(jié)論 21：TTP Can prove （A Sent m），再基于原則 P12可得結(jié)論 22：TTP Believe（A Sent m）。結(jié)論22即為要達(dá)成的目標(biāo)G3。

④由協(xié)議描述（M4）、假設(shè) 4、結(jié)論 19和原則 P11可得結(jié)論 23：TTP Can prove（B Received C），結(jié)合已知C=（m）Kx-1和結(jié)論 7， 基于原則 P8可得結(jié)論 24：TTP Can prove（B Received m），進(jìn)一步基于基本推理原則P13 得出結(jié)論 25：TTP Believe（B Received m），結(jié)論 25即為要達(dá)成的目標(biāo)G4。

由上述分析可知，該協(xié)議的4個(gè)目標(biāo)都可滿足，協(xié)議的各方的信任都可以建立，具有不可否認(rèn)的性質(zhì)，協(xié)議具有追究性。

基于推理結(jié)構(gòu)性方法體系通常由一些命題和推理公理組成，命題表示了主體對(duì)消息的信仰或知識(shí)，運(yùn)用推理公理可以從已知的知識(shí)和信仰推導(dǎo)出新的知識(shí)和信仰。其中，Kailar邏輯和SVO邏輯是最重要的兩種方法，各具優(yōu)點(diǎn)和不足。針對(duì)Kailar邏輯的不足，本文借助SVO邏輯的思想對(duì)其進(jìn)行了改進(jìn)和完善，使得它能更好地應(yīng)用于協(xié)議的不可否認(rèn)性和可追究性的分析。將擴(kuò)展了的Kailar邏輯應(yīng)用于類NG協(xié)議的可追究性的分析，證明了該協(xié)議可追究方面的安全性質(zhì)。該協(xié)議分析方法簡(jiǎn)單、語(yǔ)義明確，為電子商務(wù)類協(xié)議的分析提供了強(qiáng)有力的工具。但是還有一些需要改進(jìn)的地方，例如如何應(yīng)用它來(lái)分析協(xié)議的公平性，如何引入恰當(dāng)?shù)某跏蓟僭O(shè)等。

[1]范紅，馮登國(guó).安全協(xié)議形式化分析的研究現(xiàn)狀與有關(guān)問(wèn)題[J].網(wǎng)絡(luò)安全技術(shù)與應(yīng)用，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]范紅，馮登國(guó).安全協(xié)議理論與方法[M].北京：科學(xué)出版社，2003.

[5]ZHOU J，GOLLMAN D.A fair non-repudiation protocol[C].Proceeding of1996 IEEE Symposium on Security and Privacy， 1996：55-61.

[6]周典萃，卿斯?jié)h，周展飛.Kailar：邏輯的缺陷[J].軟件學(xué)報(bào)，1999，10（12）：1238-1245.

[7]卿斯?jié)h，常曉林，章江.安全電子商務(wù)協(xié)議 iKP I的設(shè)計(jì)和實(shí)現(xiàn)[C].信息和通信安全——CC ICS’99：第一屆中國(guó)信息和通信安全學(xué)術(shù)會(huì)議，2000.230-239.

[8]ISO/IEC 1388822，Information technology security techniques non-repudiation part2： mechanisms using symmetrical techniques[S].International Organization for Standardization，1998.