基于模型檢測(cè)的形式化協(xié)議驗(yàn)證.pdf

1、隨著科學(xué)的發(fā)展和社會(huì)的進(jìn)步，信息技術(shù)的不斷向前發(fā)展，計(jì)算機(jī)互聯(lián)網(wǎng)及其分布式系統(tǒng)的應(yīng)用變得越來越廣泛，密碼協(xié)議在人們?nèi)粘Ｉ钌a(chǎn)中的運(yùn)用越來越受到關(guān)注，人們對(duì)密碼協(xié)議的可靠性和安全性的要求越來越高。任何不可預(yù)測(cè)的錯(cuò)誤都會(huì)產(chǎn)生極其嚴(yán)重的后果，而模型檢測(cè)就是一種能保證協(xié)議系統(tǒng)在設(shè)計(jì)時(shí)就證明是正確的，在其設(shè)計(jì)的過程中就發(fā)現(xiàn)是否有錯(cuò)的自動(dòng)化驗(yàn)證有力技術(shù)。這一檢測(cè)技術(shù)的基本原理就是用狀態(tài)遷移系統(tǒng)來表示系統(tǒng)的行為，以模態(tài)或時(shí)序邏輯來對(duì)系統(tǒng)的性質(zhì)進(jìn)行描

2、述。這樣，系統(tǒng)是否具備所期望的性質(zhì)，以及狀態(tài)遷移系統(tǒng)是否是公式的一個(gè)模型，就轉(zhuǎn)化為了一個(gè)數(shù)學(xué)公式，密碼協(xié)議的安全問題就轉(zhuǎn)化為一個(gè)數(shù)學(xué)問題。它通過系統(tǒng)模型的構(gòu)建，來檢測(cè)所期望的性質(zhì)是否滿足所建的模型，如不滿足，就會(huì)給出相應(yīng)的反例。
　　本文的主要工作是采用系統(tǒng)驗(yàn)證工具SPIN首先對(duì)LEAP進(jìn)行形式化分析研究，然后分別采用SPIN和AVISPA對(duì)其改進(jìn)協(xié)議----LEAP+A，LEAP+B進(jìn)行了驗(yàn)證，分別用Promela和HLPSL對(duì)