發(fā)布時間：2019-09-20 05:40

【摘要】：針對安全協(xié)議的形式化驗證問題,運(yùn)用模型檢測方法,以一種改進(jìn)的入侵者Promela語義模型,對雙方密鑰分配中心協(xié)議進(jìn)行Spin模型檢測,驗證發(fā)現(xiàn)其不滿足線性時序邏輯(LTL)公式描述的安全性,得到了原協(xié)議的安全漏洞。針對該漏洞,提出了一種協(xié)議改進(jìn)方案,并針對改進(jìn)后的協(xié)議,給出新的Promela語義模型的建模方法。改進(jìn)的入侵者模型建模方法比起原方法:模型檢測過程中的存儲狀態(tài)數(shù)減少,使模型復(fù)雜度降低約40%;遷移狀態(tài)數(shù)減少,使驗證效率提升約44%。
【作者單位】： 中國科學(xué)院成都計算機(jī)應(yīng)用研究所;中國科學(xué)院大學(xué);廣西混雜計算與集成電路設(shè)計分析重點實驗室(廣西民族大學(xué));北京交通大學(xué)計算機(jī)與信息技術(shù)學(xué)院;
【基金】：國家自然科學(xué)基金資助項目(11371003) 廣西自然科學(xué)基金資助項目(2011GXNSFA018154,2012GXNSFGA060003) 廣西區(qū)主席科技資金資助項目(10169-1) 廣西教育廳科研資助項目(201012MS274)
【分類號】：TN918.4

【共引文獻(xiàn)】

相關(guān)期刊論文 前10條

1 李月寒;鄭議天;;信息安全關(guān)鍵技術(shù)演示系統(tǒng)的設(shè)計與實現(xiàn)[J];合肥師范學(xué)院學(xué)報;2008年06期

2 王凱;高陽陽;秦雅娟;;分離機(jī)制下一種互聯(lián)網(wǎng)安全接入方法[J];北京交通大學(xué)學(xué)報;2011年02期

3 李蘭翠;孟博;;網(wǎng)絡(luò)投票協(xié)議[J];長江大學(xué)學(xué)報(自然科學(xué)版)理工卷;2008年03期

4 桑林瓊;王玉柱;;具有零知識特性的身份認(rèn)證方案設(shè)計及分析[J];重慶科技學(xué)院學(xué)報(自然科學(xué)版);2008年04期

5 胡焰智;馬大瑋;田增山;;一種基于移動公網(wǎng)的安全專網(wǎng)認(rèn)證與密鑰協(xié)商方案[J];電訊技術(shù);2008年03期

6 葛瑋;謝堅;劉斌;;基于終端的計算機(jī)網(wǎng)絡(luò)防御體系技術(shù)小析[J];江西電力職業(yè)技術(shù)學(xué)院學(xué)報;2011年01期

7 余磊;顧維娜;王猛;;基于串空間極小元理論的改進(jìn)Woo-Lam協(xié)議的認(rèn)證性分析[J];電腦編程技巧與維護(hù);2010年04期

8 楊杰;;基于串空間理論的kerberos協(xié)議的安全性分析[J];電腦編程技巧與維護(hù);2010年04期

9 劉慧芳;;基于串空間模型的Andrew安全RPC協(xié)議分析[J];電腦編程技巧與維護(hù);2012年04期

10 曹進(jìn);;計算機(jī)協(xié)議安全漏洞及其防護(hù)[J];電腦知識與技術(shù);2006年26期

相關(guān)會議論文 前8條

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

2 胡遠(yuǎn)鋒;;數(shù)字簽名原理淺析及其在網(wǎng)上銀行的應(yīng)用[A];2007北京地區(qū)高校研究生學(xué)術(shù)交流會通信與信息技術(shù)會議論文集（上冊）[C];2008年

