密碼協(xié)議工程與基于新鮮性的協(xié)議安全研究.pdf

1、密碼協(xié)議的安全性研究是網(wǎng)絡(luò)安全研究的主要熱點(diǎn)。本論文主要研究了如何應(yīng)用系統(tǒng)工程思想和形式化方法來(lái)分析和設(shè)計(jì)密碼協(xié)議，取得的主要研究結(jié)果如下： 1.將系統(tǒng)工程思想引入密碼協(xié)議設(shè)計(jì)，結(jié)合前人的研究成果，提出了10條密碼協(xié)議工程原則：5條安全需求分析原則，4條詳細(xì)設(shè)計(jì)原則以及l(fā)條安全性證明原則。將密碼協(xié)議設(shè)計(jì)看作密碼協(xié)議工程，從協(xié)議設(shè)計(jì)的不同階段給出原則，是幫助研究人員按系統(tǒng)工程思想進(jìn)行密碼協(xié)議設(shè)計(jì)的有益嘗試。實(shí)例分析表明，這些原則不

2、僅較為完備，而且可操作性強(qiáng)，能幫助研究人員明確協(xié)議設(shè)計(jì)背后的隱含假設(shè)，發(fā)現(xiàn)和避免協(xié)議設(shè)計(jì)中的漏洞，簡(jiǎn)化協(xié)議設(shè)計(jì)。 2.首次提出基于信任的新鮮性標(biāo)識(shí)符分析密碼協(xié)議的安全性，給出了新鮮性原則：對(duì)每個(gè)通信參與主體而言，密碼協(xié)議的安全性取決于發(fā)送或者接收的、包含自身已相信新鮮的新鮮性標(biāo)識(shí)符的單向變換。該原則找到了一條快捷、有效的密碼協(xié)議安全性分析方法，論文示例了20多個(gè)經(jīng)典密碼協(xié)議的分析結(jié)果，分析出的針對(duì)協(xié)議的攻擊或者安全隱患有12個(gè)是

3、以往沒(méi)有指出過(guò)的。新鮮性原則的特點(diǎn)是：①能有效區(qū)分消息是否新鮮，安全性的分析獨(dú)立于并發(fā)運(yùn)行環(huán)境的具體形式化描述，也獨(dú)立于攻擊者能力的具體形式化描述；②基于該原則得到的分析結(jié)果能夠證明正確協(xié)議的安全性，也能夠分析出不安全協(xié)議存在的安全屬性缺失，以及由該缺失直接構(gòu)造攻擊的結(jié)構(gòu)。 3.基于新鮮性原則，提出了基于邏輯推理的信任多集形式化分析方法。以Needham-Schroeder公鑰認(rèn)證協(xié)議為例，說(shuō)明了該分析方法的有效性、嚴(yán)謹(jǐn)性和自動(dòng)

4、化實(shí)現(xiàn)的可能。另外，針對(duì)無(wú)線網(wǎng)絡(luò)的開(kāi)放性和數(shù)據(jù)包易失的特點(diǎn)，擴(kuò)展了信任多集方法，能有效用于無(wú)線密碼協(xié)議分析。 4.證明了保證認(rèn)證協(xié)議安全的充分必要條件，這些條件在計(jì)算模型下分別滿足基于匹配對(duì)話和不可區(qū)分性的4個(gè)可證安全定義。 5.提出了信任多集自動(dòng)分析工具的總體框架，通過(guò)在2種不同開(kāi)發(fā)環(huán)境下信任多集自動(dòng)分析工具初步實(shí)現(xiàn)的比較，給出了信任多集自動(dòng)分析工具的詳細(xì)設(shè)計(jì)。正在開(kāi)發(fā)的信任多集自動(dòng)分析工具已成功實(shí)現(xiàn)了對(duì)若干密碼協(xié)議的