本文選題：安全協(xié)議　切入點(diǎn)：形式化分析　出處：《解放軍信息工程大學(xué)》2014年碩士論文　論文類(lèi)型：學(xué)位論文

【摘要】：安全協(xié)議是借助于密碼學(xué)技術(shù)在不安全的公共網(wǎng)絡(luò)上提供安全服務(wù)的通信協(xié)議,其正確性和安全性對(duì)于保障網(wǎng)絡(luò)信息安全而言有至關(guān)重要的作用。然而安全協(xié)議的設(shè)計(jì)是一項(xiàng)極其復(fù)雜的系統(tǒng)工程,即使在完美密碼假設(shè)的前提下,安全協(xié)議仍然可能存在嚴(yán)重漏洞或缺陷,因此在安全協(xié)議被廣泛應(yīng)用之前,必須對(duì)其正確性與安全性進(jìn)行全面深入的分析與檢測(cè)。形式化分析方法能夠有效的檢驗(yàn)安全協(xié)議的正確性與安全性,被公認(rèn)為輔助安全協(xié)議設(shè)計(jì)與分析的有效方法,安全協(xié)議的自動(dòng)化檢測(cè)和形式化分析相關(guān)技術(shù)的研究已成為信息安全領(lǐng)域極其重要的研究方向,具有重要的理論意義和現(xiàn)實(shí)應(yīng)用價(jià)值。本文在對(duì)現(xiàn)有安全協(xié)議形式化分析方法研究和分析的基礎(chǔ)上,提出了一種新的基于布爾可滿足性問(wèn)題的安全協(xié)議模型檢測(cè)方法,并利用該方法對(duì)實(shí)際網(wǎng)絡(luò)環(huán)境中運(yùn)行的安全協(xié)議進(jìn)行安全性分析。詳細(xì)工作總結(jié)如下:1.提出了基于布爾可滿足性的安全協(xié)議形式化分析方法SAT-LMC。SAT-LMC引入?yún)f(xié)議初始狀態(tài)惰性描述方法,通過(guò)變量保持以及協(xié)議參與方能力混淆等優(yōu)化方法,使協(xié)議分析的初始狀態(tài)大大減少,與傳統(tǒng)協(xié)議分析工具相比效率得到很大提升;在協(xié)議重寫(xiě)規(guī)則中添加了類(lèi)型缺陷攻擊、并行會(huì)話攻擊等多種攻擊類(lèi)型的檢測(cè)支持,并通過(guò)重寫(xiě)規(guī)則的變量保持以及惰性的攻擊者技術(shù)得到惰性的協(xié)議重寫(xiě)規(guī)則,效率進(jìn)一步得到提升,攻擊檢測(cè)更加全面;采用項(xiàng)重寫(xiě)技術(shù)將協(xié)議的形式化描述轉(zhuǎn)換為協(xié)議不安全問(wèn)題,通過(guò)智能規(guī)劃技術(shù)對(duì)其進(jìn)行圖形編碼,最終轉(zhuǎn)換為求解一個(gè)布爾可滿足性問(wèn)題;最后,針對(duì)現(xiàn)有的求解布爾可滿足性問(wèn)題的完備搜索算法和局部搜索算法的不足,設(shè)計(jì)了一種基于中間解加速的啟發(fā)式復(fù)合算法IS-CSAT,該算法通過(guò)對(duì)兩種算法的結(jié)合,在保持了完備搜索算法完備性的同時(shí),對(duì)大部分實(shí)例具備了局部搜索算法高效性的特點(diǎn)。2.以SAT-LMC協(xié)議分析方法為基礎(chǔ),實(shí)現(xiàn)了安全協(xié)議分析工具SAT-LMC Tool。該工具中的可滿足性問(wèn)題復(fù)合求解算法集成了傳統(tǒng)局部搜索算法的高效以及傳統(tǒng)全局搜索算法的求全解和證偽的優(yōu)點(diǎn);與傳統(tǒng)協(xié)議形式化分析工具OFMC以及SATMC比較,SAT-LMC Tool的分析速度更快,檢測(cè)效率更高,同時(shí)具備對(duì)類(lèi)型缺陷攻擊以及并行會(huì)話攻擊的檢測(cè)能力,攻擊檢測(cè)范圍更全面。3.利用安全協(xié)議分析工具SAT-LMC Tool,分析了云上開(kāi)放授權(quán)協(xié)議OAuth2.0的安全性。對(duì)其在安全信道四種使用情景下的安全性分別進(jìn)行分析,對(duì)可能存在的攻擊給出了相應(yīng)的攻擊路徑;另外,基于工具所給出的攻擊路徑,實(shí)現(xiàn)了針對(duì)新浪微博和優(yōu)酷網(wǎng)的用戶(hù)賬號(hào)劫持攻擊,上述實(shí)驗(yàn)結(jié)果表明,SAT-LMC Tool的設(shè)計(jì)與應(yīng)用對(duì)于對(duì)規(guī)范網(wǎng)絡(luò)安全環(huán)境有重要的作用和意義。
[Abstract]:Security protocol is a communication protocol that provides secure services on an insecure public network by means of cryptography. Its correctness and security play an important role in ensuring network information security. However, the design of security protocols is an extremely complex system engineering, even under the premise of perfect cryptographic assumption. Security protocols can still have serious vulnerabilities or flaws, so before they are widely used, Formal analysis method can effectively verify the correctness and security of security protocols, and is recognized as an effective method to assist the design and analysis of security protocols. The research of automatic detection and formal analysis of security protocols has become a very important research direction in the field of information security. Based on the research and analysis of the existing formal analysis methods of security protocols, a new security protocol model detection method based on Boolean satisfiability problem is proposed in this paper. The detailed work is summarized as follows: 1. A formal analysis method for security protocols based on Boolean satisfiability is proposed. SAT-LMC.SAT-LMC introduces the protocol initial state inertia description method. The initial state of protocol analysis is greatly reduced and the efficiency is greatly improved compared with the traditional protocol analysis tools, and the type defect attack is added to the protocol rewriting rules. Parallel session attacks and other attack types of detection support, and through overwriting rules of variable retention and lazy attacker technology to obtain lazy protocol rewriting rules, the efficiency is further improved, attack detection is more comprehensive; The formal description of the protocol is transformed into a protocol insecurity problem by item rewriting technology. Finally, the formal description of the protocol is transformed into a Boolean satisfiability problem by the graphic coding of the protocol through intelligent planning technology. Finally, a Boolean satisfiability problem is solved. Aiming at the shortcomings of the existing complete search algorithm and local search algorithm for solving Boolean satisfiability problem, a heuristic compound algorithm is designed based on intermediate solution acceleration, which combines the two algorithms. While maintaining the completeness of the complete search algorithm, it has the characteristic of high efficiency of the local search algorithm for most examples. 2. Based on the SAT-LMC protocol analysis method, A security protocol analysis tool, SAT-LMC Toolkit, is implemented, which integrates the advantages of the traditional local search algorithm and the global search algorithm. Compared with OFMC and SATMC, SAT-LMC Tool has faster analysis speed and higher detection efficiency. It also has the ability to detect type defect attacks and parallel session attacks. The security of Open Authorization Protocol (OAuth2.0) on the cloud is analyzed by using the security protocol analysis tool SAT-LMC tools. In addition, based on the attack path given by the tool, the hijacking attack against user accounts of Sina Weibo and Youku net is realized. The experimental results show that the design and application of SAT-LMC Tool play an important role in standardizing the network security environment.
【學(xué)位授予單位】：解放軍信息工程大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2014
【分類(lèi)號(hào)】：TN918.4

【參考文獻(xiàn)】

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

1 呂帥;劉磊;魏唯;高冰冰;;智能規(guī)劃的邏輯編碼方式研究[J];計(jì)算機(jī)研究與發(fā)展;2012年03期

2 呂帥;劉磊;石蓮;魏唯;楊超;;依賴(lài)公理約簡(jiǎn)的經(jīng)典規(guī)劃方法[J];電子學(xué)報(bào);2011年02期

3 楊晉吉;蘇開(kāi)樂(lè);肖茵茵;李超明;;有界模型檢測(cè)和串空間模型相結(jié)合的安全協(xié)議驗(yàn)證[J];小型微型計(jì)算機(jī)系統(tǒng);2010年08期

4 劉楠;朱文也;祝躍飛;陳晨;;基于樹(shù)語(yǔ)言逼近的安全協(xié)議形式化分析[J];計(jì)算機(jī)科學(xué);2010年01期

5 薛銳;馮登國(guó);;安全協(xié)議的形式化分析技術(shù)與方法[J];計(jì)算機(jī)學(xué)報(bào);2006年01期

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

1 武濤;基于增量式可滿足性求解的安全協(xié)議形式化驗(yàn)證方法[D];北京交通大學(xué);2009年

，

本文編號(hào)：1622250