基于AVISPA的MS-CHAPv2协议形式化分析

基于AVISPA的MS-CHAPv2协议形式化分析摘要：AVISPA安全协议分析工具是基于模型检测技术的一套完整、标准的形式化自动分析工具；并利用AVISPA提供的WEB接口对CHAPv2的安全性进行了形式化分析，实验表明CHAPv2达到了预期的安全目标。关键词：AVISPA协议形式化分析CHAPv21引言1.1背景安全协议也称作密码协议,是以密码学为基础的消息交换协议其目的是在网络环境中提供各种安全服务。它是许多分布系统安全的基础。确保这些协议能够安全地运行是极为重要的。虽然安全协议中仅仅进行很少的几组消息传输，但是其中的每一消息的组都是经过巧妙设计的，而且这些消息之间有着复杂的相互作用和制约。在设计密码协议时，人们通常采用不同的密码体制。而且所设计的协议也常常应用于许多不同的通信环境。但是，现有的许多协议在设计上普遍存在着某些安全缺陷。造成认证协议存在安全漏洞的原因有很多，我们通过对协议的安全性进行分析，可以发现协议的设计漏洞，反过来可以进一步指导协议的设计。目前已经有很多研究安全协议的理论和方法,其中比较著名的有可证明安全理论、BAN逻辑、串空间模型理论以及模型检测和定理证明的方法等。模型检测作为形式化分析安全理论方法的一种,有着自动化和提供反例等诸多优点。1.2模型检测方法模型检测方法，考虑的是协议的有限多种行为，检测它们满足一些正确条件．它更适合于去发现协议的攻击，而并非去证明协议的正确性。模型检测有以下特点：(1)关于协议操作行为的有限状态系统被刻画为有限状态迁移系统．这个系统的状态取决于与环境的交互，满足一定条件就迁移到另一个状态．这些条件被标记到迁移的边上．这个系统称为标记迁移系统(LabelledTransitiveSystem，LTS)。(2)在每个状态上，有某些性质被满足，这些性质被描述为一个(古典逻辑或者时态等逻辑)公式。(3)与定理证明一样，系统要满足的性质也被刻画为逻辑公式．(4)用自动的手段检测上述的性质是否在系统的每个轨迹(trace)上都被满足．这里的轨迹是指系统的一个可能迁移路径。形式上说，假如一个系统为S，期望的系统性质表达为逻辑公式，那么模型检测就是验证是否S满足。通常把S满足表示为S|=。模型检测的方法完全是自动化的，这是该方法的优点．但是，因为协议的行为是潜在无限的，而模型检测的方法只能够处理有限状态的系统，故而决定了这个方法的不完善性，即在实际应用过程中，一定要对检测的范围加以限制。2模型检测工具AVISPA模型检测工具的代表工具就是AVISPA，它的前身是欧洲AVISS项目中由ETHZurich的信息安全组开发的HLPSL/OFMC，后来得到了不断地完善，现在的AVISPA集成了OFMC，CL,SATMC和TA4SP等后台工具。AVISPA以高级协议规范语言（HighLevelProtocolSpecificationLanguage，HLPSL）作为输入，通过翻译器HLPS2IF将HLPSL转换为中间格式（IntermediateFormat，IF），然后使用模型检测器（On-the-FlyModel-Checker，OFMC）来验证。2.1功能架构AVISPAN工具提供了一套建立和分析协议安全的应用软件。协议用高级协议说明语言HLPSL来建模，以描述协议和协议的的安全性质。其结构图如下所示：图1.1AVISPA的基本结构示意图HLPSL是一种丰富的、模块化的、基于角色的形式语言，提供了一套包括控制流模式、数据结构、可选择入侵者模式、复杂的安全目标以及不同的密码初始值和代数性质的说明。这些特性能够使HLPSL很好的描述现代的、工业化规模的协议。而且，HLPSL不仅支持基于时间片段的逻辑行为的公开语义，还支持基于重写的中间形式化语言IF。IF是一个比HLPSL低级的语言，可以被AVISPAN工具的后台直接使用。HLPSL2IF自动将HLPSL语言翻译成IF语言，并将它们依次反馈给测试后端。AVISPA使用了4种后端分析工具来解决安全协议的确认问题：（1）OFMC(On-the-flyModel-Checker)：基于IF语言需求驱使的描述，通过探测系统的变迁，OFMC能够完成协议的篡改和有限制的确认。OFMC支持密码操作的代数性质的规范，以及各种协议模型。（2）CL-AtSe（Constraint-Logic-basedAttackSearcher）：CL-AtSe通过强大的简化探测法和冗余排除技术来执行协议。它建立在模型化的方式上，并且是对密码操作的代数性质的延伸。CL-AtSe支持输入缺陷探测和处理消息串联。（3）SATMC（SAT-basedModel-Checker）：SATMC建立在通过IF语言描述的，有限域上变迁关系的编码的公式，初始状态和状态集合的说明代表了整个协议的安全特性。此公式将反馈给SAT状态推导机，并且建立的任何一个模型都将转化为一个攻击事件。（4）TA4SP(TreeAutomatabasedonAutomaticApproximationsfortheAnalysisofSecurityProtocols)：TA4SP通过树形语言和重写机制估计入侵者的知识。根据不同的保密特性，TA4SP能够判断一个协议是否有缺陷，或者是几个会合的对话后是否安全。2.2使用方法使用AVISPA协议分析工具对安全协议进行分析的一般性过程如下：首先，将安全协议编码为某种形式化描述语言；然后，根据协议目标和安全属性，给出不同的消息成分的类型；最后，根据分析工作的结果判断协议是否安全，是否达到了预期目标。（1）分析安全协议，并根据HLPSL语法，将协议进行建模，编辑成后缀名为“.hlpsl”的文件，（2）将HLPSL文件导入，利用HLPSL编辑器将HLPSL文件转换为后缀名为“.if”的中间文件；（3）将IF文件导入，利用选定的后端分析工具将IF文件分析得到后缀名“.atk”的结果文件，通过结果文件可以分析得出该协议的安全性、目标、攻击轨迹等各种细节。3MS-CHAPv2协议形式化分析3.1MS-CHAPv2协议简介CHAP(Challenge-HandshakeAuthenticationProtocol),即质询-握手鉴别协议,通常被嵌入到其它协议中,在无线网络通信、PSTN或ISDN的电路交换连接、拨入连接或专有连接完成身份鉴别功能。作为一种被广泛应用的身份鉴别协议,MSCHAP协议在RFC1994[1]中有详细描述。MS-CHAP协议采用加密验证机制,其主要的工作过程如下:1)客户端向服务器发出一个质询请求;2)服务器返回一个随机质询数;3)客户端根据口令HASH值生成对应密钥,对随机质询数加密,发送到服务器作为响应;4)服务器在数据库中查询HASH值生成对应密钥并对响应解密,将所得与原来发送的质询数作比较。若匹配,则鉴别通过。MS-CHAP[4]对PAP进行了改进,不再直接通过链路发送明文口令,而是发送被口令HASH值加密质询数。采用这种方式服务器端将只存储经过HASH算法加密的用户口令而不是明文口令,这样就能够提供进一步的安全保障。MS-CHAP为每一次验证任意生成一个随机质询数来防止受到重放攻击(replayattack)、字典攻击。由于有人对MS-PPTP进行了密码分析，并将其弱点公布于众，Microsoft对MS-PPTP中所使用的协议进行了改进。新版本称为MS-CHAPv2。MS-CHAPv2主要改变如下：(1)LANManagerhash不再与WindowsNThash一起发送；(2)引入了对server的认证方案，防止恶意的server的伪装；(2)MS-CHAPv2使用一个单一的改变口令包，防止了针对MS-CHAP失败包的主动攻击。MPPE在每个方向上使用一个唯一的密钥。这样可以防止对每一方向的流量进行XOR，从而去掉密码的影响而实施的攻击。这些改变确实纠正原来协议中的主要安全弱点：对LANManagerhash函数的使用及使用同一输出反馈加密密钥多次。但是，许多安全问题依然存在，例如客户如何保护自己，加密密钥与用户口令熵相同，给攻击者进行加密比较攻击留有太多的信息。3.2协议自然语言描述B：服务器A：客户端k(A,B)：A与B的共享密钥Na客户端生成的随机数Nb客户端生成的随机数1.A-B:A2.B-A:Nb3.A-B:Na,H(k(A,B),(Na,Nb,A))4.B-A:H(k(A,B),Na)3.2HLPSL形式化语言描述：3.2.1角色提取通过对MS-CHAP协议分析,客户端和服务器的两个角色被提取。根据协议消息的来源、消息的内容和参与主体,客户端和服务器的角色提取表示为:（1）客户端（协议的发起者）rolechap_Init(A,B:agent,代理Kab:symmetric_key,对称密钥H:hash_func,哈希函数Snd,Rcv:channel(dy))信道played_byA定义：localState:nat,Na,Nb:textconstsec_kab1:protocol_idinitState:=0（2）服务器（协议的接收者）rolechap_Resp(B,A:agent,代理Kab:symmetric_key,对称密钥H:hash_func,哈希函数Snd,Rcv:channel(dy))信道played_byB定义：localState:nat,Na,Nb:textconstsec_kab2:protocol_idinitState:=0（3）角色会话提取rolesession(A,B:agent,代理Kab:symmetric_key,对称密钥H:hash_func)哈希函数定义：localSA,SB,RA,RB:channel(dy)compositionchap_Init(A,B,Kab,H,SA,RA)/\chap_Resp(B,A,Kab,H,SB,RB)转换规则：（1）客户端：（2）服务器：攻击者描述：roleenvironment()定义：consta,b:agent,kab,kai,kbi:symmetric_key,h:hash_func,na,nb:protocol_id攻击者知识={a,b,h,kai,kbi}compositionsession(a,b,kab,h)/\session(a,i,kai,h)/\session(b,i,kbi,h)3.4安全目标共享密钥sec_kab1,sec_kab2的保密性客户端对服务器随机数nb的验证服务器对客户端随机数na的验证4AVISPA分析MS-CHAPv2协议利用AVISPA提供的WEB接口可以很方便地分析MS-CHAPv2协议，下面介绍实验过程：4.1实验过程（1）选择一个待测试的MS-CHAPv2协议：（2）点击执行：（3）查看HLPSL和IF的语言描述4.2实验结果（1）查看OMFC结果分析（2）查看CL-AtSe结果分析（3）查看SATMC结果分析（4）查看TA4SP结果分析4.3实验结论通过这四种后台检测工具分析得出chapv2协议达到了预期的安全目标，不存在致命的安全缺陷。附录1、HLPSL语言描述%%PROTOCOL:(MS-)CHAPv2%%Challenge/ResponseAuthenticationProtocol,version2%%PURPOSE:%%Mutualauthenticationbetweenaserverandaclientwhoshareapassword.%%CHAPv2istheauthenticationprotocolforthePoint-to-PointTunnelingProtocol%%suite(PPTP).%%REFERENCE:%%\cite{RFC2759}%%MODELER:%%\begin{itemize}%%\itemHaykalTej,SiemensCTIC3,2003%%\itemPaulHankesDrielsma,ETHZ\urich%%\e