基于模型檢測(cè)的電子商務(wù)協(xié)議形式化驗(yàn)證方法研究.pdf

1、安全的電子商務(wù)協(xié)議是保證電子商務(wù)活動(dòng)正常開(kāi)展的基礎(chǔ)。一個(gè)貌似安全的協(xié)議往往存在安全上的漏洞。模型檢測(cè)是一種常見(jiàn)的形式化分析方法，在驗(yàn)證電子商務(wù)協(xié)議時(shí)，它的邏輯推理能力比較弱。此外，隨著網(wǎng)絡(luò)的大規(guī)模應(yīng)用，需要分析安全的電子商務(wù)協(xié)議在不可靠環(huán)境下并發(fā)運(yùn)行時(shí)是否仍然保持安全性。本文主要結(jié)果如下： 1.基于消息轉(zhuǎn)換的驗(yàn)證模型。定義了一個(gè)擴(kuò)展的有限狀態(tài)自動(dòng)機(jī)、一些新的邏輯轉(zhuǎn)換規(guī)則，并給出了詳細(xì)的分析步驟。用擴(kuò)展的FSA根據(jù)消息為協(xié)議建模，

2、不僅可動(dòng)態(tài)顯示各個(gè)參與者并發(fā)執(zhí)行協(xié)議的過(guò)程，而且增強(qiáng)了自動(dòng)機(jī)的邏輯分析能力。利用該方法分析匿名原子交易協(xié)議，可知當(dāng)交易主體誠(chéng)實(shí)時(shí)，該協(xié)議滿(mǎn)足可追究性、公平性、原子性等；對(duì)協(xié)議模型抽象后，借助模型檢測(cè)工具UPPAAL驗(yàn)證了協(xié)議的活性。 2.基于動(dòng)作轉(zhuǎn)換的驗(yàn)證模型。定義了一個(gè)信任矩陣和一個(gè)動(dòng)作集合，并將它們和邏輯規(guī)則一起引入有限狀態(tài)自動(dòng)機(jī)為協(xié)議參與者建模。信任矩陣形式化了協(xié)議參與者之間的信任關(guān)系，從而無(wú)需初始化假設(shè)；動(dòng)作集合將加密、

3、簽名等動(dòng)作明確地表示出來(lái)，從而在規(guī)范協(xié)議時(shí)無(wú)需理想化過(guò)程。利用該方法分析匿名原子交易協(xié)議，可知當(dāng)交易主體不誠(chéng)實(shí)時(shí)，該協(xié)議不滿(mǎn)足可追究性；通過(guò)搜索參與者進(jìn)程的模型，找到了性質(zhì)不滿(mǎn)足的原因，從而對(duì)原協(xié)議進(jìn)行了修改；對(duì)修改后的協(xié)議進(jìn)一步分析，發(fā)現(xiàn)其滿(mǎn)足可追究性、公平性、原子性等。 3.用模型檢測(cè)方法分析了不可靠環(huán)境下協(xié)議的安全性質(zhì)。驗(yàn)證結(jié)果表明，一個(gè)安全的電子商務(wù)協(xié)議在不可靠環(huán)境下由多對(duì)參與者同時(shí)執(zhí)行時(shí)，有可能不再滿(mǎn)足安全性質(zhì)；當(dāng)安全