田 園，惠 煌，李明楚

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

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

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

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

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

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

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

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

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

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

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

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

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

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

3.1 協(xié)議建模

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

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

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

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

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

用戶在該軟件的界面窗口中首先創(chuàng)建消息流的框架，然后對每個消息指派消息表達(dá)式。消息表達(dá)式以一組約定的規(guī)則表達(dá)協(xié)議消息如何構(gòu)成與計算，例如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)行對稱加密。用戶對每個消息分量的最小單元賦予類型（如Na是隨機數(shù)、A和B是身份標(biāo)志、KAS是密鑰），使系統(tǒng)在分析計算中按照相應(yīng)的規(guī)則進(jìn)行處理。

3.2 協(xié)議分析

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

圖2是該分析平臺內(nèi)置的元攻擊模型，是安全分析（攻擊仿真）的出發(fā)點。每一個元模型表示現(xiàn)實攻擊者可能采取的某種計算步驟，例如元模型（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)實，容易為學(xué)生所理解。該軟件通過一組計算規(guī)則（這些規(guī)則反映攻擊者的現(xiàn)實能力）將協(xié)議模型與元模型進(jìn)行組合，如果得到的最終流程圖達(dá)到了破壞協(xié)議安全目標(biāo)的目的，例如對密鑰交換協(xié)議，最終合成的流程圖中出現(xiàn)含保密密鑰K的子圖（f），就等價于找到了一條攻擊鏈，也就表明該協(xié)議不安全［6，9］。

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

4 教學(xué)案例

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

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

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

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

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

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

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

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

5 結(jié)束語

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

（References）

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

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

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

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

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

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

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

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

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

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

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

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