基于Pi-演算的安全協(xié)議的形式化描述和驗(yàn)證論文

　　安全協(xié)議是以密碼學(xué)為基礎(chǔ)的消息交換協(xié)議，其目的是在網(wǎng)絡(luò)環(huán)境中提供各種安全服務(wù)。密碼學(xué)是網(wǎng)絡(luò)安全的基礎(chǔ)，但網(wǎng)絡(luò)安全不能單純依靠安全的密碼算法。安全協(xié)議是網(wǎng)絡(luò)安全的一個(gè)重要組成部分，我們需要通過(guò)安全協(xié)議進(jìn)行實(shí)體之間的認(rèn)證、在實(shí)體之間安全地分配密鑰或其它各種秘密、確認(rèn)發(fā)送和接收的消息的非否認(rèn)性等。以下是學(xué)習(xí)啦小編今天為大家精心準(zhǔn)備的：基于Pi-演算的安全協(xié)議的形式化描述和驗(yàn)證相關(guān)論文。內(nèi)容僅供閱讀與參考!

　　基于Pi-演算的安全協(xié)議的形式化描述和驗(yàn)證全文如下：

　　摘要：形式化論文范文方法對(duì)于建模和驗(yàn)證軟件系統(tǒng)是一種有效的方法，所以對(duì)安全協(xié)議的形式化描述和驗(yàn)證是一個(gè)重要的研究方向。Pi-演算是一種移動(dòng)進(jìn)程代數(shù)，可用于對(duì)并發(fā)和動(dòng)態(tài)變化的系統(tǒng)進(jìn)行建模;移動(dòng)工作臺(tái)MWB(Mobility Workbench)是為Pi-演算開(kāi)發(fā)的一個(gè)自動(dòng)驗(yàn)證工具，可對(duì)用Pi-演算等描述的移動(dòng)并發(fā)系統(tǒng)進(jìn)行分析與驗(yàn)證。本文基于Pi-演算對(duì)Aziz-Diffie無(wú)線通信安全協(xié)議進(jìn)行形式化分析并使用MWB工具驗(yàn)證此協(xié)議存在的攻擊。

　　關(guān)鍵詞：移動(dòng)進(jìn)程代數(shù);Pi-演算;移動(dòng)工作臺(tái)MWB;Aziz-Diffie;無(wú)線通信安全協(xié)議

　　本文首先扼要敘述了Pi-演算的基本概念，然后介紹了MWB工具在Windows下的使用并提出了基于Pi-演算協(xié)議分析的形式化方法，最后以Aziz-Diffie無(wú)線通信安全協(xié)議為例說(shuō)明了如何使用Pi-演算與MWB工具分析安全協(xié)議，找出協(xié)議攻擊。

　　1 Pi-演算

　　1.1 名字與進(jìn)程

　　設(shè)Χ = {x, y, z,a,b,c,…} 是名字(names)的可數(shù)集(可將名字看作是通信中的通道channels of communication)，?，??X，

　　定義 Pi演算的進(jìn)程(processes)如下(其中//…為幫助理解的直觀說(shuō)明)：

　　P:: = 0 //空進(jìn)程

　　P|Q //并發(fā)(并行)

　　P+Q //選擇

　　[x=y]P //匹配

　　?.P //沉默(Silent)前綴、內(nèi)部(Internal)前綴

　　x.P //輸出(Output)前綴

　　x(y).P //輸入(Input)前綴

　　νx.P //限制(Restriction)

　　A(x1, x2,…, xn) //代理(Agent)

　　A(x1, x2,…, xn)是被某P唯一定義的進(jìn)程(寫(xiě)為A(x1, x2,…, xn) =P，或A(x1, x2,…, xn) = P)，其中x1, x2,…, xn是彼此不同的名字且fn(P)?{x1, x2,…, xn}。

　　為減少刮號(hào)，約定下列作用順序：限制與前綴、并發(fā)、選擇;例如：νx.P|?.Q+R應(yīng)讀為((νx.P)|(?.Q))+R。

　　1.2 自由與約束的名字

　　設(shè)P、Q為進(jìn)程，歸納定義名字集合fn(P)如下：

　　稱(chēng) 為進(jìn)程P的自由名字集，若 ，稱(chēng)名字x在進(jìn)程P中是自由的;如果進(jìn)程P中的名字x不是自由名字，則稱(chēng)為約束名字，用 表示P的約束名字集，記 稱(chēng)nP為P的名字集;對(duì) ，將在P中自由出現(xiàn)的x稱(chēng)為被 約束的名字;注意，有P，使 ，即某個(gè)名字x可能同時(shí)在P中自由出現(xiàn)與約束出現(xiàn).

　　自由名字的代入：對(duì)任何進(jìn)程P，進(jìn)程P[z/x]是將P里每個(gè)自由出現(xiàn)的x改為z而得的進(jìn)程，稱(chēng)為在進(jìn)程P里對(duì)自由名字進(jìn)行代入。

　　約束名字的改名：(1)對(duì)進(jìn)程 的約束名字x可用z改名并將改名結(jié)果記為 ，如果 ;(2)對(duì)進(jìn)程 的約束名字x可用z改名并將改名結(jié)果記為 ，如果 ;

　　注意：對(duì) 改名的結(jié)果并不導(dǎo)致 或 里的任何名字的自由出現(xiàn)變?yōu)榧s束出現(xiàn);為防止改名失敗，可簡(jiǎn)單地使用新鮮名字來(lái)改名，

