田 园,惠 煌,李明楚
(大连理工大学 软件学院,辽宁 大连 116620)
网络安全是当代信息学科的重要领域之一,网络安全协议的设计与分析则构成网络安全研究与教学活动的核心内容,同时对学生而言也是最为困难的内容之一。即使对网络技术与信息安全已经具备一定基础知识的高年级学生,甚至研究生,掌握网络安全协议的正确分析方法仍然具有一定困难。概括起来,这些困难集中体现在以下层面:
(1)在安全概念层面,学生往往难以准确抓住协议安全概念的要点,仔细分析起来,主要原因在于协议的安全性概念本质上是从攻击者的角度来表达的,包含对攻击者掌握哪些信息和如何采取攻击的一组合理假设。这些假设是对现实攻击途径的高度概括,例如身份认证协议和密钥交换协议中的攻击模型[1-2],正因为如此,这些构成协议安全概念的要素对大多数学生总显得抽象、晦涩,难以准确领悟其确切含义。
(2)在分析方法层面,由于安全协议具有交互性特点,学生不仅需要正确理解协议如何运用基础安全方案(如对称和公钥加密方案、数字签名、散列方案),而且需要正确理解协议消息的时序关系,而这正是导致协议的安全分析复杂而微妙的主要方面[3-4]。很多网络安全协议,即使所基于的基础安全方案完美无瑕,但由于没能正确地与消息时序关联起来,也会导致不安全的结果[5-6]。对此要使学生达到较为充分的认识,仅采用传统的理论分析方法是十分不够的,尤其不适合针对较为复杂的协议;而直接在真实的网络环境中进行实验,则难以真正观察到完整的攻击过程,且难以重复。因此2种传统的教学途径都不能很好地满足教学要求。为此,需要为学生建立一种能针对较复杂协议、同时又表达直观的协议建模与分析工具来支持教学,特别是支持学生的自主设计与分析。
我们采用基于软件仿真的安全协议分析方法进行教学,有效化解学生在学习网络安全协议过程中所面临的概念抽象、分析困难等障碍,取得了很好的成效。
学生在学习网络安全协议时所面临的2个主要障碍,一是安全性的概念(出于在理论上高度概括和精确的需要)较为抽象,二是缺乏有效而直观的分析工具。基于仿真实验教授网络安全协议,正是为了克服以上难点。从本质上讲,基于仿真实验的网络安全协议教学方法是以协议的建模与仿真软件为工具,通过计算来明确生成破坏协议安全目标的攻击途径,以此为学生直观地展示一个协议为什么不安全,或者通过生成一个不成功的攻击途径来向学生展示一个协议中的某些看似“多此一举”的设计为什么十分必要。
该协议安全仿真与分析平台从一项国家自然科学基金研究课题的研究成果演化而来,经适当改造和简化应用于教学实践,在教学中具有以下特点:
(1)对网络协议的表达与建模简洁、直观,特别适合于初学者。该平台基于软件工程领域常见的时序图模型来表达协议,而不是像很多其他分析平台那样采用一阶谓词逻辑、π-演算等专门的形式符号体系[6-8],特别直观、易懂。
(2)使以往较为抽象的概念模型与协议的交互式过程具体化和形象化,便于学生准确理解。学生可以通过开放的实验软件自主观察,并以实验观察为基础提出和发现问题。例如,学生可以有针对性地修改某些正确的协议方案,通过该平台寻求攻击仿真,以此验证原来的设计方案为什么正确,而那些不适当的修改究竟错在哪里,这一点对学生积累经验特别有价值。
(3)该仿真实验平台所采用的分析算法先进,具有充分的理论基础,对任何不满足安全目标的协议一定可以发现至少一个攻击途径,从而保证仿真分析的结果正确、可靠[9]。
基于仿真实验的网络安全协议教学方法,不是简单补充传统的理论分析型教学或仅为理论分析提供验证[4,10-12],而是既为理论分析提供验证,同时也作为引导正确的理论分析与结论的启发性工具。在这里,传统的理论分析教学环节恰好成为分析仿真实验结果的一个步骤。我们的教学实践表明后一种功效对学生更有价值,它也往往极大地激发起学生深入探索的兴趣与热情。
网络安全协议的建模包括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是密钥),使系统在分析计算中按照相应的规则进行处理。
该仿真平台的安全分析方法是寻求对网络安全协议的攻击途径,具体算法是基于系统内部的一组基本攻击模型(元模型)进行组合演算,判定能否得到针对具体协议实例的完整的攻击链。如果攻击链存在,则进一步计算出该攻击链。
图2是该分析平台内置的元攻击模型,是安全分析(攻击仿真)的出发点。每一个元模型表示现实攻击者可能采取的某种计算步骤,例如元模型(a)表示攻击者生成一条消息t,(b)表示攻击者转发一条消息g,(c)表示攻击者转发并复制一条消息g,(d)表示攻击者截获2条消息并加以合成,(e)表示攻击者截获1条消息并加以分割,(f)表示攻击者生成密钥K,(g)表示攻击者以K作密钥加密明文h,(h)表示攻击者截获1条密文并解密之。
显然这些元模型十分直观、现实,容易为学生所理解。该软件通过一组计算规则(这些规则反映攻击者的现实能力)将协议模型与元模型进行组合,如果得到的最终流程图达到了破坏协议安全目标的目的,例如对密钥交换协议,最终合成的流程图中出现含保密密钥K的子图(f),就等价于找到了一条攻击链,也就表明该协议不安全[6,9]。
以上概述了该软件平台实现协议安全仿真分析的要点,详细的理论依据与算法分析参见参考文献[9]。
以上一节的Otway-Rees协议为例,我们基于该仿真分析平台对网络安全协议进行教学实践的典型步骤如下:
(1)对网络协议进行建模,方法如前,鼓励学生自行完成,增加对协议方案细节的领会。
(2)指定安全分析目标,如抗身份欺诈、密钥保密及隐式确认、密钥保密及显式确认等。
(3)该平台进行自动分析计算并输出结果,例如图3是对前述实例(图1)所生成的一种攻击链。
(4)让学生自行解释仿真输出。这是关键性步骤,通过仔细理解攻击者在该攻击途径中如何利用协议的各个环节与消息元素,学生能够切实领悟到为什么某些看似“无关紧要”或 “保守”的设计细节,其实至关重要。
(5)在学生正确认识到一个协议方案为什么不安全之后,鼓励他们自主修改以前的设计,然后通过该平台继续实验,直到获得满意的方案。这一步也十分重要,通过这样的反复失败和改进,有利于学生培养起对网络安全协议如何达到安全目标的正确认识,而该仿真实验平台正为此提供了一个高效而便捷的工具。
(6)针对正确的协议方案为学生进行理论分析。由于前面积累了丰富的认识,这一步对学生而言,已经远不像面对单纯的理论分析那样较为难以理解。
攻击链中的消息表达式如下:
随着网络安全协议越来越丰富,同时攻击的途径与手段也越来越复杂,对网络安全工程师的协议设计与分析能力必然具有越来越高的要求,为此在教学上需要不断开发与时俱进的新方法、新手段,以满足这一挑战。我们分析了学生理解和掌握安全协议分析方面的主要困难,提出了基于仿真协议安全分析技术的教学方法,并结合所开发的基于消息代数算法的协议仿真分析平台进行安全协议的教学实践。我们的教学实践充分证实了该方法的成效,不仅有效降低了学生的学习障碍,而且有利于提高他们针对新型安全应用的理解与分析能力。
(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.