安全協(xié)議論文：安全協(xié)議形式化分析串空間模型認(rèn)證測(cè)試

1、真誠(chéng)為您提供優(yōu)質(zhì)參考資料，若有不當(dāng)之處，請(qǐng)指正。安全協(xié)議論文：安全協(xié)議 形式化分析 串空間模型 認(rèn)證測(cè)試【中文摘要】隨著網(wǎng)絡(luò)技術(shù)和信息技術(shù)的迅速發(fā)展,計(jì)算機(jī)網(wǎng)絡(luò)在諸多領(lǐng)域內(nèi)的應(yīng)用日益普及,然而由于其運(yùn)行環(huán)境具有開放性,使得計(jì)算機(jī)網(wǎng)絡(luò)在給人們帶來(lái)巨大便利的同時(shí),也產(chǎn)生一系列的安全問(wèn)題,因此如何確保網(wǎng)絡(luò)中信息的安全性成為亟待解決的問(wèn)題。安全協(xié)議又稱密碼協(xié)議,是以密碼學(xué)技術(shù)為基礎(chǔ),在不安全的公共網(wǎng)絡(luò)和分布式系統(tǒng)中提供各種安全服務(wù)的一種通信協(xié)議。由于安全協(xié)議的安全性是評(píng)價(jià)網(wǎng)絡(luò)好壞的一個(gè)重要指標(biāo),所以在安全協(xié)議投入使用之前,對(duì)其安全性分析就顯得尤為重要。至今,安全協(xié)議的形式化分析和自動(dòng)化檢測(cè)己成為分析和

2、研究安全協(xié)議領(lǐng)域的兩個(gè)重要方向,而研制可靠實(shí)用的安全協(xié)議自動(dòng)化分析工具也逐漸成為主流趨勢(shì)。本文以串空間理論為基礎(chǔ),通過(guò)對(duì)當(dāng)前存在的一些安全協(xié)議形式化方法和自動(dòng)化技術(shù)進(jìn)行比較分析,深入地研究了安全協(xié)議的自動(dòng)化分析方法。主要內(nèi)容包括：1)深入研究了安全協(xié)議的安全性質(zhì),針對(duì)當(dāng)前運(yùn)用比較廣泛的形式化分析方法串空間模型,通過(guò)研究構(gòu)造方法,重點(diǎn)介紹了NSL協(xié)議的分析過(guò)程；同時(shí),以SSM協(xié)議為例,探討了如何使用認(rèn)證測(cè)試驗(yàn)證協(xié)議的過(guò)程及設(shè)計(jì)原理。2)給出了一種基于串空間模型的安全協(xié)議自動(dòng)化驗(yàn)證方法。在該方法中,針對(duì)參與方不檢測(cè)某些消息的來(lái)源,只是將其作為消息的子項(xiàng)參與協(xié)議的運(yùn)行的問(wèn)題,通過(guò)構(gòu)造和合法串結(jié)構(gòu)相同

3、的攻擊者串的方式,給出了一種自動(dòng)化驗(yàn)證方法；它不僅能夠分析具有加密類型的攻擊缺陷的協(xié)議,還將可信方引入到協(xié)議的參與方,使之能夠分析具有重放類型攻擊缺陷的協(xié)議,整個(gè)過(guò)程無(wú)需人工干預(yù),直觀和高效。在文章的最后借助兩個(gè)實(shí)例,詳細(xì)說(shuō)明了該系統(tǒng)的驗(yàn)證過(guò)程,結(jié)果表明系統(tǒng)具有良好的性能?！居⑽恼縒ith the fast development of network communication and information technology, network has exised in various fields. And network security problem is increasi

4、ngly serious; whose reason is its circumstances is an open secret that can be easily modified, forged and replayed. So how to solve the network security problem has been the increasingly outstanding problem.Security protocol, called cryptographic protocol which seems especially important in safety a

