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

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

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

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

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

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

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

　　1 Pi-演算

　　1.1 名字與進程

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

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

　　P:: = 0 //空進程

　　P|Q //并發(并行)

　　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}。

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

　　1.2 自由與約束的名字

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

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

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

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

　　注意：對 改名的結果并不導致 或 里的任何名字的自由出現變為約束出現;為防止改名失敗，可簡單地使用新鮮名字來改名，

　　2 移動工作臺MWB(Mobility Workbench)

　　2.1 移動工作臺MWB(Mobility Workbench)

　　移動工作臺MWB(Mobility Workbench)是針對Pi-演算開發的第一個自動驗證工具[5]，可對用多子Pi-演算[2]描述的移動并發系統進行分析與驗證;MWB首先在瑞典的Uppsala大學開發;可在Windows、Linux等系統下使用，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 安全協議分析

　　3.1 進程的性質

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

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

　　4總結

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

　　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密鑰建立協議，通信學報，2005年2月第26卷第2期，P15-18

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

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