摘  要： 綜合Kailar邏輯和SVO邏輯兩種協(xié)議分析方法的優(yōu)點(diǎn)，借助SVO邏輯的思想對(duì)Kailar邏輯進(jìn)行了改進(jìn)，使其更好地應(yīng)用于不可否認(rèn)協(xié)議的可追究性分析和設(shè)計(jì)。同時(shí)，將改進(jìn)后的Kailar邏輯應(yīng)用在類NG協(xié)議的分析中，分析結(jié)果證明了該協(xié)議可追究方面的安全性質(zhì)。
關(guān)鍵詞： 邏輯系統(tǒng)；Kailar邏輯；SVO邏輯；安全協(xié)議

　協(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中的符號(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ì)。
?。?）協(xié)議的前提和假設(shè)
　假設(shè)1：A Can prove（KB Authenticates B）；
　假設(shè)2：B Can prove（KA Authenticates A）；
　假設(shè)3：Shared（A，KAT，TTP）；
　假設(shè)4：Shared（B，KBT，TTP）；
　假設(shè)5：A Believe TTP；
　假設(shè)6：B Believe TTP。
?。?）說(shuō)明協(xié)議目標(biāo)
　G1：A Believe（B Received m）；
　G2：B Believe（A Sent m）；
　G3：TTP Believe（A Sent m）；
　G4：TTP Believe （B Received m）。
?。?）運(yùn)用規(guī)則和公理進(jìn)行推證協(xié)議理想化描述為：
?。∕1）B Received（（B，L，Na，C）Signedwith KA-1）
?。∕2）A Received（（A，L，Na+1，C）Signedwith KB-1）
?。∕3）TTP Received（（Kx，C）Signedwith KAT）
?。∕4）TTP Received（C Signedwith KBT）
?。∕5）B Received（（Kx，Nb）Signedwith KBT）
?。∕6）TTP Received（（Kx，Nb+1）Signedwith KBT）
?。?）協(xié)議分析
?、儆蓞f(xié)議描述（M2）知A Received（C Signedwith KB-1）（規(guī)則P14）。結(jié)合假設(shè)1可得結(jié)論1：A Can prove（B Says C）（規(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。
?、谟蓞f(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（Kx Signedwith 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。
?、苡蓞f(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è)等。
參考文獻(xiàn)
[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 of 1996 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.