電子商務(wù)協(xié)議安全性的形式化分析方法研究.pdf

1、為了保障電子商務(wù)活動(dòng)中各方的利益不被侵害，需要利用基于密碼技術(shù)的電子商務(wù)協(xié)議來(lái)保證商務(wù)活動(dòng)的安全性，因此對(duì)電子商務(wù)協(xié)議的安全性的形式化分析是一個(gè)至關(guān)重要的有難度的問題。
　　 針對(duì)電子商務(wù)協(xié)議安全性的形式化分析方法的研究晚于對(duì)傳統(tǒng)的密碼協(xié)議的形式化分析方法的研究，目前主要的分析方法有：Kailar邏輯，SVO邏輯，基于SMV的模型檢測(cè)，基于ATL/ATS博弈邏輯系統(tǒng)的分析方法，以及卿斯?jié)h等學(xué)者提出的對(duì)兩方或者多方電子商務(wù)協(xié)議和公

2、平交換協(xié)議進(jìn)行分析、證明的方法。這些方法分別從協(xié)議的消息語(yǔ)義、協(xié)議結(jié)構(gòu)角度對(duì)協(xié)議進(jìn)行建模與分析。綜合考慮協(xié)議的消息和結(jié)構(gòu)兩個(gè)因素的形式化分析方法較少。當(dāng)前，對(duì)電子商務(wù)協(xié)議的形式化分析方法的研究依然是一個(gè)熱點(diǎn)領(lǐng)域。
　　 本文首先對(duì)主要的博弈邏輯：ATL邏輯、ATEL邏輯、ATL-A/ATEL-A邏輯、多代理邏輯等，進(jìn)行了研究，發(fā)現(xiàn)他們對(duì)博弈主體的狀態(tài)轉(zhuǎn)移的建模方式采用固定的步驟。本文提出了一個(gè)智能代理博弈主體模型(IA)，在IA

3、中，一個(gè)博弈主體的狀態(tài)由博弈主體根據(jù)其接收的消息按照邏輯推理規(guī)則進(jìn)行狀態(tài)的更新，在每一個(gè)狀態(tài)，根據(jù)推理規(guī)則推演出當(dāng)前可發(fā)送消息集合。多個(gè)IA構(gòu)成了一個(gè)基于消息的并發(fā)博弈系統(tǒng)(MCGS)，這個(gè)系統(tǒng)中每一步的遷移是通過兩個(gè)動(dòng)作完成，分別是：各個(gè)IA的收發(fā)消息，以及各IA根據(jù)自己接收的消息按邏輯推理規(guī)則更新自身狀態(tài)。整個(gè)系統(tǒng)的策略使用基于ATL擴(kuò)展的ATL-B邏輯進(jìn)行表達(dá)。IA，MCGS，ATL-B共同構(gòu)成了一個(gè)對(duì)系統(tǒng)進(jìn)行建模的工具，稱為MI

4、AG(多智能體博弈)系統(tǒng)，這個(gè)系統(tǒng)的特點(diǎn)是各博弈主體之間只通過消息交互，每個(gè)主體有自己的認(rèn)知推理邏輯規(guī)則用以更新狀態(tài)，與其他博弈邏輯相比，博弈主體具有動(dòng)態(tài)的狀態(tài)遷移特性。
　　 基于MIAG模型，本文構(gòu)建了一個(gè)電子商務(wù)協(xié)議分析的新模型，其主要特點(diǎn)是在博弈主體中引入了針對(duì)電子商務(wù)協(xié)議的邏輯推理規(guī)則用于更新博弈主體的認(rèn)知狀態(tài)；使用ATL-B策略公式表達(dá)不同的安全目標(biāo)，使其能夠適應(yīng)對(duì)不同目的的電子商務(wù)協(xié)議的建模要求。在新模型中，將協(xié)議

5、主體分成誠(chéng)實(shí)主體與非誠(chéng)實(shí)主體兩個(gè)集合，分析過程依次針對(duì)誠(chéng)實(shí)主體的各個(gè)協(xié)議運(yùn)行跡分析非誠(chéng)實(shí)方是否存在攻擊策略。本文總結(jié)了四種典型的非誠(chéng)實(shí)方攻擊策略，使得本文的分析模型能夠比之前的模型更切合實(shí)際的形式化非誠(chéng)實(shí)主體的能力。
　　 應(yīng)用電子商務(wù)協(xié)議分析的新模型，本文對(duì)一個(gè)公平交換協(xié)議Nenadi04和一個(gè)無(wú)需中央機(jī)構(gòu)的電子投票協(xié)議Su-Vote協(xié)議進(jìn)行了分析，發(fā)現(xiàn)了協(xié)議中存在的漏洞，說(shuō)明了新模型的有效性。在對(duì)Nenadi04協(xié)議的分析中

6、，利用新模型發(fā)現(xiàn)了發(fā)方不可否認(rèn)證據(jù)不滿足可追究性的要求，也發(fā)現(xiàn)了協(xié)議中發(fā)起方可以利用并發(fā)多個(gè)協(xié)議實(shí)例來(lái)混淆應(yīng)答方對(duì)恢復(fù)子協(xié)議接收消息的識(shí)別，從而破壞協(xié)議的公平性。這個(gè)協(xié)議實(shí)例說(shuō)明了新模型能夠同時(shí)處理對(duì)消息和協(xié)議結(jié)構(gòu)的分析。對(duì)Su-Vote協(xié)議的分析中發(fā)現(xiàn)非誠(chéng)實(shí)的投票人能夠篡改投票結(jié)果并能夠控制協(xié)議是否終止。
　　 本文最后研究了公平交換協(xié)議的一種基礎(chǔ)簽名算法——并發(fā)簽名，提出并定義了并發(fā)簽名的可追蹤性以保證簽名方與簽署消息之間的