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

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

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

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

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

【相似文獻】

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

9 段雷;可選運行框架的J2EE Web應用自動生成[D];山東大學;2005年

10 張震;基于Cactus的JSP頁面測試及代碼自動生成器[D];北京郵電大學;2008年

，

本文編號：878762