不可否認(rèn)協(xié)議分析的擴(kuò)展ZQZ 邏輯方法*

韓志耕, 石青山, 楊 鵬, 陳 耿, 范遠(yuǎn)哲

1. 南京審計(jì)大學(xué) 信息工程學(xué)院, 南京 211815

2. 江蘇省審計(jì)信息工程重點(diǎn)實(shí)驗(yàn)室(南京審計(jì)大學(xué)), 南京 211815

1 引言

2020 年受新冠疫情“黑天鵝” 事件的影響, 人們的工作方式和生活習(xí)慣悄然發(fā)生了改變, 在線(xiàn)辦公、在線(xiàn)購(gòu)物、在線(xiàn)教育和在線(xiàn)醫(yī)療等需求顯著增加. 伴隨著線(xiàn)下活動(dòng)大規(guī)模向線(xiàn)上遷移, 網(wǎng)絡(luò)欺詐也隨之泛濫[1]. 據(jù)360 獵網(wǎng)平臺(tái)統(tǒng)計(jì)數(shù)據(jù)顯示, 疫情期間共收到網(wǎng)絡(luò)欺詐舉報(bào)3243 例, 比上一年同期增長(zhǎng)了47%.網(wǎng)絡(luò)欺詐在特征上表現(xiàn)為網(wǎng)絡(luò)行為真實(shí), 而網(wǎng)絡(luò)主體不誠(chéng)實(shí), 對(duì)其進(jìn)行取證需要借助不可否認(rèn)服務(wù)進(jìn)行.該類(lèi)服務(wù)通過(guò)生成、交換和管理一系列與網(wǎng)絡(luò)行為有關(guān)的密碼學(xué)證據(jù), 為溯源網(wǎng)絡(luò)欺詐提供依據(jù), 在物聯(lián)網(wǎng)安全[2]、合同簽名[3]、簽收郵件[4,5]等領(lǐng)域應(yīng)用廣泛. 不可否認(rèn)服務(wù)的實(shí)現(xiàn)依賴(lài)于不可否認(rèn)協(xié)議. 不可否認(rèn)協(xié)議邏輯復(fù)雜, 細(xì)小的邏輯缺陷都會(huì)導(dǎo)致不可否認(rèn)服務(wù)失效, 使得相應(yīng)的網(wǎng)絡(luò)欺詐無(wú)法溯源.

邏輯正確的不可否認(rèn)協(xié)議通常需要滿(mǎn)足存活性、不可否認(rèn)性、公平性和時(shí)限性[6,7]. 形式化分析是驗(yàn)證該類(lèi)協(xié)議邏輯是否正確的常用手段. 以ZG 協(xié)議[8]為例, 為驗(yàn)證其邏輯是否正確: (1) 在邏輯推理方面,Zhou 等人使用SVO 邏輯分析過(guò)其不可否認(rèn)性[9]; 黎波濤等人使用改進(jìn)的SVO 邏輯分析過(guò)其時(shí)限性[10];基于改進(jìn)的SVO 邏輯, 韓志耕等人分析過(guò)該協(xié)議多方多消息變體的不可否認(rèn)性、公平性和時(shí)限性[11,12];苑博奧等人分析過(guò)多方單消息變體[13]和帶區(qū)塊鏈的多方單消息變體[14]的不可否認(rèn)性、公平性和時(shí)限性; 周典萃等人使用類(lèi)Kailar 邏輯(簡(jiǎn)稱(chēng)ZQZ 邏輯) 分析過(guò)ZG 協(xié)議的不可否認(rèn)性和公平性[15]; Liu等人使用改進(jìn)的ZQZ 邏輯分析過(guò)ZG 協(xié)議及其變體的不可否認(rèn)性、公平性和時(shí)限性[16]. (2) 在模型檢測(cè)方面, 黎波濤等人使用有色Petri 網(wǎng)分析過(guò)其公平性[17]; Kremer 等人[18]首次利用基于博弈論的交替轉(zhuǎn)換邏輯ATL 和模型檢測(cè)工具M(jìn)OCHA 分析過(guò)該協(xié)議多方單消息樂(lè)觀變體的公平性; 文靜華等人使用ATL 和MOCHA 分析過(guò)該協(xié)議及其兩方樂(lè)觀變體的保密性、不可否認(rèn)性、公平性及時(shí)限性[19,20]; 汪學(xué)明等人[21]使用MOCHA 分析過(guò)該協(xié)議多方單消息變體的不可否認(rèn)性和抗合謀性. (3) 在定理證明方面, 沈海峰等人利用串空間結(jié)點(diǎn)標(biāo)號(hào)的遞歸公平交換協(xié)議分析方法分析過(guò)該協(xié)議的公平性[22]; 王濤等人利用擴(kuò)展的串空間模型分析過(guò)其樂(lè)觀變體的公平性[23]; Li 等人利用串空間模型分析過(guò)其多方單消息變體的公平性[24]; 姚萌萌等人利用擴(kuò)展的串空間理論分析過(guò)該協(xié)議基于區(qū)塊鏈的多方變體的不可否認(rèn)性、公平性和時(shí)限性[25]; Bella 等人使用Paulson 歸納法分析過(guò)該協(xié)議的不可否認(rèn)性[26]. (4) 在進(jìn)程代數(shù)方面,Schneider 利用CSP 分析過(guò)該協(xié)議的不可否認(rèn)性和公平性[27]; 韓志耕等人利用增廣CSP 分析過(guò)該協(xié)議[28]及其多方單消息變體[29]的不可否認(rèn)性、公平性和時(shí)限性; 李援等人利用擴(kuò)展SPI 演算分析過(guò)其不可否認(rèn)性[30].

