基于模型檢測技術(shù)的NS協(xié)議分析模型的研究.pdf

1、計算機(jī)技術(shù)迅速發(fā)展,并且越來越多的滲透到各個行業(yè)和領(lǐng)域。尤為重要的是人們對軟件的可靠性要求也越來越高。為了提高軟件可靠性,眾多專家學(xué)者對多種方法進(jìn)行了研究。在眾多的理論和方法中,模型檢測(model checking)成為近幾年的研究熱點?；谠摾碚摰难芯?在高可靠性的軟件設(shè)計領(lǐng)域也不斷取得了重大的應(yīng)用。
　　模型檢測是一種形式化驗證方法,它將需要驗證的系統(tǒng)抽象成有限狀態(tài)模型,并使用時序邏輯語言描述系統(tǒng)所要檢測的屬性,然后對以上抽

2、象出的模型進(jìn)行有限狀態(tài)的窮盡搜索。使用模型檢測技術(shù)對電子商務(wù)協(xié)議進(jìn)行分析建模并且驗證其安全性是近年來的研究熱點。
　　本文詳細(xì)地介紹了模型檢測的理論背景,以及現(xiàn)在使用較為廣泛的模型檢測工具,例如SPIN,SMV等等。其中,SPIN是由貝爾實驗室開發(fā)的一種模型檢測工具,用于分析軟件系統(tǒng)的設(shè)計模型和各種協(xié)議的設(shè)計模型。同時,模型檢測在電子商務(wù)協(xié)議中的應(yīng)用也進(jìn)行了介紹。以及,對 Needham-Schroeder公鑰密碼協(xié)議進(jìn)行了說明。