田 園，惠 煌，李明楚

（大連理工大學(xué) 軟件學(xué)院，遼寧 大連 116620）

1 網(wǎng)絡(luò)安全協(xié)議設(shè)計(jì)與分析教學(xué)難點(diǎn)分析

網(wǎng)絡(luò)安全是當(dāng)代信息學(xué)科的重要領(lǐng)域之一，網(wǎng)絡(luò)安全協(xié)議的設(shè)計(jì)與分析則構(gòu)成網(wǎng)絡(luò)安全研究與教學(xué)活動(dòng)的核心內(nèi)容，同時(shí)對(duì)學(xué)生而言也是最為困難的內(nèi)容之一。即使對(duì)網(wǎng)絡(luò)技術(shù)與信息安全已經(jīng)具備一定基礎(chǔ)知識(shí)的高年級(jí)學(xué)生，甚至研究生，掌握網(wǎng)絡(luò)安全協(xié)議的正確分析方法仍然具有一定困難。概括起來，這些困難集中體現(xiàn)在以下層面：

（1）在安全概念層面，學(xué)生往往難以準(zhǔn)確抓住協(xié)議安全概念的要點(diǎn)，仔細(xì)分析起來，主要原因在于協(xié)議的安全性概念本質(zhì)上是從攻擊者的角度來表達(dá)的，包含對(duì)攻擊者掌握哪些信息和如何采取攻擊的一組合理假設(shè)。這些假設(shè)是對(duì)現(xiàn)實(shí)攻擊途徑的高度概括，例如身份認(rèn)證協(xié)議和密鑰交換協(xié)議中的攻擊模型［1－2］，正因?yàn)槿绱耍@些構(gòu)成協(xié)議安全概念的要素對(duì)大多數(shù)學(xué)生總顯得抽象、晦澀，難以準(zhǔn)確領(lǐng)悟其確切含義。

（2）在分析方法層面，由于安全協(xié)議具有交互性特點(diǎn)，學(xué)生不僅需要正確理解協(xié)議如何運(yùn)用基礎(chǔ)安全方案（如對(duì)稱和公鑰加密方案、數(shù)字簽名、散列方案），而且需要正確理解協(xié)議消息的時(shí)序關(guān)系，而這正是導(dǎo)致協(xié)議的安全分析復(fù)雜而微妙的主要方面［3－4］。很多網(wǎng)絡(luò)安全協(xié)議，即使所基于的基礎(chǔ)安全方案完美無瑕，但由于沒能正確地與消息時(shí)序關(guān)聯(lián)起來，也會(huì)導(dǎo)致不安全的結(jié)果［5－6］。對(duì)此要使學(xué)生達(dá)到較為充分的認(rèn)識(shí)，僅采用傳統(tǒng)的理論分析方法是十分不夠的，尤其不適合針對(duì)較為復(fù)雜的協(xié)議；而直接在真實(shí)的網(wǎng)絡(luò)環(huán)境中進(jìn)行實(shí)驗(yàn)，則難以真正觀察到完整的攻擊過程，且難以重復(fù)。因此2種傳統(tǒng)的教學(xué)途徑都不能很好地滿足教學(xué)要求。為此，需要為學(xué)生建立一種能針對(duì)較復(fù)雜協(xié)議、同時(shí)又表達(dá)直觀的協(xié)議建模與分析工具來支持教學(xué)，特別是支持學(xué)生的自主設(shè)計(jì)與分析。

我們采用基于軟件仿真的安全協(xié)議分析方法進(jìn)行教學(xué)，有效化解學(xué)生在學(xué)習(xí)網(wǎng)絡(luò)安全協(xié)議過程中所面臨的概念抽象、分析困難等障礙，取得了很好的成效。

2 基于仿真實(shí)驗(yàn)的網(wǎng)絡(luò)安全協(xié)議教學(xué)方法

學(xué)生在學(xué)習(xí)網(wǎng)絡(luò)安全協(xié)議時(shí)所面臨的2個(gè)主要障礙，一是安全性的概念（出于在理論上高度概括和精確的需要）較為抽象，二是缺乏有效而直觀的分析工具?；诜抡鎸?shí)驗(yàn)教授網(wǎng)絡(luò)安全協(xié)議，正是為了克服以上難點(diǎn)。從本質(zhì)上講，基于仿真實(shí)驗(yàn)的網(wǎng)絡(luò)安全協(xié)議教學(xué)方法是以協(xié)議的建模與仿真軟件為工具，通過計(jì)算來明確生成破壞協(xié)議安全目標(biāo)的攻擊途徑，以此為學(xué)生直觀地展示一個(gè)協(xié)議為什么不安全，或者通過生成一個(gè)不成功的攻擊途徑來向?qū)W生展示一個(gè)協(xié)議中的某些看似“多此一舉”的設(shè)計(jì)為什么十分必要。

