基于π-演算的Petri網(wǎng)和密碼協(xié)議的形式化分析.pdf

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

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

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

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

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

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

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