基于avispa的ms-chapv2协议形式化分析

基于 AVISPA 的 MS-CHAPv2 协议形式化分析 摘要：AVISPA 安全协议分析工具是基于模型检测技术的一套完整、标准的形式化自动分析工具； 并利用AVISPA提供的WEB接口对CHAPv2的安全性进行了形式化分析，实验表明CHAPv2达到了预期的 安全目标。 关键词：AVISPA 协议形式化分析 CHAPv2 1 引言 1.1 背景 安全协议也称作密码协议,是以密码学为基础的消息交换协议其目的 是在网络环境中提供各种安全服务。它是许多分布系统安全的基础。确保 这些协议能够安全地运行是极为重要的。虽然安全协议中仅仅进行很少的 几组消息传输，但是其中的每一消息的组都是经过巧妙设计的，而且这些 消息之间有着复杂的相互作用和制约。在设计密码协议时，人们通常采用 不同的密码体制。而且所设计的协议也常常应用于许多不同的通信环境。 但是，现有的 许多协议在设计上普遍存在着某些安全缺陷。造成认证协议 存在安全漏洞的原因有很多，我们通过对协议的安全性进行分析，可以发 现协议的设计漏洞，反过来可以进一步指导协议的设计。 目前已经有很多研究安全协议的理论和方法,其中比较著名的有可证 明安全理论、 BAN 逻辑、串空间模型理论以及模型检测和定理证明的方法 等。 模型 检测作为形式化分析安全理论方法的一种,有着自动化和提供反 例等诸多优点。 1.2 模型检测方法 模型检测方法，考虑的是协议的有限多种行为，检测它们满足一些正 确条件它更适合于去发现协议的攻击，而并非去证明协议的正确性。 模型检测有以下特点： (1)关于 协议 操作行为的有限状态系统被刻画为有限状态迁移系统这 个系统的状态取决于与环境的交互，满足一定条件就迁移到另一个状 态这些条件被标记到迁移的边上这个系统称为标记迁移系统(Labelled Transitive System，LTS)。 (2)在每个状态上，有某些性质被满足，这些性质被描述为一个(古典逻 辑或者时态等逻辑)公式。 (3)与定理 证 明一样，系统要满足的性质也被刻画为逻辑公式 (4)用自 动的手段 检测上述的性质是否在系统的每个轨迹(trace)上都被 满足这里的 轨迹是指系统的一个可能迁移路径。 形式上说，假如一个系统为 S，期望的系 统性质表达为逻辑公式 ，那 么模型检测就是验证是否 S 满足 。通常把 S 满足 表示为 S|= 。 模型检测的方法完全是自动化的，这是该方法的优点但是，因为协议 的行为是潜在无限的，而模型检测的方法只能够处理有限状态的系统，故 而决定了这个方法的不完善性，即在实际应用过程中，一定要对检测的范 围加以限制。 2 模型检测工具 AVISPA 模型检测工具的代表工具就是 AVISPA，它的前身是欧洲 AVISS 项目 中由 ETH Zurich 的信息安全 组开发的 HLPSL/ OFMC，后来得到了不断地 完善，现在的 AVISPA 集成了 OFMC，CL,SATMC 和 TA4SP 等后台工具。 AVISPA 以高 级协议规范语言（High Level Protocol Specification Language，HLPSL）作为输入，通过翻译器 HLPS2IF 将 HLPSL 转换为中间 格式（Intermediate Format，IF），然后使用模型检测器（On-the-Fly Model- Checker，OFMC）来验证 。 2.1 功能架构 AVISPAN 工具提供了一套建立和分析协议安全的应用软件。协议用 高级协议说明语言 HLPSL 来建模，以描述协议 和协议的的安全性质。其结 构图如下所示： 图 1.1 AVISPA 的基本结构示意图 HLPSL 是一种丰富的、模块化的、基于角色的形式语言，提供了一套 包括控制流模式、数据结构、可选择入侵者模式、复杂的安全目标以及不同 的密码初始值和代数性质的说明。这些特性能够使 HLPSL 很好的描述现 代的、工业 化规模的协议。而且， HLPSL 不 仅支持基于时间片段的逻辑行 为的公开语义，还支持基于重写的中间形式化语言 IF。IF 是一个比 HLPSL 低级的语言，可以被 AVISPAN 工具的后台直接使用。 HLPSL2IF 自动将 HLPSL 语言翻译成 IF 语言，并将它们依次反馈给 测试后端。 AVISPA 使用了 4 种后端分析工具来解决安全协议的确认问题： （1）OFMC(On-the-fly Model-Checker)：基于 IF 语言需求驱使的描述， 通过探测系统的变迁，OFMC 能够完成 协议的篡改和有限制的确认。 OFMC 支持密码操作的代数性质的规范，以及各种 协议模型。 （2）CL-AtSe（Constraint-Logic-based Attack Searcher）：CL-AtSe 通过强 大的简化探测法和冗余排除技术来执行协议。它建立在模型化的方式上， 并且是对密码操作的代数性质的延伸。CL-AtSe 支持输入缺陷探测和处理 消息串联。 （3）SATMC（SAT-based Model-Checker）：SATMC 建立在通过 IF 语言 描述的，有限域上变迁关系的编码的公式，初始状态和状态集合的说明代 表了整个协议的安全特性。此公式将反馈给 SAT 状态推导机，并且建立的 任何一个模型都将转化为一个攻击事件。 （4）TA4SP(Tree Automata based on AutomaticApproximations for the Analysis of Security Protocols)：TA4SP 通过树形语言和重写机制估计入侵者 的知识。根据不同的保密特性，TA4SP 能 够判断一个协议是否有缺陷，或 者是几个会合的对话后是否安全。 2.2 使用方法 使用 AVISPA 协议分析工具对安全协议进行分析的一般性过程如下： 首先，将安全协议编码为某种形式化描述语言；然后，根据协议目标和安全 属性，给出不同的消息成分的类型；最后，根据分析工作的结果判断协议是 否安全，是否达到了预期目标。 （1）分析安全协议，并根据 HLPSL 语法，将协议进行建模，编辑成后 缀名为“.hlpsl”的文件， （2）将 HLPSL 文件导入，利用 HLPSL 编辑 器将 HLPSL 文件转换为 后缀名为“.if” 的中间文件； （3）将 IF 文件导入，利用选定的后端分析工具将 IF 文件分析得到后 缀名“.atk”的结果文件，通 过结果文件可以分析得出该协议的安全性、目标、 攻击轨迹等各种细节。 3 MS-CHAPv2 协议形式化分析 3.1 MS-CHAPv2 协议简介 CHAP( Challenge-Handshake Authentication Protocol),即质询- 握手鉴 别协议, 通常被嵌入到其它协议中, 在无线 网络通信、PSTN 或 ISDN 的电 路交换连接、 拨入连接或专有连接完成身份鉴别功能。作为一种被广泛应 用的身份鉴别协议, MSCHAP 协议在 RFC19941 中有详细描述。MS- CHAP 协议采用加密验证机制, 其主要的工作过程如下: 1) 客 户端向服务器发出一个质询请求; 2) 服 务器返回一个随机质询数; 3) 客户端根据口令 HASH 值生成对应密钥, 对随机质询数加密, 发 送到服务器作为响应; 4) 服 务器在数据库中查询HASH 值生成对应密钥并对响应解密, 将 所得与原来发送的质询数作比较。若匹配, 则鉴别通过。MS-CHAP4 对 PAP 进行了改进, 不再直接通过链路发送明文口令 , 而是发送被口令 HASH 值加密 质询数。采用这种方式服务器端将只存储经过HASH 算法加 密的用户口令而不是明文口令, 这样就能够提供进一步的安全保障。MS- CHAP 为每一次验证任意生成一个随机质询数来防止受到重放攻击( replay attack)、字典攻 击 。 由于有人对MS-PPTP进行了密码分析，并将其弱点公布于众， Microsoft 对MS-PPTP中所使用的协议进行了改进。新版本称为MS-CHAPv2。 MS-CHAPv2主要改变如下： (1)LAN Manager hash不再与Windows NT hash一起发送； (2)引入了 对 server的认证方案，防止恶意的server的伪装； (2)MS-CHAPv2使用一个单一的改变口令包，防止了针对MS-CHAP失败包 的主动攻击。 MPPE在每个方向上使用一个唯一的密 钥。这样 可以防止对每一方向 的流量进行XOR，从而去掉密 码的影响而实 施的攻击。 这些改变确实纠正原来协议中的主要安全弱点：对LAN Manager hash 函数 的使用及使用同一输出反馈加密密钥多次。但是，许多安全问题依然存在， 例如客户如何保护自己，加密密钥与用户口令熵相同，给攻击者进行加密 比较攻击留有太多的信息。 3.2 协议自然语言描述 B：服 务 器 A：客户端 k(A,B)：A 与 B 的共享密钥 Na 客 户端生成的随机数 Nb 客户端生成的随机数 1. A - B : A 2. B - A : Nb 3. 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）客户端（协议的发起者） role chap_Init (A,B : agent,代理 Kab : symmetric_key,对称密钥 H : hash_func,哈希函数 Snd, Rcv : channel(dy)信道 played_by A 定义： local State : nat, Na, Nb : text const sec_kab1 : protocol_id init State := 0 （2）服务器（协议的接收者） role chap_Resp (B,A : agent, 代理 Kab : symmetric_key, 对称密钥 H : hash_func, 哈希函数 Snd, Rcv : channel(dy) 信道 played_by B 定义： local State : nat, Na, Nb : text const sec_kab2 : protocol_id init State := 0 （3）角色会话提取 role session(A,B : agent,代理 Kab : symmetric_key,对称密钥 H : hash_func)哈希函数 定义： local SA, SB, RA, RB: channel (dy) composition chap_Init(A, B, Kab, H, SA, RA) / chap_Resp(B, A, Kab, H, SB, RB) 转换规则： （1）客户端： （2）服务器： 攻击者描述： role environment() 定义： const a, b : agent, kab, kai, kbi : symmetric_key, h : hash_func, na, nb : protocol_id 攻击者知识= a, b, h, kai, kbi composition session(a,b,kab,h) / session(a,i,kai,h) / session(b,i,kbi,h) 3.4 安全目标 共享密钥 sec_kab1, sec_kab2 的保密性 客户端对服务器随机数 nb 的验证 服务器对客户端随机数 na 的验证 4 AVISPA 分析 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/Response Authentication Protocol, version 2 % PURPOSE: % Mutual authentication between a server and a client who share a password. % CHAPv2 is the authentication protocol for the Point-to-Point Tunneling Protocol % suite (PPTP). % REFERENCE: % citeRFC2759 % MODELER: %beginitemize %item Haykal Tej, Siemens CT IC 3, 2003 %item Paul Hankes Drielsma, ETH Z“urich %enditemize % % ALICE_BOB: % We assume that the server verb!B! and client verb!A! share % password verb!k(A,B)! in advance. The server and client generate % nonces verb!Nb! and verb!Na!, respectively. %beginverbatim % 1. A - B : A % 2. B - A : Nb % 3. A - B : Na,H(k(A,B),(Na,Nb,A) % 4. B - A : H(k(A,B),Na) %endverbatim % % LIMITATIONS: % %Issues abstracted from: %beginitemize %item Message structure: As is standard, we abstract away from the concrete details % of message structure such as bit lengths, etc. What is left after this abstraction % contains several redundancies, however (at least in the Dolev-Yao model). % We therefore eliminate these redundancies, retaining the core of the data % dependencies of the protocol. %enditemize % % PROBLEMS: 3 % CLASSIFICATION: G1, G2, G12 % ATTACKS: None % % NOTES: % A cryptanalysis of this protocol in its full complexity can be found % inciteschneier99cryptanalysis. % % % %HLPSL: role chap_Init (A,B : agent, Kab : symmetric_key, H : hash_func, Snd, Rcv: channel(dy) played_by A def= local State : nat, Na, Nb : text const sec_kab1 : protocol_id init State := 0 transition 1. State = 0 / Rcv(start) =| State := 1 / Snd(A) 2. State = 1 / Rcv(Nb) =| State := 2 / Na := new() / Snd(Na.H(Kab.Na.Nb.A) / witness(A,B,na,Na) / secret(Kab,sec_kab1,A,B) 3. State = 2 / Rcv(H(Kab.Na) =| State := 3 / request(A,B,nb,Nb) end role % role chap_Resp (B,A : agent, Kab : symmetric_key, H: hash_func, Snd, Rcv: channel(dy) played_by B def= local State : nat, Na, Nb : text const sec_kab2 : protocol_id init State := 0 transition 1. State = 0 / Rcv(A) =| State := 1 / Nb := new() / Snd(Nb) / witness(B,A,nb,Nb) 2. State = 1 / Rcv(Na.H(Kab.Na.Nb.A) =| State := 2 / Snd(H(Kab.Na) / request(B,A,na,Na) / secret(Kab,sec_kab2,A,B) end role % role session(A,B: agent, Kab: symmetric_key, H: hash_func) def= local SA, SB, RA, RB: channel (dy) composition chap_Init(A, B, Kab, H, SA, RA) / chap_Resp(B, A, Kab, H, SB, RB) end role % role environment() def= const a, b : agent, kab, kai, kbi : symmetric_key, h : hash_func, na, nb : protocol_id intruder_knowledge = a, b, h, kai, kbi composition session(a,b,kab,h) / session(a,i,kai,h) / session(b,i,kbi,h) end role % % goal %secrecy of the shared key secrecy_of sec_kab1, sec_kab2 % Addresses G12 %CHAP_Init authenticates CHAP_Resp on nb authentication_on nb % Addresses G1, G2 %CHAP_Resp authenticates CHAP_Init on na authentication_on na % Addresses G1, G2 end goal 附录 2 IF 语言描述： % IF specification of /home/avispa/web-interface-computation/./tempdir/workfileYicrwd section signature: state_chap_Resp: agent * agent * symmetric_key * hash_func * nat * text * text * set(agent) * nat - fact state_chap_Init: agent * agent * symmetric_key * hash_func * nat * text * text * set(agent) * nat - fact section types: sec_kab2, nb, na, sec_kab1: protocol_id Na, Nb, Dummy_Nb, Dummy_Na, dummy_nonce: text set_79, set_77, set_76, set_74, set_69, set_61: set State, 9, 6, 3, 4, SID, 2, 1, 0, Dummy_State, SID2, SID1: nat Set_37, Dummy_Set_37, Set_21, Dummy_Set_21, ASGoal: set(agent) start, MGoal: message H, h: hash_func a, b, B, A, Dummy_A, A2Goal, A1Goal, i: agent Kab, kab, kai, kbi: symmetric_key section inits: initial_state init1 := iknows(start). iknows(a). iknows(b). iknows(h). iknows(kai). iknows(kbi). iknows(i). state_chap_Init(a,b,kab,h,0,dummy_nonce,dummy_nonce,set_61,3). state_chap_Resp(b,a,kab,h,0,dummy_nonce,dummy_nonce,set_69,4). state_chap_Init(a,i,kai,h,0,dummy_nonce,dummy_nonce,set_74,6). state_chap_Init(b,i,kbi,h,0,dummy_nonce,dummy_nonce,set_77,9) section rules: step step_0 (A,B,Kab,H,Na,Nb,Set_21,SID) := state_chap_Init(A,B,Kab,H,0,Na,Nb,Set_21,SID). iknows(start) = state_chap_Init(A,B,Kab,H,1,Na,Nb,Set_21,SID). iknows(A) step step_1 (A,B,Kab,H,Dummy_Na,Dummy_Nb,Dummy_Set_21,SID,Na,Nb) := state_chap_Init(A,B,Kab,H,1,Dummy_Na,Dummy_Nb,Dummy_Set_21,SID). iknows(Nb) =exists Na= state_chap_Init(A,B,Kab,H,2,Na,Nb,Dummy_Set_21,SID). iknows(pair(Na,apply(H,pair(Kab,pair(Na,pair(Nb,A). witness(A,B,na,Na). secret(Kab,sec_kab1,Dummy_Set_21). contains(A,Dummy_Set_21). contains(B,Dummy_Set_21) step step_2 (A,B,Kab,H,Na,Nb,Set_21,SID) := state_chap_Init(A,B,Kab,H,2,Na,Nb,Set_21,SID). iknows(apply(H,pair(Kab,Na) = state_chap_Init(A,B,Kab,H,3,Na,Nb,Set_21,SID). request(A,B,nb,Nb,SID) step step_3 (B,Dummy_A,Kab,H,Na,Dummy_Nb,Set_37,SID,A,Nb) := state_chap_Resp(B,Dummy_A,Kab,H,0,Na,Dummy_Nb,Set_37,SID). iknows(A) =exists Nb= state_chap_Resp(B,A,Kab,H,1,Na,Nb,Set_37,SID). iknows(Nb). witness(B,Dummy_A,nb,Nb) step step_4 (B,A,Kab,H,Dummy_Na,Nb,Dummy_Set_37,SID,Na) := state_chap_Resp(B,A,Kab,H,1,Dummy_Na,Nb,Dummy_Set_37,SID). iknows(pair(Na,apply(H,pair(Kab,pair(Na,pair(Nb,A) = state_chap_Resp(B,A,Kab,H,2,Na,Nb,Dummy_Set_37,SID). iknows(apply(H,pair(Kab,Na). request(B,A,na,Na,SID). secret(Kab,sec_kab2,Dummy_Set_37). contains(A,Dummy_Set_37). contains(B,Dummy_Set_37) section properties: property secrecy_of_sec_kab1 (MGoal,ASGoal) := (secret(MGoal,sec_kab1,ASGoal) / iknows(MGoal) = contains(i,ASGoal) property secrecy_of_sec_kab2 (MGoal,ASGoal) := (secret(MGoal,sec_kab2,ASGoal) / iknows(MGoal) = contains(i,ASGoal) property authentication_on_nb (A1Goal,A2Goal,MGoal,SID,SID1,SID2) := (request(A1Goal,A2Goal,nb,MGoal,SID) / equal(A2Goal,i) = witness(A2Goal,A1Goal,nb,MGoal) / (request(A1Goal,A2Goal,nb,MGoal,SID1) / request(A1Goal,A2Goal,nb,MGoal,SID2) / equal(A2Goal,i)