該協(xié)議安全仿真與分析平臺(tái)從一項(xiàng)國家自然科學(xué)基金研究課題的研究成果演化而來，經(jīng)適當(dāng)改造和簡化應(yīng)用于教學(xué)實(shí)踐，在教學(xué)中具有以下特點(diǎn)：

（1）對(duì)網(wǎng)絡(luò)協(xié)議的表達(dá)與建模簡潔、直觀，特別適合于初學(xué)者。該平臺(tái)基于軟件工程領(lǐng)域常見的時(shí)序圖模型來表達(dá)協(xié)議，而不是像很多其他分析平臺(tái)那樣采用一階謂詞邏輯、π－演算等專門的形式符號(hào)體系［6－8］，特別直觀、易懂。

（2）使以往較為抽象的概念模型與協(xié)議的交互式過程具體化和形象化，便于學(xué)生準(zhǔn)確理解。學(xué)生可以通過開放的實(shí)驗(yàn)軟件自主觀察，并以實(shí)驗(yàn)觀察為基礎(chǔ)提出和發(fā)現(xiàn)問題。例如，學(xué)生可以有針對(duì)性地修改某些正確的協(xié)議方案，通過該平臺(tái)尋求攻擊仿真，以此驗(yàn)證原來的設(shè)計(jì)方案為什么正確，而那些不適當(dāng)?shù)男薷木烤瑰e(cuò)在哪里，這一點(diǎn)對(duì)學(xué)生積累經(jīng)驗(yàn)特別有價(jià)值。

（3）該仿真實(shí)驗(yàn)平臺(tái)所采用的分析算法先進(jìn)，具有充分的理論基礎(chǔ)，對(duì)任何不滿足安全目標(biāo)的協(xié)議一定可以發(fā)現(xiàn)至少一個(gè)攻擊途徑，從而保證仿真分析的結(jié)果正確、可靠［9］。

基于仿真實(shí)驗(yàn)的網(wǎng)絡(luò)安全協(xié)議教學(xué)方法，不是簡單補(bǔ)充傳統(tǒng)的理論分析型教學(xué)或僅為理論分析提供驗(yàn)證［4，10－12］，而是既為理論分析提供驗(yàn)證，同時(shí)也作為引導(dǎo)正確的理論分析與結(jié)論的啟發(fā)性工具。在這里，傳統(tǒng)的理論分析教學(xué)環(huán)節(jié)恰好成為分析仿真實(shí)驗(yàn)結(jié)果的一個(gè)步驟。我們的教學(xué)實(shí)踐表明后一種功效對(duì)學(xué)生更有價(jià)值，它也往往極大地激發(fā)起學(xué)生深入探索的興趣與熱情。

3 網(wǎng)絡(luò)安全協(xié)議仿真實(shí)驗(yàn)平臺(tái)的設(shè)計(jì)與實(shí)現(xiàn)

3.1 協(xié)議建模

網(wǎng)絡(luò)安全協(xié)議的建模包括2個(gè)組成部分：

第一是對(duì)協(xié)議本身工作流程的建模，包括每條協(xié)議消息的組成結(jié)構(gòu)（消息表達(dá)式）、消息的時(shí)序等要素。

第二是對(duì)協(xié)議安全目標(biāo)的建模，例如對(duì)身份認(rèn)證協(xié)議的抗欺詐目標(biāo)、密鑰交換協(xié)議的抗欺詐性和保密性目標(biāo)等。

第二類建模只與協(xié)議的類型有關(guān)，因此在該系統(tǒng)內(nèi)置地實(shí)現(xiàn)，用戶（教師和學(xué)生）在每次進(jìn)行仿真分析實(shí)驗(yàn)時(shí)只需針對(duì)具體協(xié)議完成第一類建模。

該軟件平臺(tái)的協(xié)議建?；跁r(shí)序圖來表達(dá)協(xié)議的工作流程，并具體圖形化界面，十分直觀和自然。圖1是以時(shí)序圖表達(dá)的著名的Otway－Rees三方認(rèn)證協(xié)議［8］的建模實(shí)例，垂直方向箭頭表示參與協(xié)議的進(jìn)程的時(shí)間序列事件，水平方向箭頭表示協(xié)議中的消息。