3 徐天嶺;王景中;袁開國;楊義先;;基于USB-KEY的P2P保密通信研究與實現(xiàn)[A];中國電子學(xué)會第十五屆信息論學(xué)術(shù)年會暨第一屆全國網(wǎng)絡(luò)編碼學(xué)術(shù)年會論文集（上冊）[C];2008年

4 王遠(yuǎn)敏;汪學(xué)明;;一種改進(jìn)的含離線可信第三方多方不可否認(rèn)協(xié)議[A];邏輯學(xué)及其應(yīng)用研究——第四屆全國邏輯系統(tǒng)、智能科學(xué)與信息科學(xué)學(xué)術(shù)會議論文集[C];2008年

5 王斌君;韋楊;鞏榮;;B/S環(huán)境下反網(wǎng)絡(luò)釣魚雙向身份鑒別系統(tǒng)的設(shè)計與實現(xiàn)[A];全國計算機(jī)安全學(xué)術(shù)交流會論文集·第二十五卷[C];2010年

6 王聰;王智學(xué);;基于UML2.0的安全協(xié)議建模方法[A];江蘇省系統(tǒng)工程學(xué)會第十一屆學(xué)術(shù)年會論文集[C];2009年

7 徐夢茗;李斌;肖聰;;怎樣用好AVISPA工具[A];第十一屆保密通信與信息安全現(xiàn)狀研討會論文集[C];2009年

8 賀琦;魯昌華;侯鋒平;;基于指紋識別與數(shù)字簽名的身份認(rèn)證系統(tǒng)設(shè)計[A];計算機(jī)技術(shù)與應(yīng)用進(jìn)展·2007——全國第18屆計算機(jī)技術(shù)與應(yīng)用（CACIS）學(xué)術(shù)會議論文集[C];2007年

相關(guān)博士學(xué)位論文 前10條

1 楊元原;密碼協(xié)議的安全性分析技術(shù)研究[D];西安電子科技大學(xué);2011年

2 李向東;公平交換協(xié)議的形式化分析與設(shè)計[D];解放軍信息工程大學(xué);2009年

3 王惠斌;安全認(rèn)證協(xié)議的設(shè)計與分析[D];解放軍信息工程大學(xué);2010年

4 陳莉;電子商務(wù)安全協(xié)議的設(shè)計與分析[D];解放軍信息工程大學(xué);2009年

5 劉益和;應(yīng)用區(qū)域邊界安全體系結(jié)構(gòu)的模型研究[D];四川大學(xué);2005年

6 肖迪;混沌理論在數(shù)字產(chǎn)品安全中的應(yīng)用研究[D];重慶大學(xué);2005年

7 王英龍;Ad Hoc網(wǎng)絡(luò)路由協(xié)議安全性分析方法研究[D];山東大學(xué);2005年

8 邢育紅;公平交換協(xié)議分析方法研究[D];山東大學(xué);2005年

9 王強(qiáng)華;基于公共信道信令模型的網(wǎng)格體系結(jié)構(gòu)研究[D];西北大學(xué);2006年

10 繆祥華;一種分析和設(shè)計安全協(xié)議的新邏輯[D];西南交通大學(xué);2006年

相關(guān)碩士學(xué)位論文 前10條

1 毋曉英;基于串空間模型的安全協(xié)議分析與驗證方法的研究[D];鄭州大學(xué);2010年

2 余磊;基于串空間模型的安全協(xié)議分析方法研究[D];淮北師范大學(xué);2010年

3 程瑩;網(wǎng)絡(luò)安全協(xié)議的模型檢測分析及驗證系統(tǒng)[D];南昌大學(xué);2010年

4 李長軍;企業(yè)級復(fù)合式數(shù)據(jù)保護(hù)系統(tǒng)關(guān)鍵技術(shù)的研究[D];電子科技大學(xué);2010年

5 魯文靜;異構(gòu)無線融合網(wǎng)絡(luò)中通用接入認(rèn)證協(xié)議研究[D];解放軍信息工程大學(xué);2009年

