本文關(guān)鍵詞：基于SAT的安全協(xié)議惰性形式化分析方法

  更多相關(guān)文章： 安全協(xié)議 形式化分析 布爾可滿足性 惰性分析 類型缺陷攻擊

【摘要】：提出了一種基于布爾可滿足性問題的安全協(xié)議形式化分析方法 SAT-LMC,通過引入惰性分析的思想優(yōu)化初始狀態(tài)與轉(zhuǎn)換規(guī)則,提高了安全性的檢測效率。另一方面,通過在消息類型上定義偏序關(guān)系,SAT-LMC能夠檢測出更豐富的類型缺陷攻擊。基于此方法實(shí)現(xiàn)了一個安全協(xié)議分析工具,針對Otway-Rees協(xié)議檢測出了一種類型缺陷攻擊;針對OAuth2.0協(xié)議,檢測結(jié)果顯示對現(xiàn)實(shí)中存在的一些應(yīng)用場景,存在一種利用授權(quán)碼截取的中間人攻擊。
【作者單位】： 解放軍信息工程大學(xué)網(wǎng)絡(luò)空間安全學(xué)院;數(shù)學(xué)工程與先進(jìn)計(jì)算國家重點(diǎn)實(shí)驗(yàn)室;
【基金】：河南省科技創(chuàng)新杰出青年基金資助項(xiàng)目(134100510002) 河南省基礎(chǔ)與前沿技術(shù)研究基金資助項(xiàng)目(142300410002) 數(shù)學(xué)工程與先進(jìn)計(jì)算國家重點(diǎn)實(shí)驗(yàn)室開放基金資助項(xiàng)目~~
【分類號】：TP393.08
【正文快照】： 1引言隨著計(jì)算機(jī)網(wǎng)絡(luò)技術(shù)的飛速發(fā)展,網(wǎng)絡(luò)信息安全問題越來越受到人們的重視。網(wǎng)絡(luò)安全協(xié)議采用密碼技術(shù)實(shí)現(xiàn)通信和數(shù)據(jù)安全,在整個網(wǎng)絡(luò)安全保障體系中具有舉足輕重的作用。隨著協(xié)議的流程步驟和網(wǎng)絡(luò)環(huán)境的日益復(fù)雜,安全協(xié)議的安全性分析評估具有非常重要的意義和價(jià)值。近年來

【相似文獻(xiàn)】

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

1 卜奎昊;;安全協(xié)議形式化分析方法的融合性研究[J];西北師范大學(xué)學(xué)報(bào)(自然科學(xué)版);2010年05期

2 卿斯?jié)h;一種電子商務(wù)協(xié)議形式化分析方法[J];軟件學(xué)報(bào);2005年10期

3 韓繼紅;郭淵博;王亞弟;;安全協(xié)議形式化分析方法[J];信息工程大學(xué)學(xué)報(bào);2008年03期

4 王昕;袁超偉;;一種安全協(xié)議的形式化分析方法[J];計(jì)算機(jī)工程;2010年07期

5 辛思遠(yuǎn);趙勇;王婷;;動態(tài)遠(yuǎn)程證明協(xié)議及其形式化分析[J];計(jì)算機(jī)工程與設(shè)計(jì);2012年08期

6 譚新蓮;李磊;;安全電子商務(wù)協(xié)議的形式化分析[J];數(shù)學(xué)愛好者(教育學(xué)術(shù));2008年02期

7 趙華偉;李大興;;加入時間因素的Needham-Schorder協(xié)議及其形式化分析[J];計(jì)算機(jī)工程與應(yīng)用;2005年36期

8 徐夢茗;肖聰;李斌;杜彪;;安全協(xié)議形式化分析的研究和實(shí)現(xiàn)[J];信息安全與通信保密;2008年08期

9 崔楠;;電子郵件協(xié)議的非否認(rèn)性形式化分析[J];計(jì)算機(jī)與信息技術(shù);2009年05期

