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

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

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

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