網絡安全協議仿真實驗教學平臺設計與應用

田 園，惠 煌，李明楚

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

1 網絡安全協議設計與分析教學難點分析

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

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

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

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

2 基于仿真實驗的網絡安全協議教學方法

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

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

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

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

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

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

3 網絡安全協議仿真實驗平臺的設計與實現

3.1 協議建模

網絡安全協議的建模包括2個組成部分：

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

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

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

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

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

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

3.2 協議分析

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

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

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

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

4 教學案例

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

（1）對網絡協議進行建模，方法如前，鼓勵學生自行完成，增加對協議方案細節的領會。

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

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

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

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

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

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

5 結束語

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

（References）

［1］田園.網絡安全教程［M］.北京：人民郵電出版社，2009.

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

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

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

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

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

［7］李建華.網絡安全協議的形式化分析與驗證［M］.北京：機械工業出版社，2010.

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

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

［10］賀慧萍，榮彥，張蘭.虛擬機軟件在網絡安全教學中的應用［J］.實驗技術與管理，2011，28（12）：112－115.

［11］鄒航，李粱，王柯柯，等.網絡信息安全實驗平臺的創新設計與實現［J］.實驗室研究與探索，2011，30（4）：61－65.

［12］唐海濤.網絡與信息安全實驗教學平臺的構建［J］.實驗技術與管理，2010，27（10）：118－120.