10 陳晨;陳衛(wèi)紅;閆振天;祝躍飛;;基于項(xiàng)重寫的形式化排序方法及應(yīng)用[J];通信學(xué)報(bào);2011年03期

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

1 文靜華;張梅;張煥國;;電子支付協(xié)議的博弈邏輯模型與形式化分析[A];2007年全國開放式分布與并行計(jì)算機(jī)學(xué)術(shù)會議論文集(上冊)[C];2007年

2 顧永跟;傅育熙;朱涵;呂銀華;;基于進(jìn)程演算的安全協(xié)議形式化分析[A];2005年全國理論計(jì)算機(jī)科學(xué)學(xué)術(shù)年會論文集[C];2005年

3 肖美華;鄧宸芳;馬小薏;薛錦云;江耘;;網(wǎng)絡(luò)安全認(rèn)證協(xié)議形式化分析[A];第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會論文集[C];2005年

4 崔楠;汪學(xué)明;;基于SVO邏輯的電子商務(wù)協(xié)議非否認(rèn)性形式化分析[A];邏輯學(xué)及其應(yīng)用研究——第四屆全國邏輯系統(tǒng)、智能科學(xué)與信息科學(xué)學(xué)術(shù)會議論文集[C];2008年

5 張梅;文靜華;張煥國;;基于ATL的電子商務(wù)協(xié)議建模與形式化分析[A];2009年全國開放式分布與并行計(jì)算機(jī)學(xué)術(shù)會議論文集(上冊)[C];2009年

6 李秋山;胡游君;;低成本RFID系統(tǒng)安全協(xié)議設(shè)計(jì)及其形式化分析[A];2006北京地區(qū)高校研究生學(xué)術(shù)交流會——通信與信息技術(shù)會議論文集（上）[C];2006年

7 謝鴻波;周明天;;安全協(xié)議的形式化技術(shù):述評[A];’2004計(jì)算機(jī)應(yīng)用技術(shù)交流會議論文集[C];2004年

8 徐銳;;設(shè)計(jì)安全協(xié)議[A];第十八次全國計(jì)算機(jī)安全學(xué)術(shù)交流會論文集[C];2003年

9 劉忠;王成道;;基于漢語語意形式系統(tǒng)的符號化研究[A];第六屆全國計(jì)算機(jī)應(yīng)用聯(lián)合學(xué)術(shù)會議論文集[C];2002年

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

1 范紅;安全協(xié)議形式化分析理論與方法[D];中國人民解放軍信息工程大學(xué);2003年

2 張帆;無線網(wǎng)絡(luò)安全協(xié)議的形式化分析方法[D];西安電子科技大學(xué);2007年

3 陳俊清;可信普適服務(wù)的形式化分析與驗(yàn)證[D];上海交通大學(xué);2012年

4 汪學(xué)明;多方安全協(xié)議的形式化分析方法研究與應(yīng)用[D];貴州大學(xué);2008年

5 楊超;無線網(wǎng)絡(luò)協(xié)議的形式化分析與設(shè)計(jì)[D];西安電子科技大學(xué);2008年

6 魯來鳳;安全協(xié)議形式化分析理論與應(yīng)用研究[D];西安電子科技大學(xué);2012年

7 趙輝;安全協(xié)議形式化分析技術(shù)的研究[D];大連理工大學(xué);2010年

8 何安平;基于層次模型的混合系統(tǒng)形式化分析與驗(yàn)證[D];蘭州大學(xué);2011年

9 李云峰;電子商務(wù)協(xié)議安全性的形式化分析方法研究[D];西南交通大學(xué);2009年

10 閆麗麗;基于串空間理論的安全協(xié)議研究[D];西南交通大學(xué);2012年

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

1 王潔;公平不可否認(rèn)協(xié)議設(shè)計(jì)及其形式化分析[D];重慶大學(xué);2008年

2 成敏盈;電力系統(tǒng)安全協(xié)議形式化分析技術(shù)研究[D];廣東工業(yè)大學(xué);2008年

3 李軼，

本文編號：1185265