邏輯推理類(lèi)方法抽象程度高, 但描述能力弱; 模型檢測(cè)類(lèi)方法容易出現(xiàn)狀態(tài)爆炸, 在主體數(shù)量加大時(shí)會(huì)因狀態(tài)過(guò)多而造成無(wú)法分析; 定理證明類(lèi)方法可以證明協(xié)議邏輯的正確性, 但對(duì)不能完成證明的協(xié)議無(wú)法指出其存在的安全缺陷, 對(duì)協(xié)議設(shè)計(jì)的指導(dǎo)能力有限; 進(jìn)程代數(shù)類(lèi)方法對(duì)發(fā)現(xiàn)協(xié)議攻擊非常有效, 但不可否認(rèn)側(cè)重于防范實(shí)體欺詐而非網(wǎng)絡(luò)攻擊. 這四類(lèi)方法各有優(yōu)勢(shì), 但共同點(diǎn)是它們中的絕大多數(shù)方法僅能對(duì)不可否認(rèn)協(xié)議的部分性質(zhì)進(jìn)行建模與分析、證明或證偽協(xié)議邏輯的局部正確性. 以ZQZ 邏輯[15]為例,該方法雖然目前被關(guān)注較少, 但其具備的無(wú)狀態(tài)爆炸、支持密文處理、初始假設(shè)形式化, 尤其是其所基于的面向責(zé)任分析與不可否認(rèn)協(xié)議所側(cè)重的欺詐溯源高度契合, 使其應(yīng)用于不可否認(rèn)協(xié)議的分析前景廣闊.該邏輯的不足是時(shí)間描述能力弱, 無(wú)法分析協(xié)議的時(shí)限性. 鑒于當(dāng)前趨勢(shì)是綜合利用多種手段, 取長(zhǎng)補(bǔ)短,以期發(fā)現(xiàn)更多的協(xié)議缺陷, 達(dá)到更好的分析效果. 借助于時(shí)間表達(dá)式可以描述協(xié)議事件的發(fā)生時(shí)間、刻畫(huà)事件間的時(shí)序關(guān)系, 已被廣泛應(yīng)用于協(xié)議時(shí)限性建模與分析[10,12,14,28]的事實(shí), 本文通過(guò)向ZQZ 邏輯添加時(shí)間表達(dá)式, 提出了一種適用于不可否認(rèn)協(xié)議建模與分析的擴(kuò)展ZQZ 邏輯方法. 與Liu 等人[16]的工作不同, 擴(kuò)展ZQZ 邏輯方法在建模與分析時(shí)將協(xié)議性質(zhì)按照是否與時(shí)間相關(guān)做了區(qū)別對(duì)待, 僅在分析時(shí)間相關(guān)的性質(zhì)(如時(shí)限性) 時(shí)才涉及到對(duì)事件發(fā)生時(shí)間及約束關(guān)系的處理, 極大降低了協(xié)議分析的復(fù)雜度.

本文主要貢獻(xiàn)在于:

(1) 給出了擴(kuò)展ZQZ 邏輯方法框架, 包括推理規(guī)則和安全性質(zhì)模型. 與原邏輯相比, 擴(kuò)展后的邏輯除了增加時(shí)限性分析功能外, 還提高了對(duì)密文信息的處理能力.

(2) 以ZG 和KPB 這兩個(gè)局部邏輯正確性已知的不可否認(rèn)協(xié)議為實(shí)驗(yàn)對(duì)象, 系統(tǒng)性地介紹了使用擴(kuò)展ZQZ 邏輯對(duì)不可否認(rèn)協(xié)議的分析步驟, 通過(guò)實(shí)驗(yàn)結(jié)果與既有事實(shí)的符合性, 從逆向工程角度驗(yàn)證了該方法的功能有效性.

(3) 利用該方法對(duì)YLL 這個(gè)邏輯正確性尚在討論的、基于區(qū)塊鏈的公平多方不可否認(rèn)協(xié)議進(jìn)行探索性分析, 發(fā)現(xiàn)其存在一個(gè)尚未公開(kāi)的時(shí)限性異常, 并給出了對(duì)應(yīng)的協(xié)議改進(jìn)方案.

(4) 將擴(kuò)展ZQZ 邏輯方法與另外12 種常用的不可否認(rèn)協(xié)議分析方法從理論基礎(chǔ)、性質(zhì)分析、狀態(tài)爆炸、自動(dòng)化程度、抽象程度、密文處理這6 個(gè)維度作了功能比較.

論文其余部分組織如下: 第2 節(jié)給出了擴(kuò)展ZQZ 邏輯方法; 第3 節(jié)和第4 節(jié)利用該邏輯分別對(duì)ZG 和KPB 進(jìn)行了建模與分析, 以逆向驗(yàn)證新邏輯的功能有效性; 第5 節(jié)利用該邏輯對(duì)YLL 協(xié)議的時(shí)限性邏輯進(jìn)行了探索分析, 發(fā)現(xiàn)該協(xié)議存在一個(gè)尚未公開(kāi)的時(shí)限性異常; 第6 節(jié)將擴(kuò)展ZQZ 邏輯與現(xiàn)有常用的分析方法進(jìn)行了比較; 最后第7 節(jié)總結(jié)全文.

2 擴(kuò)展ZQZ 邏輯

2.1 ZQZ 邏輯介紹

ZQZ 邏輯是周典萃等人[15]提出的一種用于分析電子商務(wù)協(xié)議的新工具, 其目的是解決Kailar 邏輯在電子商務(wù)協(xié)議分析方面的能力不足. 電子商務(wù)協(xié)議必須遵循可追究性(迫使交易雙方對(duì)自己的行為負(fù)責(zé)) 和公平性(保證電子貨物獲取的對(duì)等性), 而Kailar 邏輯只能分析電子商務(wù)協(xié)議的可追究性, 其缺陷[31]包括: (1) 不能分析協(xié)議的公平性; (2) 列舉初始化假設(shè)是非形式化的, 假設(shè)的不當(dāng)會(huì)導(dǎo)致協(xié)議分析的失敗; (3) 無(wú)法理解包含簽過(guò)名的密文的協(xié)議語(yǔ)句. ZQZ 邏輯本質(zhì)上是一種類(lèi)Kailar 邏輯, 它使用擁有集合來(lái)記錄協(xié)議實(shí)體的信息狀態(tài), 使用推理規(guī)則來(lái)推演協(xié)議事件間的關(guān)聯(lián). 每個(gè)主體在協(xié)議運(yùn)行前擁有一個(gè)初始擁有集合, 之后該集合隨著協(xié)議語(yǔ)句的執(zhí)行不斷更新, 在協(xié)議運(yùn)行結(jié)束時(shí)每個(gè)主體將擁有最終擁有集合. 該邏輯方法通過(guò)判斷發(fā)方不可否認(rèn)證據(jù)(proof-of-origin, POO) 是否屬于收方最終擁有集合來(lái)驗(yàn)證協(xié)議是否滿(mǎn)足發(fā)方可追究性、通過(guò)判斷收方不可否認(rèn)證據(jù)(proof-of-receipt, POR) 是否屬于發(fā)方最終擁有集合來(lái)驗(yàn)證協(xié)議是否滿(mǎn)足收方可追究性; 通過(guò)驗(yàn)證協(xié)議的執(zhí)行在任何一步異常終止時(shí), POO 屬于收方的擁有集合是否當(dāng)且僅當(dāng)POR 屬于發(fā)方的擁有集合來(lái)驗(yàn)證協(xié)議的公平性; 通過(guò)增加密文理解規(guī)則, 來(lái)分析包含簽過(guò)名的加密公式的消息; 此外, 初始擁有集合的設(shè)置僅依賴(lài)環(huán)境而非人為引入的初始化假設(shè), 避免了假設(shè)不當(dāng)造成的協(xié)議分析失敗.

