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

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

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

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

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