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

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

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

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