不可否認(rèn)協(xié)議對(duì)時(shí)間敏感, ZQZ 邏輯無(wú)法描述協(xié)議事件的發(fā)生時(shí)間, 無(wú)法刻畫(huà)協(xié)議事件間的時(shí)序關(guān)系. 下面對(duì)ZQZ 邏輯進(jìn)行擴(kuò)展, 以使其能夠分析不可否認(rèn)協(xié)議更多的性質(zhì).

2.2 標(biāo)識(shí)及其含義

2.3 擁有集合更新

擴(kuò)展ZQZ 邏輯仍采用原邏輯的擁有集合, 簡(jiǎn)介如下:

主體P的擁有集合是協(xié)議環(huán)境賦予P的信息、能證明的公式, 以及獲得的信息集合. 協(xié)議運(yùn)行前P的初始擁有集合記為O0P, 協(xié)議執(zhí)行后P的擁有集合OP=OnP, 其中n為協(xié)議步數(shù).OiP的更新策略為:

2.4 推理規(guī)則擴(kuò)展

在介紹擴(kuò)展ZQZ 邏輯的推理規(guī)則之前, 首先給出本文所使用的時(shí)間表達(dá)式.

定義1 (時(shí)間常元) 設(shè)Integer={0,1,2,···}∪{-1,-2,···},v是時(shí)間常元, 當(dāng)v ∈Integer.

定義2 (時(shí)間變?cè)?V是時(shí)間變?cè)? 當(dāng)V是一個(gè)變域?yàn)镮nteger 的變?cè)?

定義3 (時(shí)間綁定表達(dá)式)V|TB 是時(shí)間綁定表達(dá)式, 當(dāng)V是時(shí)間變?cè)襎B?Integer.

定義4 (時(shí)間表達(dá)式) [T] 是時(shí)間表達(dá)式, 當(dāng)T是時(shí)間綁定表達(dá)式.

規(guī)則R1 (1) 是對(duì)原ZQZ 邏輯簽名規(guī)則的時(shí)間拓展, 規(guī)則R1(2) 是新引入的簽名規(guī)則.

R2. 分解與合并規(guī)則

(1) 負(fù)責(zé)分解與合并規(guī)則: 若P證明Q在T時(shí)間對(duì)公式(x1,x2,··· ,xn) 或公式xi負(fù)責(zé), 則可證明Q在T時(shí)間對(duì)公式xi或公式(x1,x2,··· ,xn) 負(fù)責(zé). 即:

(2) 擁有分解與合并規(guī)則: 若P證明Q在T時(shí)間擁有公式(x1,x2,··· ,xn) 或公式xi, 則其能證明Q在T時(shí)間擁有公式xi或公式(x1,x2,··· ,xn). 即:

規(guī)則R2(1) 是對(duì)原ZQZ 邏輯連接規(guī)則的改進(jìn)與時(shí)間拓展, 規(guī)則R2(2) 是新引入的規(guī)則.

R3. 密文理解規(guī)則

(1) 加密規(guī)則: 若P證明在T時(shí)間Q對(duì){x}K負(fù)責(zé), 且證明Q擁有對(duì)稱(chēng)密鑰K, 則其能證明Q在T時(shí)間對(duì)x負(fù)責(zé). 即:

(2) 解密規(guī)則: 若P證明Q在Tx時(shí)間擁有密文{x}K, 且證明Q在Ty時(shí)間擁有對(duì)稱(chēng)密鑰K, 則其能證明Q在max(Tx,Ty) 時(shí)間擁有x. 即:

(3) 隱私規(guī)則: 若P證明Q在T時(shí)間擁有公鑰KQ加密形成的密文{x}KQ, 且證明KQ能驗(yàn)證Q身份, 則其能證明Q在T時(shí)間擁有x. 即:

規(guī)則R3(1) 是對(duì)原ZQZ 邏輯密文理解規(guī)則的時(shí)間擴(kuò)展, 規(guī)則R3(2) 和R3(3) 是新引入的密文理解規(guī)則.

