基于串空間模型的安全協(xié)議自動(dòng)化驗(yàn)證方法研究.pdf

1、隨著網(wǎng)絡(luò)技術(shù)和信息技術(shù)的迅速發(fā)展,計(jì)算機(jī)網(wǎng)絡(luò)在諸多領(lǐng)域內(nèi)的應(yīng)用日益普及,然而由于其運(yùn)行環(huán)境具有開(kāi)放性,使得計(jì)算機(jī)網(wǎng)絡(luò)在給人們帶來(lái)巨大便利的同時(shí),也產(chǎn)生一系列的安全問(wèn)題,因此如何確保網(wǎng)絡(luò)中信息的安全性成為亟待解決的問(wèn)題。安全協(xié)議又稱(chēng)密碼協(xié)議,是以密碼學(xué)技術(shù)為基礎(chǔ),在不安全的公共網(wǎng)絡(luò)和分布式系統(tǒng)中提供各種安全服務(wù)的一種通信協(xié)議。由于安全協(xié)議的安全性是評(píng)價(jià)網(wǎng)絡(luò)好壞的一個(gè)重要指標(biāo),所以在安全協(xié)議投入使用之前,對(duì)其安全性分析就顯得尤為重要。至今,

2、安全協(xié)議的形式化分析和自動(dòng)化檢測(cè)己成為分析和研究安全協(xié)議領(lǐng)域的兩個(gè)重要方向,而研制可靠實(shí)用的安全協(xié)議自動(dòng)化分析工具也逐漸成為主流趨勢(shì)。
　　 本文以串空間理論為基礎(chǔ),通過(guò)對(duì)當(dāng)前存在的一些安全協(xié)議形式化方法和自動(dòng)化技術(shù)進(jìn)行比較分析,深入地研究了安全協(xié)議的自動(dòng)化分析方法。主要內(nèi)容包括:
　　 1)深入研究了安全協(xié)議的安全性質(zhì),針對(duì)當(dāng)前運(yùn)用比較廣泛的形式化分析方法--串空間模型,通過(guò)研究構(gòu)造方法,重點(diǎn)介紹了NSL協(xié)議的分析過(guò)程

3、;同時(shí),以SSM協(xié)議為例,探討了如何使用認(rèn)證測(cè)試驗(yàn)證協(xié)議的過(guò)程及設(shè)計(jì)原理。
　　 2)給出了一種基于串空間模型的安全協(xié)議自動(dòng)化驗(yàn)證方法。在該方法中,針對(duì)參與方不檢測(cè)某些消息的來(lái)源,只是將其作為消息的子項(xiàng)參與協(xié)議的運(yùn)行的問(wèn)題,通過(guò)構(gòu)造和合法串結(jié)構(gòu)相同的攻擊者串的方式,給出了一種自動(dòng)化驗(yàn)證方法;它不僅能夠分析具有加密類(lèi)型的攻擊缺陷的協(xié)議,還將可信方引入到協(xié)議的參與方,使之能夠分析具有重放類(lèi)型攻擊缺陷的協(xié)議,整個(gè)過(guò)程無(wú)需人工干預(yù),直觀