基于網(wǎng)絡(luò)協(xié)議的Petri網(wǎng)研究——利用著色Petri網(wǎng)分析驗(yàn)證安全協(xié)議.pdf

1、在因特網(wǎng)技術(shù)飛速發(fā)展的今天，信息安全問題已經(jīng)成為日益突出的問題。安全協(xié)議的出現(xiàn)雖然在很大程度上提高了網(wǎng)絡(luò)信息傳輸?shù)陌踩?，但同時(shí)因?yàn)樵O(shè)計(jì)上的缺陷性，安全協(xié)議也存在著很多漏洞。在當(dāng)前，安全協(xié)議的形式化分析已經(jīng)成了一個(gè)熱點(diǎn)研究問題。目前安全協(xié)議的形式化分析方法主要包括：形式邏輯方法、模型檢測(cè)方法、定理證明方法和Petri網(wǎng)方法，這些方法各有自己的優(yōu)點(diǎn)和缺點(diǎn)。本文采用的研究方法是基于著色Petri網(wǎng)的安全協(xié)議形式化分析，開展了以下主要工作：<

2、br>　　 1.介紹了安全協(xié)議的基礎(chǔ)知識(shí)和常見的安全協(xié)議形式化分析方法；闡述了Petri網(wǎng)的定義和Petri網(wǎng)的動(dòng)態(tài)特性，并介紹了著色Petri網(wǎng)的相關(guān)知識(shí)。
　　 2.采用一種基于著色Petri網(wǎng)的安全協(xié)議驗(yàn)證方法，該方法采用逆向狀態(tài)分析方法以及Petri網(wǎng)的可達(dá)性分析思想。而后，用兩個(gè)安全協(xié)議實(shí)例來驗(yàn)證這種方法的有效性，同時(shí)，發(fā)現(xiàn)隨著安全協(xié)議復(fù)雜性的增加，Petri網(wǎng)模型的狀態(tài)空間爆炸問題也隨之發(fā)生，并且此模型只能驗(yàn)證已知