R4. 擁有規(guī)則

這是對(duì)原ZQZ 邏輯擁有規(guī)則的改進(jìn). 若P擁有集合OiP中包含公式x, 那么Q能證明P擁有該x.即:

R5. 傳遞規(guī)則

這是對(duì)原ZQZ 邏輯傳遞規(guī)則的改進(jìn)與時(shí)間拓展. 令TTP 向P和Q共享消息x, 若P能夠證明TTP 在時(shí)間T對(duì)x負(fù)責(zé), 那么它能夠分別證明P在后繼時(shí)間Tx、Q在后繼時(shí)間Ty也必定擁有x. 即:

R6. 證書(shū)規(guī)則

這是對(duì)原電子證書(shū)規(guī)則的時(shí)間拓展. 若P能夠證明電子證書(shū)機(jī)構(gòu)CA 在時(shí)間T對(duì)公式(KQ,Q) 負(fù)責(zé), 那么P能夠證明在后續(xù)時(shí)間Tx可用KQ驗(yàn)證主體Q的身份(其中Trev為證書(shū)撤銷(xiāo)時(shí)間). 即:

2.5 安全性質(zhì)建模

擴(kuò)展ZQZ 邏輯將存活性、不可否認(rèn)性、公平性視為時(shí)間不相關(guān)性質(zhì), 將時(shí)限性視為時(shí)間相關(guān)性質(zhì). 前者在描述時(shí)無(wú)需引入時(shí)間信息.

令A(yù)是發(fā)方,B是收方,J是仲裁方, POO、POR 和M是數(shù)據(jù), Pr 是密碼協(xié)議,R是Pr 的一次成功運(yùn)行實(shí)例.

定義5 (存活性) Pr 滿(mǎn)足存活性, 若存在一個(gè)R有: (1)R之前:A持有M但不持有POR,B不持有POO 和M. (2)R之后:A持有POR,B持有POO 和M. 即:?R,POR∈OA ∧POO∈OB.

定義8 (不可否認(rèn)性) 若Pr 既滿(mǎn)足發(fā)方不可否認(rèn)性, 又滿(mǎn)足收方不可否認(rèn)性, 則Pr 滿(mǎn)足不可否認(rèn)性.

定義9 (公平性) Pr 滿(mǎn)足公平性, 若對(duì)于任意的R有: (1)R之前:A持有M且A不持有POR,B不持有POO 和M. (2)R之后:A持有POR 且B持有M和POO, 或者A不持有POR 且B不持有POO 和M. (3) 如果A持有POR, 那么B持有M; 如果B持有POO 和M, 那么A持有M.

定義10 (可中斷) 可中斷是指協(xié)議語(yǔ)句在執(zhí)行中可能會(huì)出現(xiàn)諸如未執(zhí)行、未正確執(zhí)行等異常情況. 如A →B:M就是可中斷的, 因?yàn)榉钦\(chéng)實(shí)的A可能會(huì)因私利而未按規(guī)定執(zhí)行該語(yǔ)句.

定義11 (不可中斷) 不可中斷是指協(xié)議語(yǔ)句在執(zhí)行中不可能出現(xiàn)諸如未執(zhí)行、未正確執(zhí)行等異常情況. 如B ?TTP :M就是不可中斷的, 因?yàn)檎\(chéng)實(shí)的TTP 總會(huì)在ftp 服務(wù)中發(fā)布M,B總會(huì)利用ftp 設(shè)法從TTP 處獲取M.

公平性可形式化為, 對(duì)于Pr 的任意可中斷語(yǔ)句i, 若POO∈iffPOR∈, 則Pr 滿(mǎn)足公平性.

定義12 (發(fā)方時(shí)限性) Pr 滿(mǎn)足發(fā)方時(shí)限性, 若對(duì)于Pr 的任意運(yùn)行實(shí)例R都有: (1)R之前:A持有M但不持有POR. (2)R之后:A持有POR. (3) 若A在T時(shí)間發(fā)送了M, 則其一定可在未來(lái)ε(ε ?+∞) 時(shí)長(zhǎng)內(nèi)持有POR. 即J ?(A ∝M@[T],A?POR@[Tx|{t|T ≤t ≤T+ε, ε ?+∞}]).

