安全協(xié)議的設(shè)計(jì)與邏輯分析

1、V ol.14, No.7 ©2003 Journal of Software 軟 件 學(xué) 報(bào) 1000-9825/2003/14(071300 安全協(xié)議的設(shè)計(jì)與邏輯分析卿斯?jié)h+(中國(guó)科學(xué)院 信息安全技術(shù)工程研究中心,北京 100080 (中國(guó)科學(xué)院 軟件研究所 信息安全國(guó)家重點(diǎn)實(shí)驗(yàn)室,北京 100080Design and Logical Analysis of Security ProtocolsQING Si-Han +(Engineering Research Center for Information Security Technology, The Chinese Ac

2、ademy of Sciences, Beijing 100080, China (State Key Laboratory of Information Security, Institute of Software, The Chinese Academy of Sciences, Beijing 100080, China + Corresponding author: Phn: 86-10-62635150, Fax: 86-10-62635150, E-mail: qsihanReceived 2003-01-23; Accepted 2003-04-07Qing SH. Desig

3、n and logical analysis of security protocols. Journal of Software , 2003,14(7:13001309. Abstract : With the rapid growth of network applications, network security has become an important issue. In this paper, the following issues are investigated: the design principles of security protocols, the use

4、 of formal methods in the design of security protocols, the characteristics of various approaches to formal analysis, in particular logical analysis. The strand space approach to logical analysis, and the possibility of the strand space model guiding the formal design of security protocols are also

5、explored.Key words : security protocol; design; logical analysis; BAN-like logic; strand space摘 要: 隨著網(wǎng)絡(luò)應(yīng)用的迅速發(fā)展,網(wǎng)絡(luò)安全的問題日益重要.研究下述課題:安全協(xié)議的設(shè)計(jì)原則;安全協(xié)議設(shè)計(jì)中形式化方法的應(yīng)用;各種形式化分析方法,特別是邏輯分析方法的特點(diǎn).另外,還探討了串空間模型在邏輯分析中的應(yīng)用以及串空間模型指導(dǎo)安全協(xié)議形式化設(shè)計(jì)的可能性.關(guān)鍵詞: 安全協(xié)議;設(shè)計(jì);邏輯分析;BAN 類邏輯;串空間中圖法分類號(hào): TP309 文獻(xiàn)標(biāo)識(shí)碼: A密碼學(xué)是網(wǎng)絡(luò)安全的基礎(chǔ),但網(wǎng)絡(luò)安全不能單純依靠安全的

6、密碼算法.安全協(xié)議是網(wǎng)絡(luò)安全的一個(gè)重要組成部分,我們需要通過安全協(xié)議進(jìn)行實(shí)體之間的認(rèn)證、在實(shí)體之間安全地分配密鑰或其他各種秘密、確認(rèn)發(fā)送和接收的消息的非否認(rèn)性等.近年來,安全協(xié)議越來越多地用于保護(hù)因特網(wǎng)上傳送的各種交易,保護(hù)針對(duì)計(jì)算機(jī)系統(tǒng)的訪問.但是,經(jīng)驗(yàn)告訴我們,設(shè)計(jì)和分析一個(gè)正確的安全協(xié)議是一項(xiàng)十分困難的任務(wù).即使我們只討論安全協(xié)議中最基本的認(rèn)證協(xié)議,其中參加協(xié)議的主體只有兩三個(gè),交換的消息只有35條,設(shè)計(jì)一個(gè)正確的、符合 Supported by the National Natural Science Foundation of China under Grant No.6008300

7、7 (國(guó)家自然科學(xué)基金; the National Grand Fundamental Research 973 Program of China under Grant No.G1999035810 (國(guó)家重點(diǎn)基礎(chǔ)研究發(fā)展規(guī)劃(973第一作者簡(jiǎn)介: 卿斯?jié)h(1939-,男,湖南隆回人,研究員,博士生導(dǎo)師,主要研究領(lǐng)域?yàn)樾畔⑾到y(tǒng)安全理論和技術(shù).卿斯?jié)h:安全協(xié)議的設(shè)計(jì)與邏輯分析1301認(rèn)證目標(biāo)的、沒有冗余的認(rèn)證協(xié)議也很不容易1,2.因此,我們必須借助形式化的分析工具,證明安全協(xié)議的正確性.自20世紀(jì)70年代以來,安全協(xié)議的形式化分析已逐漸成為信息安全研究領(lǐng)域中的一個(gè)熱點(diǎn),涌現(xiàn)出眾多的研究方法.目

8、前,研究比較廣泛和深入的方法主要有以下4種:基于知識(shí)與信念推理的模態(tài)邏輯方法、基于通信狀態(tài)機(jī)模型的研究方法、基于知識(shí)推理的代數(shù)方法和基于順序通信進(jìn)程的CSP方法3.近年來,串空間模型4,5方法的應(yīng)用日益廣泛.本文第1節(jié)討論基于知識(shí)與信念推理的模態(tài)邏輯方法,對(duì)BAN邏輯6及其重要的增強(qiáng)與擴(kuò)展GNY邏輯7、AT邏輯8、VO邏輯9進(jìn)行詳盡的研究,比較它們的特點(diǎn)和優(yōu)缺點(diǎn).第2節(jié)討論BAN類邏輯中的佼佼者SVO邏輯10,并研究安全協(xié)議的邏輯分析方法和串空間模型4,5相結(jié)合的問題.第3節(jié)討論安全協(xié)議的設(shè)計(jì)原則.設(shè)計(jì)時(shí)必須充分考慮Dolev-Yao11攻擊者模型,不低估攻擊者的能力.安全協(xié)議必須能夠抵抗常見

9、攻擊,特別是重放攻擊12,13.然后,通過串空間模型的實(shí)例,說明形式化方法如何指導(dǎo)安全協(xié)議的正確設(shè)計(jì).第4節(jié)是簡(jiǎn)短的結(jié)論,并討論今后研究的若干方向.1 安全協(xié)議的形式化分析方法1.1 基于知識(shí)與信念推理的模態(tài)邏輯方法模態(tài)邏輯方法是分析安全協(xié)議的最為重要的方法之一,它們分析并驗(yàn)證了許多重要的安全協(xié)議14,其中包括分析經(jīng)典的Needham-Schroeder私鑰協(xié)議15、Lowe-Needham-Schroeder公鑰協(xié)議16、Nessett協(xié)議17等.模態(tài)邏輯分析方法與分布式系統(tǒng)中分析知識(shí)和信念演化的邏輯相似.這些邏輯系統(tǒng)由一些命題和推理規(guī)則組成,命題表示主體對(duì)消息的知識(shí)或信念,應(yīng)用推理規(guī)則可以

10、從已知的知識(shí)和信念推導(dǎo)出新的知識(shí)和信念.Syverson在文獻(xiàn)18中闡述了在安全協(xié)議的分析中,知識(shí)、信念和語義之間關(guān)系的相互作用.在這類方法中,最著名的是BAN類邏輯610.其他相近的工作還包括:Bieber邏輯CKT519、Syverson 邏輯KPL20、Rangan邏輯21、Moser邏輯22以及Yahalom,Klein,Beth的YHK邏輯23等.1999年,Kindred 在他的博士論文24中提出的密碼協(xié)議的生成理論RV邏輯是這方面的又一個(gè)新成果.Syverson邏輯將攻擊者具有的知識(shí)分為兩類:一類是攻擊者收到一條消息后所具有的知識(shí)(在看見一個(gè)比特串的含義下;另一類是攻擊者可以識(shí)別

11、消息時(shí)所具有的知識(shí).然后,Syverson邏輯可以對(duì)此進(jìn)行推理.類似于Syverson邏輯,Bieber邏輯也區(qū)別看見一條消息和理解一條消息,并能對(duì)安全協(xié)議中知識(shí)的演化進(jìn)行推理.Rangan邏輯的特點(diǎn)是研究可信(trust,對(duì)由“可信”到“信念”(belief的演化過程進(jìn)行推理.YKB邏輯則從另一個(gè)角度討論“可信”.在上述邏輯中,知識(shí)和信念的演化都是單調(diào)的,亦即知識(shí)和信念的演化只增不減.Moser邏輯是惟一的例外,它的信念演化是非單調(diào)的.例如,在推理過程中如果知道一個(gè)密鑰已被泄露,則其信念集合可以減小.BAN邏輯之所以著名,不僅由于它開創(chuàng)了安全協(xié)議形式化分析的先河,是一項(xiàng)開拓性的工作,而且由于

12、它提供的形式化分析方法特別直觀與簡(jiǎn)單.有人說,BAN邏輯成功的秘訣是“簡(jiǎn)單加實(shí)用”,這話有一定的道理.BAN 邏輯雖然簡(jiǎn)單,但仍然可以成功地揭示安全協(xié)議中的設(shè)計(jì)缺陷.例如,通過BAN邏輯分析,發(fā)現(xiàn)了CCITT X.509標(biāo)準(zhǔn)25推薦草案中的安全漏洞.BAN邏輯的直觀性與簡(jiǎn)單性主要表現(xiàn)在以下幾個(gè)方面:第1,BAN邏輯不區(qū)分看見一條消息和理解一條消息;第2,BAN邏輯的信念演化過程是單調(diào)遞增的;第3,BAN邏輯不討論“可信”;第4,BAN邏輯不討論知識(shí);第5,BAN邏輯假設(shè)參加協(xié)議的主體是誠(chéng)實(shí)的,他們都忠實(shí)地根據(jù)協(xié)議的規(guī)則執(zhí)行協(xié)議;第6,BAN邏輯假設(shè)加密系統(tǒng)是完善的(perfect等等.但是,B

13、AN邏輯不追求完美而追求簡(jiǎn)潔、實(shí)用的設(shè)計(jì)思想,也為BAN邏輯分析方法帶來了局限性,使BAN 方法的抽象級(jí)別過高,分析范圍過窄.例如,由于BAN邏輯不能對(duì)知識(shí)進(jìn)行推理,因此,BAN邏輯只能分析協(xié)議的認(rèn)證性質(zhì),而不能分析協(xié)議的保密性質(zhì).然而在現(xiàn)實(shí)中,通常的密鑰分配協(xié)議要同時(shí)實(shí)現(xiàn)保密性和認(rèn)證性兩個(gè)重要目標(biāo).1302Journal of Software 軟件學(xué)報(bào) 2003,14(71.2 BAN 邏輯 BAN 邏輯是一種多類型模態(tài)邏輯(many-sorted modal logic,它包含以下3種處理對(duì)象:主體、密鑰和公式.其中的公式,也稱作語句或命題.BAN 邏輯僅包含合取這一命題聯(lián)接詞,用逗號(hào)表

14、示.BAN 邏輯共有19條推理規(guī)則.在推理規(guī)則中,是元語言符號(hào).C 表示可以由前提集推導(dǎo)出結(jié)論C .應(yīng)用BAN 邏輯形式化分析安全協(xié)議的步驟是:1. 對(duì)安全協(xié)議進(jìn)行理想化,亦即,將協(xié)議消息轉(zhuǎn)換為BAN 邏輯所能理解的公式;2. 對(duì)安全協(xié)議進(jìn)行解釋,亦即,將形如的消息轉(zhuǎn)換成形如Q 的邏輯語言.解釋過程中遵循以下規(guī)則:X Q P :X received (1 若命題X 在消息前成立,則在其后,X 和都成立;Y Q P :Y Q received (2 若根據(jù)推理規(guī)則可以由命題X 推導(dǎo)出命題Y ,則命題X 成立時(shí),命題Y 亦成立;3. 應(yīng)用BAN 邏輯語言對(duì)系統(tǒng)的初始狀態(tài)進(jìn)行描述,給出初始化假設(shè)集;

15、4. 應(yīng)用BAN 推理規(guī)則對(duì)協(xié)議進(jìn)行形式化分析,得出相應(yīng)的結(jié)論.關(guān)于BAN 邏輯的其他內(nèi)容,例如BAN 邏輯構(gòu)件的語法和語義、BAN 邏輯的推理規(guī)則、BAN 邏輯分析認(rèn)證協(xié)議的實(shí)例等,讀者可參見其他文獻(xiàn),例如文獻(xiàn)1,2.1990年,Nessett 17引入一個(gè)簡(jiǎn)單的例子,試圖說明BAN 邏輯本身存在一個(gè)重要的安全問題.Nessett 協(xié)議如下:. : .2, : .11AB A K b K AB a N A B K N B A 在消息1中,A 用其秘密密鑰加密A 與B 之間的會(huì)話密鑰和臨時(shí)值,然后發(fā)送給B .B 用A 的公開密鑰解密出,然后用加密臨時(shí)值后發(fā)送給A ,顯然,不是A 和B 之間通信

16、的“良好”的會(huì)話密鑰,因?yàn)槿魏沃黧w都可以從消息1中獲得會(huì)話密鑰.但是,用BAN 邏輯分析Nessett 協(xié)議,卻得出是良好的會(huì)話密鑰的結(jié)論.a N A K AB K AB Kb N AB K AB K AB K 據(jù)此,Nessett 認(rèn)為,BAN 邏輯本身存在一個(gè)重要缺陷,該缺陷源于BAN 邏輯的分析范圍.因?yàn)锽AN 邏輯只考慮分配密鑰和身份認(rèn)證的問題,但未考慮哪個(gè)主體不應(yīng)當(dāng)獲得密鑰,亦即,未考慮機(jī)密性的問題.BAN 26對(duì)Nessett 的批評(píng)答復(fù)如下:在BAN 邏輯的文獻(xiàn)中,已經(jīng)清楚地說明,BAN 邏輯只討論誠(chéng)實(shí)主體的認(rèn)證問題,并不關(guān)心檢測(cè)非授權(quán)地暴露秘密的問題.在Nessett 協(xié)議中,

17、A 在消息1中公開了,故Nessett 的假定:不符合BAN 的基本假定.因此,Nessett 從不合理的初始假定推導(dǎo)出了不合理的結(jié)論,而BAN 邏輯本身并不能防止建立不合理的初始假定集合.AB K B A A AB K believes 雖然我們不能通過Nessett 協(xié)議說明BAN 邏輯本身存在著缺陷,但Nessett 的反例啟示我們,BAN 邏輯的推理分析依賴于我們所作的基本假設(shè)和初始假設(shè).如果非形式化的初始假設(shè)錯(cuò)了,則通過形式化分析之后常常得出錯(cuò)誤的結(jié)論.1.3 GNY 邏輯、AT 邏輯和VO 邏輯在對(duì)BAN 邏輯進(jìn)行增強(qiáng)和擴(kuò)充的過程中,GNY 邏輯、AT 邏輯、VO 邏輯和SVO 邏

18、輯最為著名,習(xí)慣上統(tǒng)稱它們?yōu)锽AN 類邏輯.其中,SVO 邏輯是在總結(jié)BAN 邏輯、GNY 邏輯、AT 邏輯和VO 邏輯的基礎(chǔ)上發(fā)展起來的,我們將在下一節(jié)加以討論.(1 GNY 邏輯BAN 邏輯問世以后,第一個(gè)對(duì)它進(jìn)行增強(qiáng)的是GNY 邏輯.GNY 的邏輯公設(shè)有44個(gè)之多.此外,在GNY 邏輯中,如果21C C 是邏輯公設(shè),則對(duì)任何主體P ,21|C P C P 也是邏輯公設(shè). 具體地說,在GNY 邏輯中,有接收法則6個(gè)(T1T6;擁有法則8個(gè)(P1P8;新鮮性法則11個(gè)(F1F11;識(shí)別法則6個(gè)(R1R6;消息解釋法則7個(gè)(I1I7;管轄法則3個(gè)(J1J3;“不在這里產(chǎn)生”法則3個(gè).GNY 邏

19、輯對(duì)BAN 邏輯的重要改進(jìn)與推廣有以下幾個(gè)方面:(1 通過新增加的邏輯構(gòu)件與法則,推廣了卿斯?jié)h:安全協(xié)議的設(shè)計(jì)與邏輯分析 1303 BAN 邏輯的應(yīng)用范圍.例如,GNY 邏輯不局限于分析認(rèn)證協(xié)議,還可以分析某些應(yīng)用單向函數(shù)的密碼協(xié)議;(2 增加了“擁有密鑰”的表達(dá)式,增強(qiáng)了GNY 邏輯本身的表達(dá)能力.因此,A 相信C 擁有A 和B 之間的共享密鑰可以表示為,并能進(jìn)行相應(yīng)的推理;(3 在GNY 邏輯中,區(qū)分一個(gè)主體收到的消息和一個(gè)主體可用的消息;(4 在GNY 邏輯中,進(jìn)一步區(qū)分一個(gè)主體自己生成的消息和其他消息;(5 在GNY 邏輯分析中,在理想化協(xié)議中保留明文.而在BAN 邏輯分析中,明文在認(rèn)

20、證過程中不起作用.AB K C A has believes 類似于BAN 邏輯,為了簡(jiǎn)化分析過程,在GNY 邏輯中不包含否定形式,也沒有粒度更細(xì)的時(shí)序概念.此外,GNY 邏輯的語義也與BAN 邏輯相似.盡管GNY 邏輯具有上述特點(diǎn),但它本身過于復(fù)雜.在它的44個(gè)法則中,有許多法則使GNY 邏輯本身不必要地復(fù)雜.因此許多學(xué)者認(rèn)為,應(yīng)用GNY 邏輯分析安全協(xié)議在實(shí)際上是行不通的.盡管如此,我們認(rèn)為,GNY 邏輯在歷史的長(zhǎng)河中發(fā)揮了它應(yīng)有的作用,使我們對(duì)認(rèn)證協(xié)議及BAN 邏輯分析有了更加深刻的認(rèn)識(shí).在BAN 邏輯之后不久出現(xiàn)的AT 邏輯為BAN 邏輯構(gòu)造了一個(gè)簡(jiǎn)單的語義模型,是對(duì)BAN 邏輯的一種

21、重要改進(jìn).類似于GNY 邏輯,AT 邏輯對(duì)BAN 邏輯的本質(zhì)與局限性進(jìn)行了深入的分析,并獲得了相近的結(jié)論.但是,GNY 得到的是一個(gè)更加復(fù)雜的邏輯,其原因是GNY 邏輯和BAN 邏輯一樣,缺乏一個(gè)適當(dāng)?shù)恼Z義基礎(chǔ).AT 邏輯比BAN 邏輯更接近傳統(tǒng)的模態(tài)邏輯:它包含一個(gè)詳細(xì)的計(jì)算模型,增加了模型論語義,表達(dá)能力更強(qiáng),因而將BAN 邏輯向前推進(jìn)了一大步.AT 邏輯對(duì)BAN 邏輯的改進(jìn)還包括:(1 對(duì)BAN 邏輯中的定義和推理法則進(jìn)行整理,拋棄其中語義和實(shí)現(xiàn)細(xì)節(jié)的混和部分;(2 對(duì)某些邏輯構(gòu)件引入更直接的定義,免除對(duì)誠(chéng)實(shí)性進(jìn)行隱含假設(shè);(3 簡(jiǎn)化了推理法則,所有的概念都獨(dú)立定義,不與其他概念相混淆;

22、(4 整個(gè)邏輯只有兩條基本推理規(guī)則,亦即:(a MP 規(guī)則(modus ponens:由和可以推導(dǎo)出;(b Nec 規(guī)則(necessitation:由可以推導(dǎo)出P believes .例如,BAN 邏輯有P said X 的邏輯構(gòu)件,說明P 發(fā)送過X ,但沒有P 最近發(fā)送X 的構(gòu)件.在AT 邏輯中引入了新的邏輯構(gòu)件P says X ,表示P 最近發(fā)送X ,因此更加接近新鮮性的本質(zhì).AT 邏輯的公理A20: ,說明若X 是新鮮的且P 發(fā)送過X ,則P 最近發(fā)送了X .這條公理更加深刻地描述了新鮮性的本質(zhì).X P X P X fresh says said (在AT 邏輯中有一條比BAN 邏輯更

23、加直接的管轄公理A15:says controls P P ,說明若P 管轄且P 最近說過,則是真實(shí)的.這個(gè)更自然的管轄內(nèi)涵,使AT 邏輯不必進(jìn)行隱含的誠(chéng)實(shí)性假設(shè).VO 邏輯的貢獻(xiàn)是擴(kuò)展了BAN 邏輯的應(yīng)用范圍.Diffie-Hellman 協(xié)議27是許多近代密鑰分配協(xié)議的基礎(chǔ),VO 邏輯的設(shè)計(jì)目標(biāo)就是增加分析Diffie-Hellman 協(xié)議的能力,進(jìn)而可以分析IETF 標(biāo)準(zhǔn)因特網(wǎng)密鑰交換協(xié)議IKE 28和SSL 等.VO 邏輯的另一個(gè)重要特點(diǎn)是,細(xì)化了認(rèn)證協(xié)議的認(rèn)證目標(biāo),給出了以下6種不同形式的認(rèn)證目標(biāo):(G1 Ping 認(rèn)證:.says believes Y B AG1說明A 相信B 最

24、近發(fā)送過消息Y ,隱含B 當(dāng)前是激活的,亦即協(xié)議本回合開始后,B 采取了行動(dòng).注意,B 實(shí)際上想把消息Y 發(fā)送給哪個(gè)主體是不清楚的.這類認(rèn)證用于,某個(gè)主體A 想知道他的對(duì)話方B 是否當(dāng)前是激活的.(G2 實(shí)體認(rèn)證:(. ,says believes Y R G R Y B A A這里,表示由主體A 生成的臨時(shí)值,G (R A R A 是A 向B 發(fā)出的請(qǐng)求.G2說明,A 相信B 最近發(fā)送了消息Y ,且它是對(duì)A 的請(qǐng)求的響應(yīng).與Ping 認(rèn)證不同,實(shí)體認(rèn)證不僅要求A 的對(duì)話方發(fā)送一條消息,而且該消息必須與當(dāng)前協(xié)議回合的會(huì)話有關(guān),例如是對(duì)A 的當(dāng)前請(qǐng)求的響應(yīng).因此,A 不僅認(rèn)證了B 在A 所執(zhí)行的

25、當(dāng)前協(xié)議回合中是激活的,而且B 參與了與A 在當(dāng)前協(xié)議回合中的對(duì)話.(G3 安全密鑰建立:.believes B A A K 1304 Journal of Software 軟件學(xué)報(bào) 2003,14(7在VO 邏輯中,對(duì)BAN 邏輯中的邏輯構(gòu)件進(jìn)行了細(xì)化.VO 認(rèn)識(shí)到,AT 邏輯中的構(gòu)件表示A 相信K 是良好的密鑰,或K 是共享密鑰等等.因此,VO 邏輯將構(gòu)件細(xì)化為:B A K K A has B A K ,表示K 是A 的適用于B 的未經(jīng)確認(rèn)的密鑰.除了A 和B 以外,任何其他主體都不知道,也不能推導(dǎo)出K .注意,這個(gè)邏輯構(gòu)件強(qiáng)調(diào)的是,A 知道K ,但B 未必知道K .以A 的觀點(diǎn),K 可

26、能是一個(gè)適合A 與B 之間通信的良好密鑰.B A K ,表示K 是A 的適用于B 的已經(jīng)確認(rèn)的密鑰.A 知道K ,且A 已經(jīng)從B 那里收到了證據(jù)(密鑰確認(rèn),說明B 確實(shí)也知道K .其他任何主體都不知道,也不能推導(dǎo)出K .B A K +因此,在增加了這兩個(gè)新的邏輯構(gòu)件之后,A 和B 的地位是不能互換的.G3說明,A 相信除了B 以外,任何其他主體都不會(huì)與A 共享密鑰K .當(dāng)B 最終獲得K 之后,A 相信K 是A 和B 之間良好的會(huì)話密鑰.注意,G3并不表明B 參加了協(xié)議的運(yùn)行,也不表明K 擁有K .(G4 密鑰確認(rèn):.believes B A A K +G4說明,A 相信K 是A 和B 之間的共

27、享密鑰,且B 向A 提供了知道K 的證據(jù).G4表示K 是A 和B 之間良好的會(huì)話密鑰,且確認(rèn)B 知道K .此時(shí),即在A 執(zhí)行當(dāng)前協(xié)議回合時(shí),B 不但是激活的,而且B 的身份也是確認(rèn)的.(G5 密鑰新鮮性:.(believes k fresh AG5說明,A 相信密鑰K 是新鮮的.(G6 互相信任共享密鑰:.believes believes A B B A K G6說明,A 相信B 相信K 是適用于A 的未經(jīng)確認(rèn)的密鑰.注意,此處B 的信念超出了A 的控制范圍.因此,以A 的觀點(diǎn),G6的意義在于B 已經(jīng)確認(rèn)了A 的身份,即B 確認(rèn)A 是與B 共享密鑰K 的主體.注意,(G4:與B A A K

28、+believes B 關(guān)于K 的信念無關(guān).因此(G4與(G6是不同的.此外,B A A K +believes (.has believes (believes K B A B A A K 關(guān)于認(rèn)證目標(biāo)的進(jìn)一步討論,讀者可參見文獻(xiàn)16,29,30.2 BAN 類邏輯分析方法與串空間模型2.1 SVO 邏輯SVO 邏輯吸取了BAN 邏輯、GNY 邏輯、AT 邏輯和VO 邏輯的優(yōu)點(diǎn),將它們集成在一個(gè)邏輯系統(tǒng)中.在形式化語義方面,SVO 邏輯對(duì)一些概念重新進(jìn)行定義(有別于AT 邏輯,從而取消了AT 邏輯系統(tǒng)中的一些限制.SVO 邏輯所用的記號(hào)與BAN 類邏輯相似,其中特有的12個(gè)符號(hào)及其含義如下:

29、1. *:主體所收到的、不可識(shí)別的消息;2.K :密鑰K 對(duì)應(yīng)的解密密鑰;3. X P K :加密消息,P 是發(fā)送者(常省略;K X 4. X K :用密鑰K 對(duì)消息X 簽名后所得到的簽名消息;5. X P Y :合成消息X Y ,P 是發(fā)送者(常省略;6. PK (P ,K :K 為主體P 的公開加密密鑰;7. PK (P ,K :K 為主體P 的公開簽名驗(yàn)證密鑰;8. PK (P ,K :K 為主體P 的公開協(xié)商密鑰(或參數(shù);9. SV (X ,K ,Y :用密鑰K 可驗(yàn)證X 是Y 的簽名;10.:K 是P 和Q 之間的良好共享密鑰,但P 和Q 可能都不知道K ; Q P K 11.:K

30、是P 的適合于與Q 通信的非確認(rèn)共享密鑰; Q P K 12.:K 是P 的適合于與Q 通信的確認(rèn)共享密鑰. Q P K +與AT 邏輯相似,SVO 邏輯也將語言劃分為集合T 上的消息語言M T 和公式語言F T .其中T 為原子術(shù)語集,由主體、共享密鑰、公開密鑰、私有密鑰及一些常量符號(hào)構(gòu)成.應(yīng)用SVO 邏輯對(duì)安全協(xié)議進(jìn)行形式化分析可以分為以下3個(gè)步驟:(1 給出協(xié)議的初始化假設(shè)集,即用SVO 邏輯語言表示出各主體的初始信念、接收到的消息、對(duì)所收到消息的理解和解釋;(2 給出協(xié)議可能或應(yīng)該達(dá)到的目標(biāo)集,即用SVO 邏輯語言表示的一個(gè)公式集;(3 在SVO 邏輯中證明結(jié)論是否成立.若成立,則說明

31、該協(xié)議達(dá)到了預(yù)期的設(shè)計(jì)目標(biāo),協(xié)議的設(shè)計(jì)是成功的.因此,正確理解安全協(xié)議中消息的含義和協(xié)議的設(shè)計(jì)目標(biāo),是應(yīng)用SVO 邏輯進(jìn)行協(xié)議分析的基礎(chǔ).SVO 邏輯是BAN 類邏輯中的佼佼者.它的理論基礎(chǔ)更加堅(jiān)實(shí),在實(shí)用上保持了BAN 邏輯簡(jiǎn)單易用的特點(diǎn),因此被廣泛接受.應(yīng)用SVO 邏輯不僅成功地分析了各種認(rèn)證協(xié)議,也成功地分析了在電子商務(wù)中應(yīng)用日益廣泛的非否認(rèn)協(xié)議31,32.2.2 串空間模型與BAN 類邏輯AT 邏輯和SVO 邏輯已經(jīng)引入模型論語義,是BAN 類邏輯發(fā)展過程中重要的一步.但是,其語義中的計(jì)算模型源于認(rèn)知邏輯中對(duì)分布計(jì)算進(jìn)行推理的一般模型,并不特別適用于認(rèn)證協(xié)議.因此,在BAN 類邏輯中引

32、進(jìn)串空間模型語義,是一種可行的方法33.串(strand是參與協(xié)議的主體可以執(zhí)行的事件序列.對(duì)于誠(chéng)實(shí)的主體,該事件序列是根據(jù)協(xié)議定義,由發(fā)送事件和接收事件組合而成的.此外,該模型還定義了攻擊者串,描述攻擊者的行為.串空間是由協(xié)議參與者,包括誠(chéng)實(shí)主體和攻擊者的串組成的串集合.串集合之間可以穿插組合,使一個(gè)串的發(fā)送消息對(duì)應(yīng)另一個(gè)串的接收消息.叢(bundle是串空間中的重要概念,表示一個(gè)完整的協(xié)議交換串空間的子集.叢可以表示為有限無環(huán)圖,其中的邊表示結(jié)點(diǎn)間的因果依賴關(guān)系.在串空間模型中,共有兩種不同類型的邊:(1 表示發(fā)送消息M 被接收;21n n 1n 2n (2 表示是在同一個(gè)串上的直接因果前

33、驅(qū).21n n 1n 2n 關(guān)于串空間模型的詳細(xì)介紹,請(qǐng)參見文獻(xiàn)4,5,34.我們假設(shè)有一個(gè)運(yùn)行集R 和一個(gè)解釋.將每個(gè)命題常量p 映射到一個(gè)點(diǎn)集(p ,在這些點(diǎn)上,p 的值為“真”.公式在點(diǎn)(r ,t 為真,寫作(r ,t .表示有效,即在所有運(yùn)行點(diǎn)均為真.令表示叢中的點(diǎn),亦即叢中串s 上的第i 個(gè)結(jié)點(diǎn).令表示執(zhí)行串s 的主體.i s C ,C C (s c prin 作為舉例,以下是SVO 邏輯中4個(gè)典型公式的串空間模型語義,其中M 為任何消息.(1 i s C ,M P sent 當(dāng)且僅當(dāng)中存在一個(gè)結(jié)點(diǎn)C j t ,滿足:(a P t princ =(;(b i s j t ,p ;(c

34、.,(M j t term +=(2 i s C ,M P received 當(dāng)且僅當(dāng)C 中存在一個(gè)結(jié)點(diǎn)j t ,滿足:(a P t princ =(;(b i s j t ,p ;(c.,(M j t term =在給出公式的串空間模型語義之前,我們還需要做下述準(zhǔn)備:M P said 設(shè)A 是我們所討論的項(xiàng)代數(shù)集合.若A 的,KK K 理想是A 的子集I ,使得對(duì)所有的及k K ,均有A g I h ,(i;,I gh hg (ii.I h k 我們將包含h 的最小K 理想記為.h I K 令,是K K A s A t 的K 子項(xiàng),記為s K t ,當(dāng)且僅當(dāng)s I t K. 若在定義中有KK

35、 =,則簡(jiǎn)稱s 是t 的子項(xiàng),并記為s t . (3M P i s C said |,=當(dāng)且僅當(dāng)存在消息M ,滿足i s C ,且M P sent M K M .這里,K 是P 在i s ,擁有的密鑰集合.為了引入公式的串空間模型語義,我們需要過濾(filter的定義,它是理想的對(duì)偶,亦稱互理想(co-ideal.M P got 若,A 的K 過濾是A 的子集F ,使得對(duì)所有的h ,g A 及KK K k ,均有: (i 若成立,則有F hg F h 且;F g (ii 若成立,則有F h k F h 對(duì)成立.K k 1我們將包含h 的最小K 過濾記為.h F K (4M P i s C go

36、t |,=當(dāng)且僅當(dāng)存在消息M ,滿足i s C ,M P received ,且M F M K .這里,K 是P 在擁有的密鑰集合. i s ,3 安全協(xié)議的設(shè)計(jì)3.1 安全協(xié)議設(shè)計(jì)的原則在設(shè)計(jì)協(xié)議時(shí),如何保證安全協(xié)議能夠滿足保密性、無冗余、認(rèn)證身份等設(shè)計(jì)目標(biāo)呢?經(jīng)過總結(jié),我們提出了以下安全協(xié)議的設(shè)計(jì)原則:(1 設(shè)計(jì)目標(biāo)明確,無二義性;(2 最好應(yīng)用描述協(xié)議的形式語言,對(duì)安全協(xié)議本身進(jìn)行形式化描述;(3 通過形式化分析方法證明安全協(xié)議實(shí)現(xiàn)了設(shè)計(jì)目標(biāo);(4 安全性與具體采用的密碼算法無關(guān);(5 保證臨時(shí)值和會(huì)話密鑰等重要消息的新鮮性,防止重放攻擊;(6 盡量采用異步認(rèn)證方式,避免采用同步時(shí)鐘(時(shí)

37、戳的認(rèn)證方式;(7 具有抵抗常見攻擊,特別是防止重放攻擊的能力;(8 進(jìn)行運(yùn)行環(huán)境的風(fēng)險(xiǎn)分析,作盡可能少的初始安全假設(shè);(9 實(shí)用性強(qiáng),可用于各種網(wǎng)絡(luò)的不同協(xié)議層;(10 盡可能減少密碼運(yùn)算,降低成本,擴(kuò)大應(yīng)用范圍.其中,第(7條十分重要.Dolev 和Yao 于1983年提出了Dolev-Yao 11攻擊者模型.它是對(duì)攻擊者的知識(shí)和能力進(jìn)行概括的最早的模型,此后關(guān)于安全協(xié)議的形式化分析或多或少都受到他們的工作的影響.“永遠(yuǎn)不低估攻擊者的能力”,這是設(shè)計(jì)安全協(xié)議時(shí)應(yīng)當(dāng)時(shí)刻牢記的一條重要原則.3.2 應(yīng)用形式化方法指導(dǎo)安全協(xié)議設(shè)計(jì)在安全協(xié)議發(fā)展的近20年中,形式化方法主要用于分析安全協(xié)議.但是,

38、形式化方法用于指導(dǎo)安全協(xié)議的設(shè)計(jì)同樣有效.近年來,關(guān)于這方面的研究日益增多3,35,36.下面我們舉例說明如何應(yīng)用串空間模型和認(rèn)證測(cè)試方法來指導(dǎo)安全協(xié)議的設(shè)計(jì)36.在這個(gè)例子中,設(shè)計(jì)目標(biāo)是修改Otway-Rees 協(xié)議的安全缺陷6,14,對(duì)它進(jìn)行重新設(shè)計(jì).首先,在協(xié)議中不再加密最初的請(qǐng)求,因此新協(xié)議將采用入測(cè)試方法.其次,新協(xié)議的目標(biāo)是對(duì)每個(gè)主體都保證對(duì)方獲得同一個(gè)會(huì)話密鑰,這個(gè)目標(biāo)原Otway-Rees 協(xié)議沒有達(dá)到.新協(xié)議的形狀如圖1所示,根據(jù)新的設(shè)計(jì)目標(biāo)增加了最后的請(qǐng)求與響應(yīng)消息序列.A 對(duì)B 的請(qǐng)求用11表示,B 對(duì)A 的響應(yīng)可在24上返回,因此不需要改變?cè)瓍f(xié)議的形狀.我們要求B 對(duì)A

39、 的請(qǐng)求用24表示,且A 在53上對(duì)此請(qǐng)求進(jìn)行響應(yīng).A 必須在1生成臨時(shí)值,然后由S 在邊21上進(jìn)行變換,在結(jié)點(diǎn)2上,這個(gè)臨時(shí)值必須與會(huì)話密鑰K 同時(shí)嵌入一個(gè)加密分量t .如此,將能向A 認(rèn)證服務(wù)器S 生成K .A 1同樣,A 必須在1生成臨時(shí)值,以供B 用于證明獲得K .B 將沿43a N 變換該臨時(shí)值,并將它嵌入加密分量后發(fā)送,以便滿足A 的第2次測(cè)試.這里,我們應(yīng)用同一個(gè)臨時(shí)值,而不是生成另一個(gè)臨時(shí)值,以節(jié)約計(jì)A t 2aN 算資源. B 必須類似地在2生成臨時(shí)值,被服務(wù)器沿邊b N 21進(jìn)行變換,生成加密項(xiàng).也要傳送給A ,以便沿著邊B t 1b N 32進(jìn)行變換.A 應(yīng)用K 生成包含

40、的加密分量.b N B t 2通過以上討論,我們可以對(duì)圖1進(jìn)行填充,所得結(jié)果如圖2所示.我們?cè)?1和12邊上引入了主體名,以便接收者知道提出請(qǐng)求的是哪個(gè)主體.在結(jié)點(diǎn)2,可以完成A 的兩次入測(cè)試.因此,此時(shí)A 收到他所需要的所有認(rèn)證保證.A Fig.1 Shape of the new protocol expressed by strand space model圖1 串空間模型表述的新協(xié)議形狀A(yù) 23Fig.2 Important components in the new protocol圖2 新協(xié)議中的重要分量下面,我們定義4個(gè)測(cè)試分量B i A i t t 2,1(=i .其中,必須向

41、A 保證,S 生成K 作為對(duì)的響應(yīng),且K 是A 和B 的會(huì)話密鑰.因此,的形狀應(yīng)為A t 1a N A t 1A K BK a N .,其中說明上述加密分量是由A 生成的.類似地,的形狀應(yīng)為A K B t 1.B K b AK N R I C C A t 1和應(yīng)當(dāng)具有不同的形狀,為此我們可以選擇兩個(gè)不同的正文值.例如,令和為常量,且,我們可以確定和如下:B 1t IC R C A t 1B t 1A t 1=A K a I BKN C , =B t 1B K b R AK N C . 對(duì)于兩個(gè)主體的第2個(gè)認(rèn)證測(cè)試,我們只要求用K 加密臨時(shí)值和,且測(cè)試分量具有不同的形狀,因此我們可以定義 a N

42、 b N A t 2=, =K a I N C B t 2.K b R N C 因此,新協(xié)議達(dá)到了如下目標(biāo):(1 發(fā)起者A 和響應(yīng)者B 從可信服務(wù)器S 獲得新鮮的會(huì)話密鑰K ;(2 A 和B共享K,未對(duì)任何其他主體泄露K;(3 每個(gè)主體都相信,對(duì)方在協(xié)議中為收到K均執(zhí)行到協(xié)議相應(yīng)的一步.關(guān)于以上論斷的形式化證明從略.4 結(jié)論形式化分析方法,包括簡(jiǎn)單直接的BAN類邏輯分析方法,不但是分析安全協(xié)議的重要工具,也是指導(dǎo)安全協(xié)議設(shè)計(jì)的理論基礎(chǔ).我們預(yù)期,今后這一領(lǐng)域的熱點(diǎn)研究方向包括:(1 減少對(duì)協(xié)議所作的基本假設(shè),例如,加密體制的“完善”(perfect假設(shè)、自由加密(free encryption

43、假設(shè)等,使理論研究盡量接近實(shí)際.(2 擴(kuò)大協(xié)議的分析范圍.例如,分析安全電子商務(wù)協(xié)議;分析協(xié)議的公平性等.(3 增加分析“協(xié)議組合”的能力,這是目前的研究熱點(diǎn)與難點(diǎn)之一.(4 綜合不同分析方法的特點(diǎn),例如,CSP模型、串空間模型、模型校驗(yàn)器(model checker方法、線性邏輯方法等的相互比較與結(jié)合的研究.(5 安全協(xié)議的自動(dòng)生成與校驗(yàn)研究.(6 參加協(xié)議的主體數(shù)目可以無限增加時(shí)的研究,等等.References:1 Qing, SH. Cryptography and Computer Network Security. Beijing: Tsinghua University Pres

44、s, 2001. 127147 (in Chinese.2 Qing, SH. Formal analysis of authentication protocols. Journal of Software, 1996,7:107114 (in Chinese with English abstract.3 Meadows C. Formal verification of cryptographic protocols: A survey. In: Advances in Cryptology, Asiacrypt96 Proceedings.LNCS 1163, Berlin: Spri

45、nger-Verlag, 1996, 135150.4 Thayer FJ, Herzog JC, Guttman JD. Strand spaces: Why is a security protocol correct? In: Proceedings of the 1998 IEEESymposium on Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1998. 160171.5 Thayer FJ, Herzog JC, Guttman JD. Strand spaces: Proving secur

46、ity protocols correct. Journal of Computer Security, 1999,7(2-3:191230.6 Burrows M, Abadi M, Needham R. A logic of authentication. Research Report 39, Digital Systems Research Center, 1989.7 Gong L, Needham R, Yahalom R. Reasoning about belief in cryptographic protocols. In: Proceedings of the 1990

47、IEEE ComputerSociety Symposium on Research in Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1990. 234248.8 Abadi M, Tuttle MR. A semantics for a logic of authentication. In: Proceedings of the 10th ACM Symposium on Principles ofDistributed Computing. ACM Press, 1991. 201216.9 van

48、Oorschot PC. Extending cryptographic logics of belief to key agreement protocols. In: Proceedings of the 1st ACM Conferenceon Computer and Communications Security. ACM Press, 1993. 233243.10 Syverson, PF, van Oorschot PC. On unifying some cryptographic protocol logics. In: Proceedings of the 1994 IE

49、EE ComputerSociety Symposium on Research in Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1994. 1428.11 Dolev D, Yao A. On the security of public key protocols. IEEE Transactions on Information Theory, 1983,29(2:198208.12 Syverson P. A taxonomy of replay attacks. In: Proceedings o

50、f the Computer Security Foundations Workshop. Los Alamitos: IEEEComputer Society Press, 1994. 187191.13 Wang GL, Qing SH, Zhou ZF. Some new attacks upon authentication protocols. Journal of Software, 2001,12(6:907913 (inChinese with English abstract.14 Clark J, Jacob J. A survey of authentication pr

51、otocol literature: Version 1.0. 1997. http:/www-users.cs.york.ac.uk/jac/under thelinkSecurity Protocols Review.15 Needham R, Schroeder M. Using encryption for authentication in large networks of computers. Communications of the ACM, 1978,21(12:993999.16 Lowe G. Breaking and fixing the Needham-Schroe

52、der public-key protocol using FDR. Software Concepts and Tools, 1996,17:93102.17 Nessett DM. A critique of the burrows, Abadi and Needham logic. ACM Operating Systems Review, 1990,24(2:3538.18 Syverson P. Knowledge, belief, and semantics in the analysis of cryptographic protocols. Journal of Compute

53、r Security, 1992,1(3:317334.19 Bieber P. A logic of communication in a hostile environment. In: Proceedings of the Computer Security Foundations Workshop III.Los Alamitos: IEEE Computer Society Press, 1990. 1422.20 Syverson P. Formal semantics for logics of cryptographic protocols. In: Proceedings o

54、f the Computer Security FoundationsWorkshop III. Los Alamitos: IEEE Computer Society Press, 1990. 3241.21 Rangan PV. An axiomatic basis of trust in distributed systems. In: Proceedings of the 1988 Symposium on Security and Privacy.Los Alamitos: IEEE Computer Society Press, 1988. 204211.22 Moser L. A

55、 logic of knowledge and belief for reasoning about computer security. In: Proceedings of the Computer SecurityFoundations Workshop II. Los Alamitos: IEEE Computer Society Press, 1989. 5763.23 Yahalom R, Klein B, Beth T. Trust relationships in secure systems: A distributed authentication perspective.

56、 In: Proceedings of the1993 IEEE Symposium on Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1993. 150164.24 Kindred D. Theory generation for security protocols Ph.D. Thesis. Pittsburgh: Department of Computer Science, Carnegie MellonUniversity, 1999.25 CCITT. CCITT draft recommendation X.509. The directory-authentication