6 馬松;不可否認(rèn)機(jī)制與時間戳服務(wù)系統(tǒng)研究[D];西安電子科技大學(xué);2009年

7 尚艷萍;RIPC中數(shù)據(jù)壓縮與安全通信技術(shù)的研究與實現(xiàn)[D];西安電子科技大學(xué);2010年

8 姬國珍;基于Maude的安全協(xié)議的形式化分析[D];西安電子科技大學(xué);2011年

9 秦好磊;基于樹自動推理的安全協(xié)議自動化檢測[D];西安電子科技大學(xué);2011年

10 盧衛(wèi)雄;基于IPSec的VPN網(wǎng)絡(luò)及其SA實現(xiàn)的研究[D];北方工業(yè)大學(xué);2011年

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

1 余冬梅,邊培泉,馮濤;安全協(xié)議中的形式化驗證技術(shù)[J];微機(jī)發(fā)展;2003年11期

2 王憶;;基于面向特征編程范式的形式化驗證技術(shù)的應(yīng)用與研究[J];信息與電腦(理論版);2011年01期

3 楊澤民;范全潤;;硬件設(shè)計的形式化驗證技術(shù)[J];太原師范學(xué)院學(xué)報(自然科學(xué)版);2007年02期

4 葉俊;譚慶平;李暾;;面向特征編程范式的形式化驗證技術(shù)研究綜述[J];計算機(jī)工程與科學(xué);2010年09期

5 周宏斌,黃連生,桑田;基于串空間的安全協(xié)議形式化驗證模型及算法[J];計算機(jī)研究與發(fā)展;2003年02期

6 韓俊剛;硬件設(shè)計的形式化驗證[J];計算機(jī)研究與發(fā)展;1991年11期

7 王彥本;;集成電路形式化驗證方法研究[J];電子科技;2008年08期

8 張慧;鄭超美;;安全協(xié)議的形式化驗證方法概述[J];計算機(jī)安全;2007年01期

9 黃連生,王新兵,謝峰,楊克;安全協(xié)議形式化驗證方法的比較與分析[J];計算機(jī)工程與應(yīng)用;2001年14期

10 張博穎;;優(yōu)先級頂協(xié)議的形式化驗證[J];計算機(jī)仿真;2007年06期

相關(guān)會議論文 前2條

1 吳鈴鈴;周干民;何偉;高明倫;;IP軟核的形式化驗證[A];全國第十五屆計算機(jī)科學(xué)與技術(shù)應(yīng)用學(xué)術(shù)會議論文集[C];2003年

2 郭華;莊雷;;電子商務(wù)協(xié)議的形式化驗證方法及FR驗證實例[A];2005年全國理論計算機(jī)科學(xué)學(xué)術(shù)年會論文集[C];2005年

相關(guān)碩士學(xué)位論文 前8條

1 李小波;龍芯2號功能部件半形式化驗證方法的研究與實現(xiàn)[D];首都師范大學(xué);2006年

2 焦金良;基于多項式模型的高層次形式化驗證[D];哈爾濱工程大學(xué);2006年

3 張倩;基于可編程邏輯的硬件平臺的設(shè)計與形式化驗證[D];北京交通大學(xué);2009年

4 張金磊;形式化驗證技術(shù)在EDA軟件開發(fā)中的應(yīng)用[D];西安電子科技大學(xué);2011年

5 馬小龍;形式化驗證在Office安全中的應(yīng)用研究[D];中國人民解放軍信息工程大學(xué);2005年

6 張澤恩;基于GSTE中的符號仿真設(shè)計與實現(xiàn)[D];電子科技大學(xué);2012年

7 林立;基于高階邏輯系統(tǒng)HOL的數(shù)字硬件形式化驗證[D];西安電子科技大學(xué);2005年

8 譚力;基于情態(tài)演算的UML形式化驗證與OCL約束自動生成研究[D];華東師范大學(xué);2010年

，

本文編號：2538580