資源描述：
《基于π演算的petri網(wǎng)和密碼協(xié)議的形式化分析》由會(huì)員上傳分享，免費(fèi)在線閱讀，更多相關(guān)內(nèi)容在學(xué)術(shù)論文-天天文庫。
1、上海交通大學(xué)博士學(xué)位論文摘要并發(fā)理論一直是計(jì)算機(jī)科學(xué)中最富有挑戰(zhàn)性的一個(gè)研究方向之一，至今，已發(fā)展出了各種并發(fā)理論的分支，如：Petri網(wǎng)、CCS(CommunicationandConcurrenceSystem)、CSP(CommunicatingSequentialProcesses)、耳·演算(ACalculusofMobileProcesses)等等。如何建構(gòu)一個(gè)統(tǒng)一的并發(fā)理論框架、特別是將Petri網(wǎng)與ILMilner的CCS、艫演算統(tǒng)一起來，一直是不少學(xué)者所追求的目標(biāo)。英國計(jì)算機(jī)科學(xué)家R．Miln盯在1993年獲得圖靈獎(jiǎng)所發(fā)表的演講報(bào)告中就曾指出
2、：“把代數(shù)并發(fā)性方面所做的工作與C．A．Pe啊在Pe研網(wǎng)上早已取得的豐碩成果聯(lián)系起來，是一個(gè)非常有希望的發(fā)展線索。然而，由于它們的概念基礎(chǔ)并不完全吻合。所以還有困難?！标P(guān)于Petri網(wǎng)與CCS問的研究已經(jīng)有了許多很好的結(jié)果。但自Milner于九十年代初期提出伽演算理論后，由于其自身的復(fù)雜性，把Petri網(wǎng)與和演算結(jié)合起來便顯得極為困難．目前，在這方面的工作僅有兩位學(xué)者進(jìn)行過，并各自得到了不成熟的結(jié)果．我們?yōu)榇颂岢隽似A網(wǎng)這一并發(fā)理論模型，并初步實(shí)現(xiàn)了將肛演算和Petri網(wǎng)統(tǒng)一到一個(gè)并發(fā)框架中的目標(biāo)．受密碼學(xué)的驅(qū)動(dòng)，我們對(duì)m網(wǎng)進(jìn)行了重新構(gòu)建，將其應(yīng)用到了對(duì)密碼協(xié)議
3、的形式化研究中，并形成到了密碼協(xié)議的舡網(wǎng)語言一一--EPL(EncryptionProtocolLanguage)語言。對(duì)密碼協(xié)議的形式化工作始于70年代末期，到目前為止已經(jīng)形成了多種研究途徑．它們所關(guān)注的是密碼協(xié)議的密鑰傳輸和鑒別性問題，要解決的核心問題是試圖能主動(dòng)的發(fā)現(xiàn)協(xié)議的缺陷，并希望能在攻擊者對(duì)其實(shí)施攻擊之前就能找出協(xié)議的漏洞。但事實(shí)是，盡管人們利用了多種的手段，如代數(shù)的，邏輯的，微分的，PeUi網(wǎng)的，等等，但直至今天，問題依舊，并沒有得到任何實(shí)質(zhì)性的解決．EPL語言致力于該問題的研究．本文的主要貢獻(xiàn)和創(chuàng)新點(diǎn)如下：1)提出了一類新型的基于小演算語義的模
4、塊化的、具有代數(shù)演算能力的哥阿，昏網(wǎng)有機(jī)的將Petri網(wǎng)和哥演算統(tǒng)一到了一個(gè)并發(fā)模型框架上，在語義上實(shí)現(xiàn)了從加演算到Petri同的自動(dòng)翻譯，同時(shí)也解決了伽演算的分布式語義悶題，從而為Petri網(wǎng)的研究提供了一個(gè)新的研究?jī)?nèi)容．上海交適大學(xué)博士學(xué)位論文2)初步解決了英國計(jì)算機(jī)科學(xué)家R．Mliner在1993年提出來的公開問題。m演算是CCS的擴(kuò)展。它們都是從九·演算和C．A．Hoare的CSP上發(fā)展出來的代數(shù)并發(fā)理論，CCS所能做的工作都能在靜演算中得到完成，因此加網(wǎng)實(shí)際上起到了將R．Milner在代數(shù)并發(fā)理論上的全部工作與Petri網(wǎng)有機(jī)的統(tǒng)一起來了。證明了在結(jié)
5、構(gòu)同余的條件下，肚演算是可以嵌入到兀·網(wǎng)的子集中去，即：甲伊)眇Ⅳ’但在伽網(wǎng)的強(qiáng)互模擬等價(jià)關(guān)系下，我們卻可以把ll，(乃和尹。這二者看成是一致的，這一結(jié)論證實(shí)了m網(wǎng)是Petri網(wǎng)和舡演算的有機(jī)結(jié)合體．3)提出了密碼協(xié)議的小網(wǎng)形式化模型，建立了密碼協(xié)議的EPL語言．EPL語言繼承了弘網(wǎng)的模塊化和代數(shù)化的特點(diǎn)，通過引入項(xiàng)、buffer庫所和解密變遷等新的建模元素，在卅網(wǎng)中建立了密鑰管理和加密信息的傳輸機(jī)制，對(duì)密碼協(xié)議進(jìn)行了形式化描述和分析．∞利用EPL語言對(duì)密碼協(xié)議進(jìn)行了實(shí)例分析，通過對(duì)晰dcMouthFrog協(xié)議和Needham-Schroeder協(xié)議的分析，不
6、僅建立了相關(guān)協(xié)議的靠．網(wǎng)模型，同時(shí)還建立了對(duì)協(xié)議的攻擊模型．·51提出了密碼協(xié)議的觀測(cè)等價(jià)概念，建立了密碼協(xié)議的鑒別性和安全性的判別機(jī)制，為密碼協(xié)議的,t-I碉形式化研究提供了一種研究方法和途徑．關(guān)鍵詞，Petri網(wǎng)，舡演算，靜網(wǎng)，標(biāo)號(hào)語義操作規(guī)則。強(qiáng)互模擬，密碼協(xié)議。鑒別，安全，觀測(cè)等價(jià)．n上海交遁大學(xué)博士學(xué)位論文A自噶臼aet’n彤r,oncurrcneytheoryisthemost,'hallenge印bjectineOmlmtet鰣e懈．There111"emanyresearchbranches，suchasPetrinet,CCS，CSP，n-c
7、alleulus，ete．Inlasty鋤，peopleaimtoeonslitutcauniformframeworkforconcurrencytheory,卸dspecially10finda丘鋤Fw伽lkbetweenJ'etrinetandCC$．Nowaplentyofattemptshavebeennlltdoinordertounderstandtherelationshipsbetwl期rltlaeseeoneurrerleytheories．ButsincelLMilnerproposedthe7t-r．a(chǎn)leul哪in1990’s，iti
8、smostdittieulttofin
