網(wǎng)絡(luò)安全協(xié)議仿真實驗教學平臺設(shè)計與應(yīng)用

田 園，惠 煌，李明楚

（大連理工大學 軟件學院，遼寧 大連 116620）

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

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

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

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

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

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

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

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

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

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

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

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

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

3.1 協(xié)議建模

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

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

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

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

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

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

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

3.2 協(xié)議分析

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

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

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

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

4 教學案例

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

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

（2）指定安全分析目標，如抗身份欺詐、密鑰保密及隱式確認、密鑰保密及顯式確認等。

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

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

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

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

攻擊鏈中的消息表達式如下：

5 結(jié)束語

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

（References）

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

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

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

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

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

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

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

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

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

［10］賀慧萍，榮彥，張?zhí)m.虛擬機軟件在網(wǎng)絡(luò)安全教學中的應(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ò)與信息安全實驗教學平臺的構(gòu)建［J］.實驗技術(shù)與管理，2010，27（10）：118－120.