關(guān)于密碼協(xié)議的形式化分析方法的研究.pdf

1、隨著信息技術(shù)的快速發(fā)展和廣泛應(yīng)用,諸如電子商務(wù)這類需要高度安全性的應(yīng)用逐漸普及,建立安全信道的重要性可想而知。在網(wǎng)絡(luò)這個(gè)特殊的大環(huán)境里,兩個(gè)互相不認(rèn)識(shí)的主體如果想要達(dá)成某種通信目的,必須要在密碼技術(shù)保障的前提下進(jìn)行。
　　 雖然現(xiàn)階段對(duì)密碼協(xié)議的分析方法的研究已經(jīng)有了很多觀點(diǎn),但是還沒有一種被廣泛認(rèn)同的可以作為工業(yè)標(biāo)準(zhǔn)的方法,所以對(duì)于密碼協(xié)議的形式化分析方法仍然是一個(gè)開放性的熱點(diǎn)問題,而且具有重要的理論意義。
　　 本文

2、首先介紹了密碼學(xué)領(lǐng)域的一些基本概念,密碼協(xié)議的分類,以及在密碼協(xié)議中需要用到的一些重要的密碼學(xué)技術(shù):保密性,數(shù)據(jù)完整性,抗抵賴性以及消息認(rèn)證性。為了使得分析方法的設(shè)計(jì)更加具有針對(duì)性,本文假設(shè)所討論的協(xié)議都是在底層密碼技術(shù)安全的前提下進(jìn)行的;然后,本文通過分析密碼協(xié)議形式化方法的主流觀點(diǎn),總結(jié)出這些觀點(diǎn)存在的缺陷。接著通過對(duì)一些經(jīng)典的攻擊方式的分析,引出本文的主題,即對(duì)密碼協(xié)議安全性分析的形式化方法,提出這套方法的依據(jù)在于Bellare和

3、Rogaway對(duì)于密碼協(xié)議安全的公式化定義,以及作者在學(xué)習(xí)過程中總結(jié)出的一些密碼協(xié)議的設(shè)計(jì)原則。這個(gè)形式化方法分為五個(gè)模塊,首先對(duì)協(xié)議進(jìn)行前四個(gè)模塊的檢驗(yàn),然后在第五個(gè)模塊中對(duì)協(xié)議進(jìn)行安全性證明。本文通過對(duì)大量相關(guān)文獻(xiàn)的研究,深深的體會(huì)到對(duì)于密碼協(xié)議安全性證明的困難性。所以本文所采用的證明方式基于不同于傳統(tǒng)密碼學(xué)證明的邏輯方式,并不是將攻擊者攻破協(xié)議的行為歸約到攻破數(shù)學(xué)難題上,而是歸約到對(duì)已知假設(shè)的否定上,每個(gè)步驟在邏輯上都嚴(yán)密合理。接