安全協(xié)議形式化分析方法的比較和研究.pdf

1、隨著計(jì)算機(jī)網(wǎng)絡(luò)的廣泛應(yīng)用，計(jì)算機(jī)網(wǎng)絡(luò)的安全問題也日益引起人們的重視。在網(wǎng)絡(luò)安全中，各種安全服務(wù)都是基于安全協(xié)議的，這使得安全協(xié)議的安全性變得尤為重要。在過去的二十多年中，為了滿足各種各樣的網(wǎng)絡(luò)應(yīng)用，提出了大量安全協(xié)議，但是后來的研究證明這些安全協(xié)議大多數(shù)都含有這樣或者那樣的安全漏洞，如何設(shè)計(jì)一個(gè)比較安全的安全協(xié)議以及如何驗(yàn)證一個(gè)已設(shè)計(jì)出來的安全協(xié)議是否安全成為安全協(xié)議研究領(lǐng)域中最重要的兩方面。 安全協(xié)議是一種通信協(xié)議，它的主要目

2、的是利用密碼技術(shù)實(shí)現(xiàn)網(wǎng)絡(luò)通信中的密鑰分發(fā)和身份認(rèn)證。然而，大量事實(shí)表明，有許多安全協(xié)議經(jīng)過安全專家認(rèn)真仔細(xì)地分析、設(shè)計(jì)和實(shí)現(xiàn)后仍然存在著漏洞。本文首先介紹了以往的各種安全協(xié)議，在此基礎(chǔ)上總結(jié)出了五種典型的安全協(xié)議漏洞。 形式化方法能有效檢驗(yàn)安全協(xié)議的安全性，BAN邏輯的發(fā)展極大地促進(jìn)了這一領(lǐng)域的研究。本文重點(diǎn)闡述了形式化方法及其在安全協(xié)議驗(yàn)證中的應(yīng)用。同時(shí)，針對(duì)串空間模型這一新興的形式化方法進(jìn)行了深入地分析和研究，在此基礎(chǔ)上，應(yīng)