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

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

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

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

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

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

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