用戶在該軟件的界面窗口中首先創(chuàng)建消息流的框架，然后對(duì)每個(gè)消息指派消息表達(dá)式。消息表達(dá)式以一組約定的規(guī)則表達(dá)協(xié)議消息如何構(gòu)成與計(jì)算，例如Otway－Rees協(xié)議的消息表達(dá)式如下：

其中 M A B｛NaM A B｝KAS表示消息M1以分量M、A、B和密文｛NaM A B｝KAS順序組成（M是前綴），密文的明文又由分量Na、M、A、B順序組成并以密鑰KAS進(jìn)行對(duì)稱加密。用戶對(duì)每個(gè)消息分量的最小單元賦予類型（如Na是隨機(jī)數(shù)、A和B是身份標(biāo)志、KAS是密鑰），使系統(tǒng)在分析計(jì)算中按照相應(yīng)的規(guī)則進(jìn)行處理。

3.2 協(xié)議分析

該仿真平臺(tái)的安全分析方法是尋求對(duì)網(wǎng)絡(luò)安全協(xié)議的攻擊途徑，具體算法是基于系統(tǒng)內(nèi)部的一組基本攻擊模型（元模型）進(jìn)行組合演算，判定能否得到針對(duì)具體協(xié)議實(shí)例的完整的攻擊鏈。如果攻擊鏈存在，則進(jìn)一步計(jì)算出該攻擊鏈。

圖2是該分析平臺(tái)內(nèi)置的元攻擊模型，是安全分析（攻擊仿真）的出發(fā)點(diǎn)。每一個(gè)元模型表示現(xiàn)實(shí)攻擊者可能采取的某種計(jì)算步驟，例如元模型（a）表示攻擊者生成一條消息t，（b）表示攻擊者轉(zhuǎn)發(fā)一條消息g，（c）表示攻擊者轉(zhuǎn)發(fā)并復(fù)制一條消息g，（d）表示攻擊者截獲2條消息并加以合成，（e）表示攻擊者截獲1條消息并加以分割，（f）表示攻擊者生成密鑰K，（g）表示攻擊者以K作密鑰加密明文h，（h）表示攻擊者截獲1條密文并解密之。

顯然這些元模型十分直觀、現(xiàn)實(shí)，容易為學(xué)生所理解。該軟件通過一組計(jì)算規(guī)則（這些規(guī)則反映攻擊者的現(xiàn)實(shí)能力）將協(xié)議模型與元模型進(jìn)行組合，如果得到的最終流程圖達(dá)到了破壞協(xié)議安全目標(biāo)的目的，例如對(duì)密鑰交換協(xié)議，最終合成的流程圖中出現(xiàn)含保密密鑰K的子圖（f），就等價(jià)于找到了一條攻擊鏈，也就表明該協(xié)議不安全［6，9］。

以上概述了該軟件平臺(tái)實(shí)現(xiàn)協(xié)議安全仿真分析的要點(diǎn)，詳細(xì)的理論依據(jù)與算法分析參見參考文獻(xiàn)［9］。

4 教學(xué)案例

以上一節(jié)的Otway－Rees協(xié)議為例，我們基于該仿真分析平臺(tái)對(duì)網(wǎng)絡(luò)安全協(xié)議進(jìn)行教學(xué)實(shí)踐的典型步驟如下：

（1）對(duì)網(wǎng)絡(luò)協(xié)議進(jìn)行建模，方法如前，鼓勵(lì)學(xué)生自行完成，增加對(duì)協(xié)議方案細(xì)節(jié)的領(lǐng)會(huì)。

（2）指定安全分析目標(biāo)，如抗身份欺詐、密鑰保密及隱式確認(rèn)、密鑰保密及顯式確認(rèn)等。

（3）該平臺(tái)進(jìn)行自動(dòng)分析計(jì)算并輸出結(jié)果，例如圖3是對(duì)前述實(shí)例（圖1）所生成的一種攻擊鏈。

（4）讓學(xué)生自行解釋仿真輸出。這是關(guān)鍵性步驟，通過仔細(xì)理解攻擊者在該攻擊途徑中如何利用協(xié)議的各個(gè)環(huán)節(jié)與消息元素，學(xué)生能夠切實(shí)領(lǐng)悟到為什么某些看似“無關(guān)緊要”或 “保守”的設(shè)計(jì)細(xì)節(jié)，其實(shí)至關(guān)重要。