定義13 (收方時(shí)限性) Pr 滿(mǎn)足收方時(shí)限性, 若對(duì)于Pr 的任意運(yùn)行實(shí)例R都有: (1)R之前:B不持有POO 和M. (2)R之后:B持有POO 和M. (3) 若B在T時(shí)間持有M, 則其一定在之前的ε(ε ?+∞) 時(shí)長(zhǎng)內(nèi)持有POO. 即J ?(B?M@[T],B?POO@[Ty|{t|T-ε ≤t ≤T, ε ?+∞}]).

定義14 (時(shí)限性) 若Pr 既滿(mǎn)足發(fā)方時(shí)限性, 又滿(mǎn)足收方時(shí)限性, 則Pr 滿(mǎn)足時(shí)限性.

3 ZG 協(xié)議分析

3.1 協(xié)議描述

ZG 協(xié)議[8]的交互步驟描述如下:

3.2 協(xié)議假設(shè)集

協(xié)議各方擁有CA為其生成的簽名私鑰與驗(yàn)證公鑰, 且可訪(fǎng)問(wèn)其他方的驗(yàn)證公鑰.

3.3 存活性

定理1 (ZG 協(xié)議滿(mǎn)足存活性) ZG 協(xié)議存在成功運(yùn)行實(shí)例, 且在該實(shí)例中發(fā)方A和收方B均可收到自己想要的證據(jù).

證明: 當(dāng)發(fā)方A和收方B遵照Z(yǔ)G 協(xié)議步驟執(zhí)行交互時(shí), 協(xié)議能夠成功運(yùn)行.

3.4 不可否認(rèn)性

由定理2、3 和定義8, 可知ZG 協(xié)議滿(mǎn)足不可否認(rèn)性.

3.5 公平性

定理4 (ZG 協(xié)議滿(mǎn)足公平性) ZG 協(xié)議執(zhí)行完成后, 要么發(fā)方A和收方B都能收集到自己想要的證據(jù), 要么都收集不到任何對(duì)己有利的證據(jù), 即POO∈OiBiffPOR∈OiA, 0≤i ≤5.

證明: 分兩種情況討論: 協(xié)議成功執(zhí)行和協(xié)議中斷執(zhí)行.

3.6 時(shí)限性

綜上所述, 利用擴(kuò)展ZQZ 邏輯方法分析到ZG 協(xié)議滿(mǎn)足存活性、不可否認(rèn)性、公平性, 但不滿(mǎn)足時(shí)限性, 對(duì)收方不公平, 是邏輯存在局部錯(cuò)誤的協(xié)議, 所獲分析結(jié)論與既有事實(shí)相符.

4 KPB 協(xié)議分析

4.1 協(xié)議描述及假設(shè)集

針對(duì)ZG 協(xié)議存在的時(shí)限性問(wèn)題, Kim 等人[32]通過(guò)向協(xié)議消息中添加時(shí)間限制信息的辦法對(duì)其進(jìn)行了改進(jìn). 改進(jìn)后的協(xié)議(KPB 協(xié)議) 描述如下:

協(xié)議執(zhí)行后,A和B收集到的證據(jù)與ZG 協(xié)議相同. 由于該協(xié)議沒(méi)有改變?cè)瓍f(xié)議的交互步驟與證據(jù)信息, 故其提供的存活性、不可否認(rèn)性和公平性級(jí)別不會(huì)低于原協(xié)議. 然而, 由于其在協(xié)議消息中添加了時(shí)間約束信息, 故需分析該協(xié)議是否如Kim 等人宣稱(chēng)的那樣, 彌補(bǔ)了原協(xié)議不滿(mǎn)足時(shí)限性的問(wèn)題.

4.2 時(shí)限性

由定理7 和定理8 可知, 該協(xié)議滿(mǎn)足時(shí)限性. 即, Kim 等人通過(guò)向Zhou-Gollman 協(xié)議中添加時(shí)間約束信息, 解決了原協(xié)議不滿(mǎn)足時(shí)限性的問(wèn)題.

綜上所述, 利用擴(kuò)展ZQZ 邏輯方法分析到KPB 協(xié)議同時(shí)滿(mǎn)足不可否認(rèn)協(xié)議的四個(gè)安全性質(zhì), 是邏輯正確的協(xié)議, 所獲分析結(jié)論與既有事實(shí)相符.

5 YLL 協(xié)議分析及改進(jìn)

5.1 協(xié)議描述及假設(shè)集

