安全交換協(xié)議模型檢測平臺的設(shè)計與實現(xiàn).pdf

1、隨著計算機網(wǎng)絡(luò)技術(shù)的發(fā)展和電子商務(wù)的普及，電子數(shù)據(jù)交換變得越來越重要，但是，伴隨而來的安全性、公平性及不可否認性等問題也困擾著電子商務(wù)的供應(yīng)商及消費者。作為電子商務(wù)的基石，安全交換協(xié)議為數(shù)據(jù)交換問題提供了一種有效的解決方案。由于安全交換協(xié)議地位的重要性，結(jié)構(gòu)的不對稱性及復(fù)雜性，對其安全分析是近幾年來信息安全領(lǐng)域的一個研究熱點與難點。目前，國內(nèi)外已有一些安全交換協(xié)議分析方法，包括Paulson歸納法，CSP形式化建模法，及串空間模型法等，

2、但是這些方法往往具有無法對密碼原語建模，無法自動生成攻擊者模型，無法形式化描述協(xié)議性質(zhì)等缺點。
　　本文對安全交換協(xié)議及其形式化分析方法進行了研究，基于可對密碼原語建模的應(yīng)用Pi演算以及線性時序邏輯提出了一種新的安全交換協(xié)議的分析方法，并利用Antlr和C＃語言實現(xiàn)了安全交換協(xié)議模型檢測平臺。主要研究包括如下幾個方面：首先以Proverif建模語言Pi演算為基礎(chǔ)，擴展選擇算子，用于安全協(xié)議交換協(xié)議的形式化描述；然后給出公平性及不可

3、否認性定義，使用線性時序邏輯語言（Linear Temporal Logic，LTL）形式化描述公式，并將LTL描述的性質(zhì)轉(zhuǎn)化為Büchi自動機；接著基于彈性信道理論，改進Dolve-Yao攻擊者模型庫，使其更符合安全交換協(xié)議攻擊者行為，實現(xiàn)根據(jù)協(xié)議自動生成攻擊者，然后將添加了攻擊者的協(xié)議Pi演算模型轉(zhuǎn)換為標(biāo)號轉(zhuǎn)移系統(tǒng)（Labelled Transition System，LTS）；最后，利用Tarjan算法，結(jié)合MoveOneStep