隨著無線傳感網(wǎng)領(lǐng)域和工業(yè)控制領(lǐng)域的不斷發(fā)展,網(wǎng)絡(luò)空間中的新興領(lǐng)域不斷產(chǎn)生,網(wǎng)絡(luò)通信機(jī)制也日益復(fù)雜。安全協(xié)議作為保障各類新興領(lǐng)域數(shù)據(jù)與服務(wù)資源的關(guān)鍵技術(shù)之一,近年來得到普遍關(guān)注。安全協(xié)議數(shù)量的激增,協(xié)議運行環(huán)境的差異,協(xié)議復(fù)雜度的提高,與設(shè)計分析人員主觀聯(lián)系密切等特點,導(dǎo)致安全協(xié)議的設(shè)計與分析成為極具挑戰(zhàn)性的課題。安全協(xié)議的形式化分析方法近年來取得了巨大進(jìn)步,在模態(tài)邏輯、定理證明以及模型檢測等幾大分支都具有頗具影響力的代表方法。與之相對應(yīng),基于計算模型的計算復(fù)雜性方法也在同步發(fā)展。該方法具有嚴(yán)謹(jǐn)?shù)臄?shù)學(xué)理論作為支撐,使用結(jié)構(gòu)復(fù)雜,對研究人員要求極高;此外,由于研究人員對協(xié)議的不同理解,在分析同種協(xié)議時,可能得到不同結(jié)果。與計算復(fù)雜性方法相比,基于符號模型的形式化分析方法由于自身的符號性和離散性,具有更簡單清晰的結(jié)構(gòu),在與分布式計算機(jī)工程領(lǐng)域相結(jié)合方面,具備天生優(yōu)勢。并且,隨著業(yè)界安全協(xié)議數(shù)量的規(guī)�；�,協(xié)議的自動化分析勢必成為協(xié)議安全性分析領(lǐng)域的重要趨勢。著色Petri網(wǎng)作為分布式異步并發(fā)系統(tǒng)分析中的最重要工具之一,具有二元性、圖形化以及代數(shù)表示性的特點,既有清晰的結(jié)構(gòu)又有嚴(yán)謹(jǐn)?shù)臄?shù)學(xué)基礎(chǔ);著... 

【文章來源】：西安電子科技大學(xué)陜西省 211工程院校 教育部直屬院校

【文章頁數(shù)】：89 頁

【學(xué)位級別】：碩士

【部分圖文】：

HelloWorld1模型圖，初始標(biāo)記0M

圖3.2 變遷激發(fā)示例圖，標(biāo)記1M 有向弧，用于連接庫所和變遷，并指示出變遷激發(fā)的條件，條件使用有向弧注入式（arc inscription）來表示，如示例圖中箭頭上的變量“s”即為一個有向弧表達(dá)式。因為有向弧不需要名字，只用來表示變遷需要和輸出的數(shù)據(jù)類型或嵌入其他 CPN ML語句，所以有向弧注入式又被稱為有向弧表達(dá)式（arc expression）。CPN 網(wǎng)絡(luò)中的有向弧可以是單向也可以是雙向，但是每個有向弧上表達(dá)式的類型必須是單一的。 由于 CPN 使用 ML 語言作為其內(nèi)部機(jī)制，故而，值和表達(dá)式以及遞歸構(gòu)成了語言的關(guān)鍵機(jī)制。在標(biāo)準(zhǔn)元語言 SML 中

圖3.3 結(jié)束狀態(tài)2 deadM（ M ） 在 CPN Tools 中，庫所內(nèi)令牌由系統(tǒng)初始標(biāo)記0M 到系統(tǒng)結(jié)束標(biāo)記2M 的流動過程，以及過程中變量綁定的變化，即為 CPN 模型 HelloWorld 的仿真。系統(tǒng)的仿真只能對模型進(jìn)行有限步的執(zhí)行，使用仿真可排除一些模型的與預(yù)設(shè)需求不相符的設(shè)計錯誤�？傮w來看，CPN 模型的運行遵循以下兩條規(guī)律： 1）當(dāng)庫所中的多重集能為弧表達(dá)式中的變量提供合適的綁定時，變遷被激發(fā)，相應(yīng)的多重集流入下一庫所，為下一變遷提供綁定。 2）在網(wǎng)絡(luò)模型中，變量的名字雖然不變，但隨著多重集在庫所中的流動，變量在不停地被重新綁定新的值。 在 CPN 的形式化定義中

【參考文獻(xiàn)】：
期刊論文
[1]EGAKA:一種面向LTE-A機(jī)器類型通信的高效組認(rèn)證與密鑰協(xié)商協(xié)議[J]. 宋亞鵬,陳昕.  計算機(jī)科學(xué). 2016(S1)
[2]一種基于CPN的協(xié)議測試序列生成方法[J]. 孫濤,葉新銘,劉靖,楊蒙.  解放軍理工大學(xué)學(xué)報(自然科學(xué)版). 2012(02)



本文編號：3251537