安全協(xié)議可視化建模和驗(yàn)證方法的分析與設(shè)計(jì).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é)議并不如它們所聲明的那樣安全，對(duì)安全協(xié)議的安全性進(jìn)行分析和驗(yàn)證已成為國內(nèi)外學(xué)者研究的熱點(diǎn)。
　　 為了保證安全協(xié)議的正確性，研究人員已提出多種分析方法來解決這個(gè)問題，但都存在一些不足。統(tǒng)一建模語言（UML）是國際上先進(jìn)的用于軟件分析

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

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