5、nd reliability, is a protocol for various types of security service over an insecure network. Before it is put into use, taking the openness of environmet and the imperfection of structrue into account, the attacker may execute effective attacks with the aid of shortcomings, therefore it is importan

6、t for us to validate its correctness.So far, it has became a hotspot and important area in security protocols to give formal analysis and automatic detection, correspondingly, designing efficient and reliable tools for analyzing security protocols has been the dominant trend.Based on strand space mo

7、del, this paper makes a research on some kinds of formal analysis and automatic analysis in security protocols nowadays, especially focus on the analysis of security protocols using automatic mehod. Following are the main results of this paper:1) This paper makes a deep study on security protocols,

8、and focusing on the current formal analysis method boardly-strand space model, we mainly studies the analysis of NSL protocol process by whose construction method. At the same time, this paper also further studies the authentication process and puts forward the SSM protocol.2) This paper proposes a

9、new automatic analysis method based on strand space model.Aming at the problem that not checking the source of information and only accepting it as a subset, the paper proposes an automatic method, which supports the string matching through structure the strings of identical construction, and it not

10、 only can analyze the two-party protocols but also makes it use three-side indentication protocols.lastly; it illuminates the structure of the tool, and implements technology with the aid of two agreements. All the whole process has majour or theoretic value and wideranging application.【關(guān)鍵詞】安全協(xié)議 形式化

11、分析 串空間模型 認(rèn)證測(cè)試【英文關(guān)鍵詞】Security protocols formal analysis strand space model authentication test method【目錄】基于串空間模型的安全協(xié)議自動(dòng)化驗(yàn)證方法研究摘要4-5Abstract5-6目錄7-10圖表目錄10-111 緒論11-161.1 概述11-141.1.1 研究背景和意義11-121.1.2 國(guó)內(nèi)外研究現(xiàn)狀12-141.2 研究?jī)?nèi)容及章節(jié)安排14-161.2.1 論文研究?jī)?nèi)容141.2.2 論文解決的問(wèn)題14-151.2.3 章節(jié)安排15-162 安全協(xié)議分析的基礎(chǔ)和理論16-302.1

12、安全協(xié)議16-192.1.1 安全協(xié)議的基本理論16-172.1.2 安全協(xié)議的安全屬性17-182.1.3 安全協(xié)議所面臨的安全威脅18-192.2 密碼學(xué)的基礎(chǔ)19-232.2.1 密碼學(xué)的分類20-212.2.2 密碼學(xué)的應(yīng)用21-232.3 串空間模型(Strand Space Model)23-272.3.1 串空間模型的基本理論232.3.2 串空間模型的基本概念23-272.4 串空間模型的應(yīng)用27-292.4.1 串空間模型中正確性概念27-282.4.2 串空間模型的應(yīng)用28-292.5 本章小結(jié)29-303 認(rèn)證測(cè)試及其應(yīng)用30-343.1 認(rèn)證測(cè)試30-323.1.1 認(rèn)證測(cè)試的概念31-323.2 SSM協(xié)議分析32-333.2.1 串空間模型323.2.2 認(rèn)證性分析32-333.3 本章小結(jié)33-344 安全協(xié)議自動(dòng)化分析技術(shù)34-434.1 協(xié)議自動(dòng)化分析簡(jiǎn)介34-354.2 協(xié)議自動(dòng)化分析技術(shù)35-424.2.1 模型框架35-384.2.2 算法描述38-424.3 本章小結(jié)42-435 系統(tǒng)設(shè)計(jì)與驗(yàn)證43-535.1 系統(tǒng)設(shè)計(jì)43-475.1.1 核心數(shù)據(jù)結(jié)構(gòu)設(shè)計(jì)43-445.1.2 核心模塊設(shè)計(jì)44-475.2 實(shí)例測(cè)試47-525.2.1 問(wèn)題描述475.2.2 串空間模型47-485.2.3 實(shí)例驗(yàn)證48-515.2.4 結(jié)果分析