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

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

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

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