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

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

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

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