本文關(guān)鍵詞：基于計(jì)算語(yǔ)義的安全協(xié)議驗(yàn)證邏輯　出處：《電子學(xué)報(bào)》2014年06期 　論文類型：期刊論文

  更多相關(guān)文章： 加密算法 安全性 形式邏輯 計(jì)算語(yǔ)義

【摘要】：提出了一個(gè)基于計(jì)算語(yǔ)義的安全協(xié)議驗(yàn)證邏輯,能準(zhǔn)確描述安全協(xié)議中的各種計(jì)算行為和通信行為.設(shè)計(jì)了基于該邏輯的證明系統(tǒng),能對(duì)密碼學(xué)中常用加密算法的各類安全屬性規(guī)范直接描述,具有密碼學(xué)可靠性.發(fā)現(xiàn)了計(jì)算協(xié)議組合邏輯在加密算法安全性建模時(shí)存在的不可靠性,并提出了解決方法.通過(guò)對(duì)Needham-Schroeder-Lowe協(xié)議安全性的證明,驗(yàn)證了邏輯的證明能力.與大部分驗(yàn)證方法不同的是,本邏輯屬于由密碼學(xué)算法安全性到協(xié)議安全性的正向推理方法,兼具符號(hào)方法的易用性和計(jì)算方法的可靠性.
[Abstract]:This paper presents a security protocol verification logic based on computational semantics , which can accurately describe various computing behaviors and communication behaviors in security protocols . The proof system based on the logic is designed . It can be directly described for various kinds of security attribute specifications of commonly used encryption algorithms in cryptography , and it has cryptographic reliability .

【作者單位】： 國(guó)防科技大學(xué)電子科學(xué)與工程學(xué)院;中國(guó)洛陽(yáng)電子裝備試驗(yàn)中心;
【基金】：國(guó)家自然科學(xué)基金(No.61301236,No.61303061)
【分類號(hào)】：TN918.4
【正文快照】： 1引言安全協(xié)議是一種特殊形式的分布式軟件,與其他形式的軟件相比,安全協(xié)議除了要保證正確性外,更需要保證安全性,即在任何輸入的情況下,協(xié)議都滿足安全規(guī)范.如何使用形式化方法對(duì)已有協(xié)議的安全性進(jìn)行準(zhǔn)確、高效的分析和驗(yàn)證成了國(guó)內(nèi)外相關(guān)領(lǐng)域的熱點(diǎn)研究問(wèn)題.經(jīng)過(guò)了近30年的

【參考文獻(xiàn)】

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

1 張暢;王亞弟;韓繼紅;郭淵博;;一種改進(jìn)的密碼協(xié)議形式化模型[J];軟件學(xué)報(bào);2007年07期

2 董玲;陳克非;來(lái)學(xué)嘉;;密碼協(xié)議分析的信任多集方法[J];軟件學(xué)報(bào);2009年11期

【共引文獻(xiàn)】

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

1 程正杰;陳克非;來(lái)學(xué)嘉;;基于細(xì)粒度新鮮性的密碼協(xié)議分析[J];北京大學(xué)學(xué)報(bào)(自然科學(xué)版);2010年05期

2 韓繼紅;范鈺丹;王亞弟;郭淵博;;一種基于語(yǔ)義的安全協(xié)議形式化模型[J];計(jì)算機(jī)科學(xué);2009年02期

3 陳晨;朱文也;陳衛(wèi)紅;劉楠;;一種對(duì)MSR模型的新擴(kuò)展[J];計(jì)算機(jī)工程;2010年08期

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

1 黃展;寬帶衛(wèi)星網(wǎng)絡(luò)安全協(xié)議研究[D];哈爾濱工業(yè)大學(xué);2009年

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

1 王恩俊;一種基于BAN類邏輯的安全協(xié)議分析方法及其自動(dòng)化實(shí)現(xiàn)[D];浙江大學(xué);2011年

2 陳晨;安全協(xié)議形式化模型刻畫與代數(shù)屬性研究[D];解放軍信息工程大學(xué);2010年

3 程正杰;基于細(xì)粒度新鮮性的密碼協(xié)議分析[D];上海交通大學(xué);2010年

【二級(jí)參考文獻(xiàn)】

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

1 季慶光,馮登國(guó);對(duì)幾類重要網(wǎng)絡(luò)安全協(xié)議形式模型的分析[J];計(jì)算機(jī)學(xué)報(bào);2005年07期

【相似文獻(xiàn)】

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

1 葉燕;數(shù)據(jù)安全傳輸及加密技術(shù)的研究[J];宜春學(xué)院學(xué)報(bào);2005年02期

2 石福斌;;移動(dòng)通信系統(tǒng)接入安全機(jī)制[J];哈爾濱理工大學(xué)學(xué)報(bào);2006年06期

3 賀金平;呂楊;;基于藍(lán)牙Ad hoc網(wǎng)絡(luò)安全機(jī)制的研究與加密設(shè)計(jì)[J];自動(dòng)化技術(shù)與應(yīng)用;2007年06期

4 張培;;淺談PKC體制及一種重要算法的實(shí)現(xiàn)[J];山西電子技術(shù);2007年05期

5 潘瑜;密碼體制及加密傳輸方式比較研究[J];常州信息職業(yè)技術(shù)學(xué)院學(xué)報(bào);2004年04期

6 劉自偉;羅燕琪;段琦;;加密算法與密鑰生成技術(shù)在數(shù)據(jù)庫(kù)加密中的應(yīng)用[J];計(jì)算機(jī)時(shí)代;2007年06期

7 孔雪蓮;;淺談無(wú)線局域網(wǎng)中的安全及黑客防范[J];電腦知識(shí)與技術(shù)(學(xué)術(shù)交流);2007年13期

8 謝慎波;;信息加密在網(wǎng)絡(luò)安全中的應(yīng)用[J];科技經(jīng)濟(jì)市場(chǎng);2007年09期

9 黃貴微;李小文;;安全模式控制過(guò)程在TD-SCDMA終端RRC子層的實(shí)現(xiàn)[J];通信技術(shù);2007年12期

10 陳偉;鮑慧;;IMS網(wǎng)絡(luò)拓?fù)潆[藏及其加密算法的研究[J];通信技術(shù);2008年03期

相關(guān)會(huì)議論文 前10條

1 孫樹峰;黃松;;基于混沌的無(wú)線安全技術(shù)[A];全國(guó)計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)論文集（第二十二卷）[C];2007年

2 張U，

本文編號(hào)：1421489