文獻(xiàn)[14] 提出了一個(gè)基于區(qū)塊鏈的多方不可否認(rèn)協(xié)議(簡(jiǎn)稱(chēng)YLL 協(xié)議). 簡(jiǎn)要描述如下:

5.2 收方時(shí)限性

文獻(xiàn)[14] 認(rèn)為YLL 滿(mǎn)足時(shí)限性, 并指出“協(xié)議的所有參與方都可以在時(shí)刻T之前完成協(xié)議, 而不影響公平性”. 此處我們使用擴(kuò)展ZQZ 邏輯分析出其并不能為收方提供如協(xié)議設(shè)計(jì)者所宣稱(chēng)的時(shí)限性.

定理9 (YLL 協(xié)議不滿(mǎn)足收方時(shí)限性) 在YLL 協(xié)議的任意運(yùn)行實(shí)例中, 當(dāng)收方所在網(wǎng)絡(luò)不可用的時(shí)間長(zhǎng)度t0大于發(fā)方所承諾的收方可從鏈上檢索到交易信息的最遲期限T與信息上鏈的真實(shí)時(shí)間TOPEN之間的時(shí)間差(T-TOPEN) 時(shí), 即使T ≥TOPEN, 收方也無(wú)法在時(shí)刻T之前完成協(xié)議且不影響公平性.

其中TBi是Bi規(guī)定的A將OPEN(in:TAx) 廣播到區(qū)塊鏈的最遲期限. 利用擴(kuò)展ZQZ 邏輯方法容易證明改進(jìn)后的協(xié)議遵循四個(gè)安全性質(zhì).

6 方法比較

表1 對(duì)邏輯推理、狀態(tài)檢測(cè)、定理證明和進(jìn)程代數(shù)這四類(lèi)分析不可否認(rèn)協(xié)議邏輯正確性的常見(jiàn)方法進(jìn)行了比較. 其一, 作為一種邏輯推理類(lèi)方法, 擴(kuò)展ZQZ 邏輯在抽象程度高、無(wú)狀態(tài)爆炸、分析難度低等方面較其它三大類(lèi)方法均具有明顯的優(yōu)勢(shì); 其二, 作為一種類(lèi)Kailar 邏輯, 擴(kuò)展ZQZ 邏輯是基于責(zé)任分析而非信念推理, 因而較SVO 邏輯及變體更適用于分析不可否認(rèn)協(xié)議邏輯正確性; 其三, 相較于原ZQZ 邏輯, 擴(kuò)展ZQZ 邏輯能夠描述與分析時(shí)間約束關(guān)系, 其不僅能夠分析協(xié)議的存活性、不可否認(rèn)性和公平性,而且還能分析時(shí)限性.

表1 不可否認(rèn)協(xié)議常見(jiàn)形式化分析方法比較Table 1 Comparison of common formal analysis methods for non-repudiation protocol

7 結(jié)束語(yǔ)

通過(guò)向ZQZ 邏輯添加時(shí)間表達(dá)式, 提出了一種適用于不可否認(rèn)協(xié)議分析的擴(kuò)展ZQZ 邏輯方法, 給出了推理規(guī)則擴(kuò)展和安全性質(zhì)模型, 并以?xún)蓚€(gè)兩方不可否認(rèn)協(xié)議和一個(gè)基于區(qū)塊鏈的多方不可否認(rèn)協(xié)議為實(shí)驗(yàn)對(duì)象, 介紹了將該邏輯方法應(yīng)用于不可否認(rèn)協(xié)議分析的使用過(guò)程. 與原ZQZ 邏輯方法相比, 該方法除了繼承了面向責(zé)任分析、初始假設(shè)形式化、抽象程度高、無(wú)狀態(tài)爆炸、可分析協(xié)議的不可否認(rèn)性和公平性等特征外, 還可分析協(xié)議的存活性和時(shí)限性, 并能提供更強(qiáng)的密文處理能力.

下一步工作是, 針對(duì)多方不可否認(rèn)協(xié)議中共謀實(shí)體間的合作博弈, 以及共謀者與被排斥者之間的非合作博弈本質(zhì), 拓展基于博弈論的交替轉(zhuǎn)換邏輯, 并將其引入到擴(kuò)展ZQZ 邏輯中, 使其能夠分析多方不可否認(rèn)協(xié)議的無(wú)排斥性和抗合謀性等特殊性質(zhì), 以減輕目前多方電子支付中存在的網(wǎng)絡(luò)欺詐現(xiàn)象.