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

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

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