發(fā)布時(shí)間：2017-09-19 01:45

  本文關(guān)鍵詞：基于計(jì)算模型生成密碼學(xué)安全的安全協(xié)議代碼

  更多相關(guān)文章： 安全性 協(xié)議實(shí)現(xiàn)代碼 形式化分析 抽象模型 認(rèn)證性

【摘要】：目前安全協(xié)議的安全性仍是學(xué)術(shù)界關(guān)注的重點(diǎn),但是安全協(xié)議的安全性分析僅僅停留在對(duì)安全協(xié)議抽象分析和驗(yàn)證方面,很難應(yīng)用于日常研究中,而且在安全協(xié)議的代碼實(shí)現(xiàn)中難免會(huì)出現(xiàn)一些人為漏洞,這可能會(huì)給安全協(xié)議引入更大的漏洞。安全協(xié)議代碼的一般安全性(如數(shù)組下標(biāo)越界、內(nèi)存泄露、類型安全等),國內(nèi)外學(xué)者已經(jīng)做了很多有效的工作,但是關(guān)于安全協(xié)議實(shí)現(xiàn)代碼的研究人們做的工作很少,故本文重點(diǎn)關(guān)注安全協(xié)議代碼的密碼學(xué)安全性。安全協(xié)議的最主要的安全性分析方法有兩種,一種是構(gòu)造攻擊下的安全性分析,另外一種是模型形式化分析。本文基于安全協(xié)議的模型形式化分析方法,由代碼級(jí)出發(fā),進(jìn)而研究安全協(xié)議的安全性,也就是對(duì)安全協(xié)議代碼的安全性進(jìn)行研究,以得到具有更強(qiáng)實(shí)用性的安全協(xié)議代碼。針對(duì)這些問題,本文首先對(duì)概率標(biāo)號(hào)遷移系統(tǒng)進(jìn)行研究,探索提出安全協(xié)議代碼的密碼學(xué)安全性模型;其次探索應(yīng)用概率進(jìn)程演算:Blanchet演算建模安全協(xié)議抽象規(guī)范的方法,給出安全協(xié)議抽象規(guī)范建模的模版;以Blanchet演算建立的安全協(xié)議抽象規(guī)范模型為基礎(chǔ),研究代碼轉(zhuǎn)換的可行性,并建立與Java代碼之間的映射關(guān)系。本文探索從安全協(xié)議抽象規(guī)范模型生成安全協(xié)議Java代碼SP[Java]的方法。從進(jìn)程、角色、目標(biāo)多方面來建立Blanchet演算語言的映射模型,介紹轉(zhuǎn)換軟件的詞法分析器、語法分析器、簡(jiǎn)化器、模板器的工作原理來闡述軟件的開發(fā)過程。最后開發(fā)生成安全協(xié)議Java代碼的自動(dòng)化轉(zhuǎn)換軟件工具CV2JAVA。本文最后基于計(jì)算方法的自動(dòng)化證明工具Crypto Verif證明SSHV2協(xié)議的抽象模型具有認(rèn)證性,同時(shí)使用自動(dòng)轉(zhuǎn)換軟件CV2JAVA對(duì)SSHV2建立的Blanchet演算模型語言進(jìn)行轉(zhuǎn)換,生成SSHV2的規(guī)范流程Java核心代碼。SSHV2協(xié)議生成的核心代碼嵌入Java環(huán)境進(jìn)行驗(yàn)證分析,結(jié)果表明生成的安全協(xié)議代碼具有SSHV2協(xié)議定義的身份認(rèn)證性。
【關(guān)鍵詞】：安全性 協(xié)議實(shí)現(xiàn)代碼 形式化分析 抽象模型 認(rèn)證性
【學(xué)位授予單位】：中南民族大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2015
【分類號(hào)】：TP393.08
【目錄】：

• 摘要7-8
• Abstract8-10
• 第1章 緒論10-12
• 1.1 研究背景和意義10-11
• 1.2 國內(nèi)外研究現(xiàn)狀11
• 1.3 本文的組織結(jié)構(gòu)11-12
• 第2章 安全協(xié)議及代碼的安全性分析技術(shù)12-16
• 2.1 如何驗(yàn)證安全協(xié)議的安全12-13
• 2.2 安全協(xié)議代碼的形式化分析技術(shù)13-16
• 第3章 安全協(xié)議轉(zhuǎn)換原理16-25
• 3.1 Blanchet演算16-17
• 3.2 Java語言17-18
• 3.3 語言解析器18
• 3.4 安全協(xié)議代碼的驗(yàn)證安全的可實(shí)施性18-20
• 3.5 Java與Blanchet演算語言映射20-25
• 3.5.1 語言轉(zhuǎn)化21
• 3.5.2 類型轉(zhuǎn)換21-22
• 3.5.3 函數(shù)轉(zhuǎn)換22-23
• 3.5.4 秘密性聲明23
• 3.5.5 通道聲明23-24
• 3.5.6 安全屬性24
• 3.5.7 發(fā)送進(jìn)程和接收進(jìn)程24
• 3.5.8 主進(jìn)程24-25
• 第4章 自動(dòng)轉(zhuǎn)換軟件CV2JAVA開發(fā)過程25-38
• 4.1 Lexical analyzer詞法分析器的開發(fā)27-28
• 4.2 Parser解析器的開發(fā)28-29
• 4.3 Simplifier語法樹簡(jiǎn)化器29-31
• 4.4 Translator翻譯器開發(fā)31-35
• 4.5 Code generator代碼生成器的開發(fā)35-36
• 4.6 Template模板器的開發(fā)36-38
• 第5章自動(dòng)轉(zhuǎn)換軟件CV2JAVA結(jié)果驗(yàn)證38-45
• 總結(jié)45-46
• 參考文獻(xiàn)46-49
• 致謝49-50
• 附錄 攻讀學(xué)位所發(fā)表的學(xué)術(shù)論文目錄50

