本文關(guān)鍵詞：基于強認證理論的三方網(wǎng)絡(luò)協(xié)議安全性證明

  更多相關(guān)文章： 形式化方法 事件邏輯 強認證理論 Neuman-Stubblebine協(xié)議

【摘要】：形式化方法是分析網(wǎng)絡(luò)安全協(xié)議的一種重要方法,網(wǎng)絡(luò)協(xié)議安全性也是信息安全領(lǐng)域的研究熱點。事件邏輯是一種描述分布式系統(tǒng)中狀態(tài)遷移的形式化方法,用于證明網(wǎng)絡(luò)安全協(xié)議的安全性。以事件邏輯為基礎(chǔ),定義強匹配及匹配會話,結(jié)合事件邏輯公理和推理規(guī)則,提出了強認證理論。利用該理論對有3個主體的Neuman-Stubblebine協(xié)議進行了研究,分析得出發(fā)送者是安全的而接收者是不安全的,從而證明了該協(xié)議是不安全的,說明了強認證理論適用于三方的網(wǎng)絡(luò)安全協(xié)議。該理論適用于類似多方網(wǎng)絡(luò)安全協(xié)議的安全性證明。
【作者單位】： 華東交通大學(xué)軟件學(xué)院;中國人民財產(chǎn)保險股份有限公司寧波市分公司信息技術(shù)部;
【關(guān)鍵詞】： 形式化方法 事件邏輯 強認證理論 Neuman-Stubblebine協(xié)議
【基金】：國家自然科學(xué)基金Nos.61163005,61562026 江西省自然科學(xué)基金Nos.20132BAB201033,20161BAB202063 江西省對外科技合作技術(shù)項目No.20151BDH80005 江西省軟科學(xué)研究計劃項目No.20151BBA10042 江西省高校科技落地計劃項目No.KJLD13038 南方山地果園智能化管理與裝備協(xié)同創(chuàng)新中心資助項目 江西省普通本科高校中青年教師發(fā)展計劃訪問學(xué)者專項資金~~
【分類號】：TP393.08
【正文快照】： 1 引言 證明網(wǎng)絡(luò)協(xié)議的安全屬性是一個復(fù)雜的問題。形式化方法是一種強大的證明網(wǎng)絡(luò)協(xié)議的安全屬性的方法,其包括模態(tài)邏輯、定理證明和模型檢測[1]。模態(tài)邏輯和定理證明又可籠統(tǒng)地歸為一類。模型檢測自動化程度高,用來驗證系統(tǒng)的不安全性,但是只能對有限數(shù)量的并行通信進行研

【相似文獻】

中國期刊全文數(shù)據(jù)庫 前10條

1 古天龍;董榮勝;;歐洲高校計算機專業(yè)的形式化方法課程教學(xué)[J];計算機教育;2008年10期

2 柴振榮;《編程中的形式化方法及其應(yīng)用》會議[J];管理科學(xué)文摘;1995年06期

3 鄭士貴;智能服務(wù)網(wǎng)絡(luò)形式化方法的模擬和實質(zhì)[J];管理科學(xué)文摘;1997年01期

4 姜利;孫永強;;形式化方法的發(fā)展及展望[J];計算機科學(xué);1998年02期

5 張廣泉;關(guān)于軟件形式化方法[J];重慶師范學(xué)院學(xué)報(自然科學(xué)版);2002年02期

6 鹿蕾;;形式化方法B的證明技術(shù)[J];現(xiàn)代電子技術(shù);2005年23期

7 陳澎;設(shè)計模式形式化方法分析和初步比較[J];計算機工程;2005年02期

8 李建華;李紅革;;形式化及其歷史發(fā)展[J];自然辯證法研究;2008年08期

9 曹源;唐濤;徐田華;穆建成;;形式化方法在列車運行控制系統(tǒng)中的應(yīng)用[J];交通運輸工程學(xué)報;2010年01期

10 ;《軟件學(xué)報》形式化方法和工具�？魑耐ㄖ猍J];軟件學(xué)報;2010年07期

中國重要會議論文全文數(shù)據(jù)庫 前7條

1 李文健;;形式化的涵義及其認識論本質(zhì)[A];1993年邏輯研究專輯[C];1993年

