基于π-演算的Petri網和密碼協議的形式化分析.pdf

1、并發(fā)理論一直是計算機科學中最富有挑戰(zhàn)性的一個研究方向之一，至今，已發(fā)展出了各種并發(fā)理論的分支，如：Petri網、CCS(Communication and ConcurrenceSystem)、CSP(Communicating Sequential Processes)、π-演算(A Calculus of MobileProcesses)等等。如何建構一個統一的并發(fā)理論框架、特別是將Petri網與R．Milner的CCS、π-演算統

2、一起來，一直是不少學者所追求的目標。英國計算機科學家R．Milner在1993年獲得圖靈獎所發(fā)表的演講報告中就曾指出：“把代數并發(fā)性方面所做的工作與C．A．Petri在Petri網上早已取得的豐碩成果聯系起來，是一個非常有希望的發(fā)展線索。然而，由于它們的概念基礎并不完全吻合，所以還有困難。”關于Petri網與CCS間的研究已經有了許多很好的結果，但自Milner于九十年代初期提出兀．演算理論后，由于其自身的復雜性，把Petri網與π-演

3、算結合起來便顯得極為困難。目前，在這方面的工作僅有兩位學者進行過，并各自得到了不成熟的結果。我們?yōu)榇颂岢隽素＃W這一并發(fā)理論模型，并初步實現了將π-演算和Petri網統一到一個并發(fā)框架中的目標。 受密碼學的驅動，本文對π-網進行了重新構建，將其應用到了對密碼協議的形式化研究中，并形成到了密碼協議的π-網語言---EPD(Encryption ProtocolLanguage)語言。對密碼協議的形式化工作始于70年代末期，到目前為

4、止已經形成了多種研究途徑。它們所關注的是密碼協議的密鑰傳輸和鑒別性問題，要解決的核心問題是試圖能主動的發(fā)現協議的缺陷，并希望能在攻擊者對其實施攻擊之前就能找出協議的漏洞。但事實是，盡管人們利用了多種的手段，如代數的，邏輯的，微分的，Petri網的，等等，但直至今天，問題依舊，并沒有得到任何實質性的解決。EPL語言致力于該問題的研究。 本文的主要貢獻和創(chuàng)新點如下： 1)提出了一類新型的基于π-演算語義的模塊化的、具有代數演

5、算能力的π-網，π-網有機的將Petri網和π-演算統一到了一個并發(fā)模型框架上，在語義上實現了從π-演算到Petri網的自動翻譯，同時也解決了π-演算的分布式語義問題，從而為Petri網的研究提供了一個新的研究內容。 2)初步解決了英國計算機科學家R．Mliner在1993年提出來的公開問題。π-演算是CCS的擴展，它們都是從λ-演算和C.A．Hoare的CSP上發(fā)展出來的代數并發(fā)理論，CCS所能做的工作都能在兀．演算中得到完成

6、，因此π-網實際上起到了將R．Milner在代數并發(fā)理論上的全部工作與：Petri網有機的統一起來了。證明了在結構同余的條件下，π-演算是可以嵌入到π-網的子集中去，即：ψ(p) P<,N>，但在兀-網的強互模擬等價關系下，我們卻可以把ψ(p)和P<,N>二者看成是一致的，這一結論證實了π-網是Petri網和π-演算的有機結合體。 3)提出了密碼協議的π-網形式化模型，建立了密碼協議的EPL語言。EPL語言繼承了π-網的模塊化和

7、代數化的特點，通過引入項、buffer庫所和解密變遷等新的建模元素，在π-網中建立了密鑰管理和加密信息的傳輸機制，對密碼協議進行了形式化描述和分析。 4)利用EPL語言對密碼協議進行了實例分析，通過對Wide Mouth Frog協議和Needham-Schroeder協議的分析，不僅建立了相關協議的π-網模型，同時還建立了對協議的攻擊模型。 5)提出了密碼協議的觀測等價概念，建立了密碼協議的鑒別性和安全性的判別機制，為