【相似文獻(xiàn)】

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

1 趙軍;;基于模板的代碼生成器的研究與實(shí)現(xiàn)[J];長春師范學(xué)院學(xué)報(bào);2011年12期

2 張仕仁;基于可重用代碼生成器設(shè)計(jì)與實(shí)現(xiàn)[J];山西大學(xué)學(xué)報(bào)(自然科學(xué)版);1993年03期

3 尤瀾濤;;基于數(shù)據(jù)表的代碼生成器的設(shè)計(jì)與實(shí)現(xiàn)[J];福建電腦;2013年10期

4 辛伯宇;;在RAD中實(shí)現(xiàn)代碼自動(dòng)生成[J];電腦開發(fā)與應(yīng)用;2008年12期

5 朱敏;蘇博;;利用VS中的宏實(shí)現(xiàn)VB.NET字段重構(gòu)[J];武漢船舶職業(yè)技術(shù)學(xué)院學(xué)報(bào);2006年02期

6 李榕;;基于多態(tài)變形的惡意代碼技術(shù)與檢測(cè)方法[J];中小企業(yè)管理與科技(下旬刊);2009年10期

7 萬軍民;基于Java的代碼生成器的設(shè)計(jì)與實(shí)現(xiàn)[J];計(jì)算機(jī)工程;2004年S1期

8 王忠杰;戰(zhàn)德臣;徐曉飛;楊美榮;程臻;;基于對(duì)象關(guān)聯(lián)模型的企業(yè)應(yīng)用軟件代碼生成器[J];計(jì)算機(jī)集成制造系統(tǒng);2007年05期

9 任佳麗;曹海燕;;嵌入式軟件自動(dòng)代碼生成和代碼整合方法研究[J];太原理工大學(xué)學(xué)報(bào);2013年04期

10 王毅;DSP/BIOS實(shí)現(xiàn)實(shí)時(shí)數(shù)據(jù)調(diào)試和交換[J];電子質(zhì)量;2001年05期

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

1 柳桐;;基于代碼再生成的Web系統(tǒng)架構(gòu)設(shè)計(jì)[A];中國電子學(xué)會(huì)第十七屆信息論學(xué)術(shù)年會(huì)論文集[C];2010年

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

1 吉林 飄零雪;妙手空空制炸彈[N];電腦報(bào);2002年

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

1 陳君;基于Sax的XML解析工具的設(shè)計(jì)與實(shí)現(xiàn)[D];中國科學(xué)院大學(xué)(工程管理與信息技術(shù)學(xué)院);2015年

2 楚龍輝;基于MDL的可視化代碼自動(dòng)生成框架的研究與應(yīng)用[D];電子科技大學(xué);2015年

3 馬杰;多核數(shù)字電路高層次綜合的研究與實(shí)現(xiàn)[D];電子科技大學(xué);2014年

4 李磊;C編譯器中間代碼生成及其后端的設(shè)計(jì)與實(shí)現(xiàn)[D];電子科技大學(xué);2016年

5 牛樂園;基于計(jì)算模型生成密碼學(xué)安全的安全協(xié)議代碼[D];中南民族大學(xué);2015年

6 柳桐;數(shù)據(jù)訪問代碼生成器的設(shè)計(jì)與實(shí)現(xiàn)[D];北京郵電大學(xué);2011年

7 彭仁夔;基于關(guān)系模型的代碼生成器的設(shè)計(jì)與實(shí)現(xiàn)[D];南昌大學(xué);2014年

8 溫衍博;基于模型驅(qū)動(dòng)的電子商務(wù)系統(tǒng)代碼生成器的研究與實(shí)現(xiàn)[D];國防科學(xué)技術(shù)大學(xué);2005年

9 段雷;可選運(yùn)行框架的J2EE Web應(yīng)用自動(dòng)生成[D];山東大學(xué);2005年

10 張震;基于Cactus的JSP頁面測(cè)試及代碼自動(dòng)生成器[D];北京郵電大學(xué);2008年

，

本文編號(hào)：878762