2 吳允曾;;關(guān)于形式化的幾個問題[A];金岳霖學(xué)術(shù)思想研究——金岳霖學(xué)術(shù)思想研討會論文集[C];1985年

3 鄭宇軍;石海鶴;薛錦云;;Spec#語言中的形式化特性[A];2005年全國理論計算機科學(xué)學(xué)術(shù)年會論文集[C];2005年

4 雷敏;雷友殉;;一種UML到SDL轉(zhuǎn)換方法的研究與應(yīng)用[A];2006通信理論與技術(shù)新進展——第十一屆全國青年通信學(xué)術(shù)會議論文集[C];2006年

5 苗潔君;王克;;密碼模塊的形式化設(shè)計和驗證研究[A];第二十一次全國計算機安全學(xué)術(shù)交流會論文集[C];2006年

6 繆道期;;評審計算機安全等級[A];第二次計算機安全技術(shù)交流會論文集[C];1987年

7 趙曉峰;;城市軌道交通自主化信號系統(tǒng)全面創(chuàng)新實踐[A];中國系統(tǒng)工程學(xué)會第十八屆學(xué)術(shù)年會論文集——A12系統(tǒng)科學(xué)與系統(tǒng)工程理論在各個領(lǐng)域中的應(yīng)用研究[C];2014年

中國重要報紙全文數(shù)據(jù)庫 前1條

1 殷杰 安軍 山西大學(xué)科學(xué)技術(shù)哲學(xué)研究中心;21世紀(jì)科學(xué)哲學(xué)的關(guān)鍵詞:語境、科學(xué)理性與形式化[N];中國社會科學(xué)報;2011年

中國博士學(xué)位論文全文數(shù)據(jù)庫 前8條

1 劉艷;互聯(lián)網(wǎng)內(nèi)容分級服務(wù)技術(shù)標(biāo)準(zhǔn)體系的形式化設(shè)計與驗證[D];華中師范大學(xué);2015年

2 錢振江;安全操作系統(tǒng)形式化設(shè)計與驗證方法研究[D];南京大學(xué);2013年

3 劉強;設(shè)計模式的形式化研究及其EMF實現(xiàn)[D];華東師范大學(xué);2011年

4 張鵬;形式化方法在云計算中的應(yīng)用研究[D];吉林大學(xué);2014年

5 劉洋;網(wǎng)絡(luò)式軟件需求驗證的形式化方法研究[D];電子科技大學(xué);2013年

6 王邁;語言形式化原理[D];上海外國語大學(xué);2011年

7 胡靜;基于Pi-演算的Web服務(wù)形式化描述模型[D];天津大學(xué);2013年

8 周寧;代數(shù)化符號模擬驗證的應(yīng)用研究[D];北京交通大學(xué);2015年

中國碩士學(xué)位論文全文數(shù)據(jù)庫 前10條

1 王春曉;MDF連續(xù)平壓質(zhì)量控制形式化建模及優(yōu)化研究[D];東北林業(yè)大學(xué);2015年

2 王亞麗;面向機器人規(guī)劃的形式化研究[D];北京化工大學(xué);2015年

3 韓佳芮;基于Event-B和MAS的車站進路聯(lián)鎖控制邏輯的形式化方法研究[D];蘭州交通大學(xué);2015年

4 徐世澤;基于Timed RAISE的RBC切換建模與分析[D];蘭州交通大學(xué);2015年

5 郭葉芳;電網(wǎng)控制系統(tǒng)軟件可靠性分析的形式化方法研究[D];華北電力大學(xué);2015年

6 黃峰;系統(tǒng)演化的形式化與具體化研究[D];南京郵電大學(xué);2014年

7 Hamza I.Bangura;基于Z規(guī)格的軟件缺陷形式化方法[D];天津大學(xué);2010年

8 鐘琪;軟件分析模式的形式化研究[D];西南師范大學(xué);2004年

9 王祥兵;形式化方法的理論及其影響[D];貴州大學(xué);2009年

10 郭忠偉;神經(jīng)內(nèi)分泌復(fù)雜系統(tǒng)的形式化研究[D];揚州大學(xué);2009年

，

本文編號：1000590