本文關(guān)鍵詞： 安全協(xié)議 形式化分析 非對稱加密　出處：《中國科學(xué)院大學(xué)(中國科學(xué)院沈陽計算技術(shù)研究所)》2017年碩士論文　論文類型：學(xué)位論文

【摘要】：安全協(xié)議是當前復(fù)雜網(wǎng)絡(luò)環(huán)境下進行秘密信息交換的基礎(chǔ),其能否符合安全協(xié)議的安全屬性要求,對于保障網(wǎng)絡(luò)環(huán)境的健康極其重要。但是設(shè)計一個滿足安全屬性的安全協(xié)議十分不易,同時安全協(xié)議只有在經(jīng)過嚴格的形式化分析,確保其正確的前提下才能投入使用。正是因為以上因素,阻礙了安全協(xié)議的進一步實現(xiàn)和大規(guī)模化應(yīng)用。本文首先說明了網(wǎng)絡(luò)通信中安全協(xié)議的重要性,之后介紹了密碼學(xué)和安全協(xié)議制定過程中需要遵循的準則、常見的安全缺陷及其對應(yīng)的應(yīng)對措施等相關(guān)基礎(chǔ)理論,對當前流行的形式化分析方法模態(tài)邏輯BAN邏輯的分析原理及其分析中需要使用的公理進行了說明。其次對本文中改進的NSSK安全協(xié)議的原生協(xié)議進行了分析,指明了原生協(xié)議存在的缺陷和不足,以及在改進和優(yōu)化過程中所采取的防范措施,并通過優(yōu)化后的形式化分析方法BAN邏輯對該改進的NSSK安全協(xié)議進行了理論分析,證明該改進的NSSK安全協(xié)議在理論上滿足安全協(xié)議的安全屬性要求,為下一步該安全協(xié)議的應(yīng)用提供了理論依據(jù)。最后通過調(diào)用硬件TF加密卡提供的接口,在檢測客戶端環(huán)境參數(shù)、確認客戶端可以使用加解密服務(wù)的前提下,在業(yè)務(wù)邏輯中調(diào)用相應(yīng)的接口對改進的NSSK安全協(xié)議運行的各個步驟進行了實現(xiàn),使得相互通信的雙方在密鑰分發(fā)中心的參與下能夠得到共享會話密鑰,并使用該共享會話密鑰對文本、文件、語音、視頻、文件消息進行加解密;使用共享會話密鑰對IP電話中的媒體流進行加解密。之后,通過在商業(yè)軟件上的測試,證明了改進的NSSK安全協(xié)議可以滿足正常的商業(yè)需求,為該安全協(xié)議的進一步市場化提供依據(jù)。
[Abstract]:Security protocol is the basis of secret information exchange in the current complex network environment. It is very important to protect the health of the network environment. However, it is very difficult to design a security protocol that satisfies the security properties. At the same time, the security protocol can only be analyzed through strict formalization. It is precisely because of the above factors that the further realization and large-scale application of security protocols are hindered. This paper first explains the importance of security protocols in network communication. Then it introduces the relevant basic theories of cryptography and security protocol, such as the criteria to be followed, the common security defects and the corresponding countermeasures, and so on. In this paper, the analysis principle of modal logic BAN logic and the axioms that need to be used in the analysis are explained. Secondly, the native protocols of the improved NSSK security protocol in this paper are analyzed. The defects and shortcomings of the native protocol are pointed out, and the preventive measures taken in the process of improvement and optimization are pointed out. The improved NSSK security protocol is theoretically analyzed by the optimized formal analysis method BAN logic. It is proved that the improved NSSK security protocol meets the security attribute requirement of the security protocol theoretically, and provides the theoretical basis for the application of the security protocol in the next step. Finally, the interface provided by the hardware TF encryption card is called. On the premise of detecting the environment parameters of the client and confirming that the client can use the encryption and decryption service, the corresponding interface is called in the business logic to realize the steps of the improved NSSK security protocol. The shared session key can be obtained by the two parties communicating with each other with the participation of the key distribution center, and the text, file, voice, video and file messages are encrypted and decrypted using the shared session key; Using the shared session key to encrypt and decrypt the media stream in the IP phone. After testing on the commercial software, it is proved that the improved NSSK security protocol can meet the normal business needs. To provide the basis for the further marketization of the security agreement.
【學(xué)位授予單位】：中國科學(xué)院大學(xué)(中國科學(xué)院沈陽計算技術(shù)研究所)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2017
【分類號】：TP393.08

【相似文獻】

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

1 范紅,馮登國;安全協(xié)議形式化分析的研究現(xiàn)狀及有關(guān)問題[J];網(wǎng)絡(luò)安全技術(shù)與應(yīng)用;2001年08期

2 范紅,馮登國;安全協(xié)議形式化分析方法綜述之二——基于攻擊結(jié)構(gòu)性方法[J];網(wǎng)絡(luò)安全技術(shù)與應(yīng)用;2003年06期

3 郭宇燕;;安全協(xié)議的形式化分析方法初探[J];內(nèi)江科技;2007年11期

4 范紅,馮登國;一種混合的安全協(xié)議形式化分析技術(shù)[J];中國科學(xué)院研究生院學(xué)報;2002年03期

5 范紅,馮登國,鄒良惠;安全協(xié)議形式化分析方法綜述之一:基于推理結(jié)構(gòu)性方法[J];網(wǎng)絡(luò)安全技術(shù)與應(yīng)用;2003年05期

6 常亮;古天龍;;安全協(xié)議及其形式化分析研究[J];桂林電子工業(yè)學(xué)院學(xué)報;2006年04期

7 蔡永泉;朱勇;;一種改進的A(0)協(xié)議及其形式化分析[J];計算機工程與應(yīng)用;2006年34期

8 亓文華;張其善;劉建偉;;關(guān)于安全協(xié)議的形式化分析方法的研究[J];遙測遙控;2007年02期

9 文靜華;張梅;張煥國;;電子支付協(xié)議的博弈邏輯模型與形式化分析[J];微電子學(xué)與計算機;2007年09期

10 陸陽;肖軍模;劉晶;;一種新的安全協(xié)議形式化分析方法——證據(jù)邏輯[J];計算機工程;2008年02期

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

7 朱薏;數(shù)據(jù)庫管理系統(tǒng)安全性形式化分析研究[D];華中科技大學(xué);2014年

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

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

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

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

1 張玲玲;物聯(lián)網(wǎng)安全協(xié)議形式化分析與驗證[D];聊城大學(xué);2015年

2 王煥孝;基于SAT的安全協(xié)議形式化分析方法研究與應(yīng)用[D];解放軍信息工程大學(xué);2014年

3 常寅龍;電子商務(wù)協(xié)議的形式化分析與漏洞檢測[D];福州大學(xué);2013年

4 丁洪;公平交換協(xié)議的理性模型及其形式化分析[D];貴州大學(xué);2016年

5 趙治剛;融合通信中安全機制的設(shè)計與實現(xiàn)[D];中國科學(xué)院大學(xué)(中國科學(xué)院沈陽計算技術(shù)研究所);2017年

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

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

8 李軼，

本文編號：1517388