　　2 移動(dòng)工作臺(tái)MWB(Mobility Workbench)

　　2.1 移動(dòng)工作臺(tái)MWB(Mobility Workbench)

　　移動(dòng)工作臺(tái)MWB(Mobility Workbench)是針對(duì)Pi-演算開(kāi)發(fā)的第一個(gè)自動(dòng)驗(yàn)證工具[5]，可對(duì)用多子Pi-演算[2]描述的移動(dòng)并發(fā)系統(tǒng)進(jìn)行分析與驗(yàn)證;MWB首先在瑞典的Uppsala大學(xué)開(kāi)發(fā);可在Windows、Linux等系統(tǒng)下使用，MWB是開(kāi)放源代碼的。

　　2.2 PI-演算公式的MWB編碼

　　為將PI-演算公式輸入MWB，需將通常的PI-演算公式做一些轉(zhuǎn)換：

　　對(duì)于限制，用 代?;對(duì)于輸入前綴，可將 寫(xiě)為 ，稱(chēng) 為P的x的抽出(Abstraction)并用\代 ; 可寫(xiě)為 ，稱(chēng)[x]為P的x的凝固(Concretion)。

　　可用 來(lái)表示P為：agent = P

　　A稱(chēng)為P的名，注意P的名可用任意的符號(hào)串(例如MyID)，但第一個(gè)字母需大寫(xiě)，且(…)里一定要將P的非受限名字完全列舉;可將幾個(gè)MWB公式放到一塊以ag為擴(kuò)展名用ASCII文件存盤(pán)。

　　3 安全協(xié)議分析

　　3.1 進(jìn)程的性質(zhì)

　　一個(gè)進(jìn)程的行為就是這個(gè)進(jìn)程的執(zhí)行樹(shù)，一個(gè)進(jìn)程的性質(zhì)就是對(duì)這個(gè)進(jìn)程行為的斷言。對(duì)于順序程序來(lái)說(shuō)，它的性質(zhì)基本上分為兩種：程序中止或者程序執(zhí)行完成并得到結(jié)果;但對(duì)于并發(fā)進(jìn)程來(lái)說(shuō)，它除了有順序程序的性質(zhì)外，還有一些其他性質(zhì)，比如：程序是否死鎖，是否公平等等。

　　死鎖：進(jìn)程之間由于互相占用對(duì)方所需要的資源而都不能繼續(xù)執(zhí)行下去的現(xiàn)象，我們稱(chēng)之為死鎖

　　4總結(jié)

　　形式化方法對(duì)于建模和驗(yàn)證軟件系統(tǒng)是一種有效的方法，對(duì)安全協(xié)議的形式化描述和驗(yàn)證是一個(gè)重要的研究方向。本文使用Pi-演算對(duì)Aziz-Diffie無(wú)線通信安全協(xié)議分析并進(jìn)行建模，最后使用MWB工具證明出該協(xié)議存在攻擊，并給出了該協(xié)議存在的攻擊。

　　5 參考文獻(xiàn)：

　　[1] R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, partI/II. Journal of Information and Computation, 100:1-77, Sept. 1992.

　　[2] Robin Milner. The polyadic ?-calculus: A tutorial. Technical Report ECS-LFCS-91-180.

　　[3]Jens Chr.Godskesen. The Needham-Schroeder Public-Key Protocol—How to Break It:Version 1.0.IT University of Copenhagen March 10,2005.

　　[4] Bjorn Victor. The Mobility Workbench User's Guide: Polyadic version 3.122. Department of Information Technology, Uppsala University, 1995.

　　[5] Bjorn Victor. A Verification Tool for the Polyadic ?-Calculus. Licentiate thesis, Department of Computer Systems, Uppsala University, 1994. Available as report DoCS 94/50.

　　[6]張玉清，王春玲，馮登國(guó)，運(yùn)行模式法分析ISO/IEC密鑰建立協(xié)議，通信學(xué)報(bào)，2005年2月第26卷第2期，P15-18

　　[7]卿斯?jié)h，認(rèn)證協(xié)議兩種形式化分析方法的比較，軟件學(xué)報(bào)，2003年，第14卷第12期，P2028-2036

　　[8] Horng G, Hsu CK. Weakness in the Helsinki protocol. Electronic Letters, 1998,34:354~355.

　　[9] Mitchell CJ, Yeun CY. Fixing a problem in the Helsinki protocol. Operating Systems Review, 1998,32:21~24.

　　[10]卿斯?jié)h，安全協(xié)議，北京：清華大學(xué)出版社，2005年3月

　　[11]范紅，馮登國(guó)， 安全協(xié)議理論與方法，北京：科學(xué)出版社，2003年

　　[12]A.Aziz，W.Diffie.www.51lunwen.com/jsjaq/ A secure communications protocol to prevent unanthorized access:Privacy and authentication for wireless local area networks[J].IEEE Personal Communications,1994:25-31.

　　[13]D.Dolev and A.Yao. On the security of public key protocols. IEEE Trans.on Information and Theory,29(2):198-208,1983

　　[14]Fredrick B.Beste. The Model Prover-a sequent-calculus based modal μ-calculus model checker tool for finite control π-calculus agents, 1998,1,9,29-33

　　[15] 劉道斌，郭莉，白碩，基于petri 網(wǎng)的安全協(xié)議形式化分析,電子學(xué)報(bào)，2004年11月，P1926-1929