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

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

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

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

　　關鍵詞：移動進程代數(shù);Pi-演算;移動工作臺MWB;Aziz-Diffie;無線通信安全協(xié)議

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

　　1 Pi-演算

　　1.1 名字與進程

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

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

　　P:: = 0 //空進程

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

　　P+Q //選擇

　　[x=y]P //匹配

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

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

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

　　νx.P //限制(Restriction)

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

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

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

　　1.2 自由與約束的名字

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

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

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

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

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

　　2 移動工作臺MWB(Mobility Workbench)

　　2.1 移動工作臺MWB(Mobility Workbench)

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

　　2.2 PI-演算公式的MWB編碼

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

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

　　可用 來表示P為：agent = P

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

　　3 安全協(xié)議分析

　　3.1 進程的性質

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

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

　　4總結

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

　　5 參考文獻：

　　[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]張玉清，王春玲，馮登國，運行模式法分析ISO/IEC密鑰建立協(xié)議，通信學報，2005年2月第26卷第2期，P15-18

　　[7]卿斯?jié)h，認證協(xié)議兩種形式化分析方法的比較，軟件學報，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é)議，北京：清華大學出版社，2005年3月

　　[11]范紅，馮登國， 安全協(xié)議理論與方法，北京：科學出版社，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é)議形式化分析,電子學報，2004年11月，P1926-1929