發(fā)布時間：2018-11-05 19:59

【摘要】：隨著互聯(lián)網(wǎng)技術(shù)的發(fā)展和普及,網(wǎng)絡(luò)環(huán)境正變得日益復(fù)雜。在開放的網(wǎng)絡(luò)中,如何確保通信安全是當(dāng)今—項(xiàng)重要的議題。以密碼技術(shù)為基礎(chǔ),網(wǎng)絡(luò)安全協(xié)議實(shí)現(xiàn)了開放網(wǎng)絡(luò)環(huán)境中的通信安全,它是網(wǎng)絡(luò)信息安全的基礎(chǔ)。由于安全協(xié)議的重要性,它本身設(shè)計(jì)的合理性和正確性已經(jīng)成為網(wǎng)絡(luò)安全研究的重要內(nèi)容。本文嘗試使用形式化方法Event-B在Rodin平臺上對安全套接層握手協(xié)議進(jìn)行了建模分析與驗(yàn)證。文中首先介紹了形式化方法的概念并概述了安全網(wǎng)絡(luò)協(xié)議及其性質(zhì)的相關(guān)內(nèi)容。然后對形式化方法Event-B及其工具Rodin進(jìn)行了簡要的介紹。其次,本文初步分析了安全套接層協(xié)議客棧的體系結(jié)構(gòu)、工作原理和安全機(jī)制,并著重探究了握手協(xié)議。隨后,試著提取了協(xié)議的需求說明,同時制定了模型精化策略,并在此基礎(chǔ)上對握手協(xié)議進(jìn)行了初步的建模分析。接著嘗試對公鑰真實(shí)性驗(yàn)證過程和有攻擊者參與的情況分別進(jìn)行了建模分析。最后借助Rodin平臺的自動證明和交互式證明機(jī)制試著對模型正確性進(jìn)行驗(yàn)證。本文的結(jié)果表明,采用Event-B方法對握手協(xié)議進(jìn)行分析和驗(yàn)證是比較有效的,模型精化過程對深入理解協(xié)議較為有利。在一定前提下協(xié)議具有認(rèn)證性和保密性,協(xié)議本身的機(jī)制能夠有效檢測出針對消息篡改類的攻擊行為。本文對SSL握手協(xié)議部分進(jìn)行了建模,未來可在本文基礎(chǔ)上完成對整個協(xié)議棧的分析。
[Abstract]:With the development and popularization of Internet technology, the network environment is becoming more and more complex. In an open network, how to ensure communication security is an important issue today. Based on cryptography, network security protocol realizes communication security in open network environment, which is the basis of network information security. Due to the importance of security protocol, the rationality and correctness of its own design has become an important content of network security research. This paper attempts to use the formal method Event-B to model and verify the secure socket layer handshake protocol on the Rodin platform. In this paper, the concept of formal method is introduced, and the contents of secure network protocol and its properties are summarized. Then the formal method Event-B and its tool Rodin are briefly introduced. Secondly, this paper analyzes the architecture, working principle and security mechanism of secure socket layer protocol inn, and probes into handshake protocol. Then, the requirements of the protocol are extracted, and the model refinement strategy is formulated. Based on this, a preliminary modeling analysis of the handshake protocol is carried out. Then we try to model and analyze the public key authenticity verification process and the situation in which the attacker is involved. Finally, with the help of the automatic proof and interactive certification mechanism of Rodin platform, we try to verify the correctness of the model. The results of this paper show that the analysis and verification of handshake protocol using Event-B method is more effective, and the process of model refinement is more beneficial to the in-depth understanding of the protocol. Under certain conditions, the protocol has authentication and confidentiality, and the mechanism of the protocol itself can effectively detect the attacks against message tampering classes. In this paper, the SSL handshake protocol is modeled and the whole stack can be analyzed in the future.
【學(xué)位授予單位】：浙江大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2017
【分類號】：TP393.08