（5）在學(xué)生正確認(rèn)識(shí)到一個(gè)協(xié)議方案為什么不安全之后，鼓勵(lì)他們自主修改以前的設(shè)計(jì)，然后通過該平臺(tái)繼續(xù)實(shí)驗(yàn)，直到獲得滿意的方案。這一步也十分重要，通過這樣的反復(fù)失敗和改進(jìn)，有利于學(xué)生培養(yǎng)起對(duì)網(wǎng)絡(luò)安全協(xié)議如何達(dá)到安全目標(biāo)的正確認(rèn)識(shí)，而該仿真實(shí)驗(yàn)平臺(tái)正為此提供了一個(gè)高效而便捷的工具。

（6）針對(duì)正確的協(xié)議方案為學(xué)生進(jìn)行理論分析。由于前面積累了豐富的認(rèn)識(shí)，這一步對(duì)學(xué)生而言，已經(jīng)遠(yuǎn)不像面對(duì)單純的理論分析那樣較為難以理解。

攻擊鏈中的消息表達(dá)式如下：

5 結(jié)束語

隨著網(wǎng)絡(luò)安全協(xié)議越來越豐富，同時(shí)攻擊的途徑與手段也越來越復(fù)雜，對(duì)網(wǎng)絡(luò)安全工程師的協(xié)議設(shè)計(jì)與分析能力必然具有越來越高的要求，為此在教學(xué)上需要不斷開發(fā)與時(shí)俱進(jìn)的新方法、新手段，以滿足這一挑戰(zhàn)。我們分析了學(xué)生理解和掌握安全協(xié)議分析方面的主要困難，提出了基于仿真協(xié)議安全分析技術(shù)的教學(xué)方法，并結(jié)合所開發(fā)的基于消息代數(shù)算法的協(xié)議仿真分析平臺(tái)進(jìn)行安全協(xié)議的教學(xué)實(shí)踐。我們的教學(xué)實(shí)踐充分證實(shí)了該方法的成效，不僅有效降低了學(xué)生的學(xué)習(xí)障礙，而且有利于提高他們針對(duì)新型安全應(yīng)用的理解與分析能力。

（References）

［1］田園.網(wǎng)絡(luò)安全教程［M］.北京：人民郵電出版社，2009.

［2］劉天華，朱宏峰.安全協(xié)議模型與設(shè)計(jì)［M］.北京：科學(xué)出版社，2012.

［3］惠煌，田園.從攻擊的觀點(diǎn)講授信息安全技術(shù)［J］.高等教育研究，2008，17（8）：42－45.

［4］周敏，龔箭.計(jì)算機(jī)網(wǎng)絡(luò)安全實(shí)驗(yàn)教學(xué)研究［J］.實(shí)驗(yàn)技術(shù)與管理，2011，28（9）：145－148.

［5］Stallings W.Network Security and Cryptography［M］.5版.北京：電子工業(yè)出版社，2012.

［6］馮登國.安全協(xié)議：理論與實(shí)踐［M］.北京：清華大學(xué)出版社，2011.

［7］李建華.網(wǎng)絡(luò)安全協(xié)議的形式化分析與驗(yàn)證［M］.北京：機(jī)械工業(yè)出版社，2010.

［8］Stinson D E.密碼學(xué)理論與實(shí)踐［M］.馮登國，譯.3版.北京：電子工業(yè)出版社，2008.

［9］田園，王穎，金峰，等.基于剛性與相似性概念的密碼協(xié)議分析方法［J］.計(jì)算機(jī)學(xué)報(bào)，2009，32（4）：618－634.

［10］賀慧萍，榮彥，張?zhí)m.虛擬機(jī)軟件在網(wǎng)絡(luò)安全教學(xué)中的應(yīng)用［J］.實(shí)驗(yàn)技術(shù)與管理，2011，28（12）：112－115.

［11］鄒航，李粱，王柯柯，等.網(wǎng)絡(luò)信息安全實(shí)驗(yàn)平臺(tái)的創(chuàng)新設(shè)計(jì)與實(shí)現(xiàn)［J］.實(shí)驗(yàn)室研究與探索，2011，30（4）：61－65.

［12］唐海濤.網(wǎng)絡(luò)與信息安全實(shí)驗(yàn)教學(xué)平臺(tái)的構(gòu)建［J］.實(shí)驗(yàn)技術(shù)與管理，2010，27（10）：118－120.