安全協(xié)議可視化建模和驗證方法的分析與設(shè)計.pdf

1、隨著網(wǎng)絡(luò)技術(shù)的日益發(fā)展和Internet在全球的普及，網(wǎng)絡(luò)安全問題越來越被人們所重視。安全協(xié)議是構(gòu)建安全網(wǎng)絡(luò)環(huán)境的基石，安全協(xié)議的安全性是網(wǎng)絡(luò)安全的關(guān)鍵所在。人們已通過不同的方法證明一些已存在的安全協(xié)議并不如它們所聲明的那樣安全，對安全協(xié)議的安全性進行分析和驗證已成為國內(nèi)外學(xué)者研究的熱點。
　　 為了保證安全協(xié)議的正確性，研究人員已提出多種分析方法來解決這個問題，但都存在一些不足。統(tǒng)一建模語言（UML）是國際上先進的用于軟件分析

2、與設(shè)計的可視化建模語言，是一種定義良好、易于表達(dá)、功能強大且普遍適用的建模語言。但UML缺乏精確的語義描述，對UML模型進一步分析和驗證比較困難。形式化方法具有精確的數(shù)學(xué)語義和自動化驗證工具的支持，可以對軟件規(guī)范進行嚴(yán)格的分析和驗證，但形式化方法存在難以設(shè)計大型軟件，直接用形式化規(guī)范對系統(tǒng)建模難度大等缺點。為保證安全協(xié)議設(shè)計的正確性，在早期發(fā)現(xiàn)可能存在的錯誤，對協(xié)議的可視化模型進行形式化分析驗證很有必要。
　　 簡單進程元語言解

3、釋器（SPIN）作為模型檢測的一種工具，由于具有占用內(nèi)存空間小，并保證程序能夠按照原有的工作方式被高效地驗證的特點，被普遍地應(yīng)用于工業(yè)界和學(xué)術(shù)界，因此，本文使用SPIN工具對安全協(xié)議UML可視化模型進行了分析驗證。論文介紹了安全協(xié)議，安全協(xié)議的形式化分析方法，模型檢測技術(shù)，并著重介紹可視化建模語言UML和模型檢測工具SPIN的原理，結(jié)合面向?qū)ο罂梢暬：托问交椒ǖ膬?yōu)點，提出了一種將安全協(xié)議的可視化模型轉(zhuǎn)換成PROMELA規(guī)范的方法。