【相似文獻(xiàn)】

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

1 王小軍;陸建德;;基于802.11i的四次握手協(xié)議的攻擊[J];計(jì)算機(jī)與現(xiàn)代化;2006年05期

2 王小軍;陸建德;;基于802.11i四次握手協(xié)議的攻擊分析與改進(jìn)[J];計(jì)算機(jī)工程;2007年03期

3 張妤;王喜發(fā);戴紫彬;;自計(jì)時電路中握手協(xié)議與延遲假定的研究[J];現(xiàn)代電子技術(shù);2007年24期

4 曹利;黃海斌;;基于802.11i的四次握手協(xié)議的攻擊分析[J];計(jì)算機(jī)工程;2009年10期

5 戴昱彤;樂大珩;李少青;張民選;;基于異步握手協(xié)議的功耗隨機(jī)技術(shù)實(shí)現(xiàn)[J];武漢理工大學(xué)學(xué)報;2009年18期

6 諶雙雙;陳澤茂;王浩;;一種高效的無線傳輸層安全握手協(xié)議[J];計(jì)算機(jī)工程;2011年16期

7 劉寧;;異地交易成功率機(jī)理探析[J];中國金融電腦;2009年01期

8 張鵬,李建,王坤;IPSec和SSL的分析和比較[J];信息工程大學(xué)學(xué)報;2002年01期

9 諶雙雙;陳澤茂;王浩;;基于身份的無線傳輸層安全握手協(xié)議改進(jìn)方案[J];計(jì)算機(jī)應(yīng)用;2011年11期

10 吳敏;梁爽;;實(shí)現(xiàn)SSL協(xié)議快速連接的一種解決方案[J];蘭州理工大學(xué)學(xué)報;2008年01期

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

1 丁瑤;于志強(qiáng);葉松;唐凌;吳淵;王杰斌;魯昱;;SSL握手協(xié)議的研究與擴(kuò)展[A];中國通信學(xué)會第六屆學(xué)術(shù)年會論文集（下）[C];2009年

2 戚帥;鄭康鋒;;一種改進(jìn)的基于無證書簽名的SSL握手協(xié)議[A];2011年全國通信安全學(xué)術(shù)會議論文集[C];2011年

3 曹慧娟;何大可;;基于SRP和基于SOKE的TLS握手協(xié)議的分析與比較[A];2006北京地區(qū)高校研究生學(xué)術(shù)交流會——通信與信息技術(shù)會議論文集（下）[C];2006年

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

1 何祝平;移動設(shè)備在無線局域網(wǎng)間快速切換算法研究[D];新疆大學(xué);2015年

2 史俊;基于Event-B的SSL握手協(xié)議建模分析與驗(yàn)證[D];浙江大學(xué);2017年

3 陶良升;基于對稱密鑰認(rèn)證的安全握手協(xié)議研究及應(yīng)用[D];華中科技大學(xué);2009年

4 劉勇;認(rèn)知無線網(wǎng)絡(luò)中的多信道握手協(xié)議研究[D];西安電子科技大學(xué);2014年

5 李根;IEEE 802.11標(biāo)準(zhǔn)四次握手協(xié)議安全性分析與改進(jìn)[D];天津大學(xué);2010年

6 戴昱彤;基于異步握手協(xié)議的抗DPA攻擊技術(shù)研究與實(shí)現(xiàn)[D];國防科學(xué)技術(shù)大學(xué);2009年

7 龔振;基于TPM的SSL VPN協(xié)議改進(jìn)[D];上海交通大學(xué);2009年

8 盛兆勇;IEC61850安全性分析及解決方案研究[D];中國海洋大學(xué);2013年

9 舒之兵;一種改進(jìn)的SSL握手協(xié)議及在VPN中的應(yīng)用[D];華中科技大學(xué);2006年

10 朱曉莉;基于端到端的WAP安全性研究[D];東北大學(xué);2012年

，

本文編號：2313227