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

1、基于AVISPA的MS-CHAPv2协议形式化分析摘要：AVISPA 安全协议分析工具是基于模型检测技术的一套完整、标准的形式化自动分析工具；并利用AVISPA提供的WEB接口对CHAPv2的安全性进行了形式化分析，实验表明CHAPv2达到了预期的安全目标。关键词：AVISPA 协议形式化分析 CHAPv21 引言1.1背景安全协议也称作密码协议,是以密码学为基础的消息交换协议其目的是在网络环境中提供各种安全服务。它是许多分布系统安全的基础。确保这些协议能够安全地运行是极为重要的。虽然安全协议中仅仅进行很少的几组消息传输，但是其中的每一消息的组都是经过巧妙设计的，而且这些消息之间有着复杂的相互

2、作用和制约。在设计密码协议时，人们通常采用不同的密码体制。而且所设计的协议也常常应用于许多不同的通信环境。但是，现有的许多协议在设计上普遍存在着某些安全缺陷。造成认证协议存在安全漏洞的原因有很多，我们通过对协议的安全性进行分析，可以发现协议的设计漏洞，反过来可以进一步指导协议的设计。目前已经有很多研究安全协议的理论和方法,其中比较著名的有可证明安全理论、BAN逻辑、串空间模型理论以及模型检测和定理证明的方法等。 模型检测作为形式化分析安全理论方法的一种,有着自动化和提供反例等诸多优点。1.2模型检测方法模型检测方法，考虑的是协议的有限多种行为，检测它们满足一些正确条件它更适合于去发现协议的攻击

3、，而并非去证明协议的正确性。模型检测有以下特点：(1)关于协议操作行为的有限状态系统被刻画为有限状态迁移系统这个系统的状态取决于与环境的交互，满足一定条件就迁移到另一个状态这些条件被标记到迁移的边上这个系统称为标记迁移系统(Labelled Transitive System，LTS)。(2)在每个状态上，有某些性质被满足，这些性质被描述为一个(古典逻辑或者时态等逻辑)公式。(3)与定理证明一样，系统要满足的性质也被刻画为逻辑公式(4)用自动的手段检测上述的性质是否在系统的每个轨迹(trace)上都被满足这里的轨迹是指系统的一个可能迁移路径。形式上说，假如一个系统为S，期望的系统性质表达为逻辑

4、公式 ，那么模型检测就是验证是否S满足 。通常把S满足 表示为S|= 。模型检测的方法完全是自动化的，这是该方法的优点但是，因为协议的行为是潜在无限的，而模型检测的方法只能够处理有限状态的系统，故而决定了这个方法的不完善性，即在实际应用过程中，一定要对检测的范围加以限制。2模型检测工具AVISPA模型检测工具的代表工具就是AVISPA，它的前身是欧洲AVISS 项目中由ETH Zurich 的信息安全组开发的HLPSL/ OFMC，后来得到了不断地完善，现在的AVISPA集成了OFMC，CL,SATMC和TA4SP等后台工具。AVISPA以高级协议规范语言（High Level Protoco

5、l Specification Language，HLPSL）作为输入，通过翻译器HLPS2IF 将HLPSL 转换为中间格式（Intermediate Format，IF），然后使用模型检测器（On-the-Fly Model-Checker，OFMC）来验证。2.1功能架构 AVISPAN工具提供了一套建立和分析协议安全的应用软件。协议用高级协议说明语言HLPSL来建模，以描述协议和协议的的安全性质。其结构图如下所示：图1.1 AVISPA的基本结构示意图HLPSL是一种丰富的、模块化的、基于角色的形式语言，提供了一套包括控制流模式、数据结构、可选择入侵者模式、复杂的安全目标以及不同的密码

6、初始值和代数性质的说明。这些特性能够使HLPSL 很好的描述现代的、工业化规模的协议。而且，HLPSL 不仅支持基于时间片段的逻辑行为的公开语义，还支持基于重写的中间形式化语言IF。IF是一个比HLPSL低级的语言，可以被AVISPAN工具的后台直接使用。HLPSL2IF 自动将HLPSL 语言翻译成IF 语言，并将它们依次反馈给测试后端。AVISPA 使用了4 种后端分析工具来解决安全协议的确认问题：（1）OFMC(On-the-fly Model-Checker)：基于IF 语言需求驱使的描述，通过探测系统的变迁，OFMC 能够完成协议的篡改和有限制的确认。OFMC 支持密码操作的代数性质

7、的规范，以及各种协议模型。（2）CL-AtSe（Constraint-Logic-based Attack Searcher）：CL-AtSe 通过强大的简化探测法和冗余排除技术来执行协议。它建立在模型化的方式上，并且是对密码操作的代数性质的延伸。CL-AtSe 支持输入缺陷探测和处理消息串联。（3）SATMC（SAT-based Model-Checker）：SATMC 建立在通过IF 语言描述的，有限域上变迁关系的编码的公式，初始状态和状态集合的说明代表了整个协议的安全特性。此公式将反馈给SAT 状态推导机，并且建立的任何一个模型都将转化为一个攻击事件。（4）TA4SP(Tree Auto

8、mata based on AutomaticApproximations for the Analysis of Security Protocols)：TA4SP通过树形语言和重写机制估计入侵者的知识。根据不同的保密特性，TA4SP 能够判断一个协议是否有缺陷，或者是几个会合的对话后是否安全。2.2使用方法使用AVISPA 协议分析工具对安全协议进行分析的一般性过程如下：首先，将安全协议编码为某种形式化描述语言；然后，根据协议目标和安全属性，给出不同的消息成分的类型；最后，根据分析工作的结果判断协议是否安全，是否达到了预期目标。（1）分析安全协议，并根据HLPSL 语法，将协议进行建模，编

9、辑成后缀名为“.hlpsl”的文件，（2）将HLPSL 文件导入，利用HLPSL编辑器将HLPSL 文件转换为后缀名为“.if”的中间文件；（3）将IF 文件导入，利用选定的后端分析工具将IF 文件分析得到后缀名“.atk”的结果文件，通过结果文件可以分析得出该协议的安全性、目标、攻击轨迹等各种细节。3 MS-CHAPv2协议形式化分析3.1 MS-CHAPv2协议简介CHAP( Challenge-Handshake Authentication Protocol),即质询- 握手鉴别协议, 通常被嵌入到其它协议中, 在无线网络通信、PSTN 或ISDN 的电路交换连接、拨入连接或专有连接完

10、成身份鉴别功能。作为一种被广泛应用的身份鉴别协议, MSCHAP协议在RFC19941 中有详细描述。MS-CHAP协议采用加密验证机制, 其主要的工作过程如下:1) 客户端向服务器发出一个质询请求;2) 服务器返回一个随机质询数;3) 客户端根据口令HASH 值生成对应密钥, 对随机质询数加密, 发送到服务器作为响应;4) 服务器在数据库中查询HASH 值生成对应密钥并对响应解密, 将所得与原来发送的质询数作比较。若匹配, 则鉴别通过。MS-CHAP4 对PAP 进行了改进, 不再直接通过链路发送明文口令, 而是发送被口令HASH 值加密质询数。采用这种方式服务器端将只存储经过HASH 算法

11、加密的用户口令而不是明文口令, 这样就能够提供进一步的安全保障。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失败包的主动攻击

12、。MPPE在每个方向上使用一个唯一的密钥。这样可以防止对每一方向的流量进行XOR，从而去掉密码的影响而实施的攻击。这些改变确实纠正原来协议中的主要安全弱点：对LAN Manager hash函数的使用及使用同一输出反馈加密密钥多次。但是，许多安全问题依然存在，例如客户如何保护自己，加密密钥与用户口令熵相同，给攻击者进行加密比较攻击留有太多的信息。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

13、: 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

14、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)

15、哈希函数定义： 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 compositionsession

16、(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结果分

17、析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 Tunnelin

18、g Protocol% suite (PPTP).% REFERENCE:% citeRFC2759% MODELER:%beginitemize%item Haykal Tej, Siemens CT IC 3, 2003%item Paul Hankes Drielsma, ETH Zurich%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

19、% 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 me

20、ssage 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:

21、 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 Adef= local State : nat, Na, Nb : text const sec_kab1 : pr

22、otocol_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,

23、A : agent, Kab : symmetric_key,H: hash_func, Snd, Rcv: channel(dy)played_by Bdef= 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 :=

24、 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

25、, kab, kai, kbi : symmetric_key, h : hash_func, na, nb : protocol_id intruder_knowledge = a, b, h, kai, kbi compositionsession(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 o

26、n 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/workfileYicrwdsection signature:state_chap_Resp: agent * agent * symmetric_key * has

27、h_func * nat * text * text * set(agent) * nat - factstate_chap_Init: agent * agent * symmetric_key * hash_func * nat * text * text * set(agent) * nat - factsection types:sec_kab2, nb, na, sec_kab1: protocol_idNa, Nb, Dummy_Nb, Dummy_Na, dummy_nonce: textset_79, set_77, set_76, set_74, set_69, set_61

28、: setState, 9, 6, 3, 4, SID, 2, 1, 0, Dummy_State, SID2, SID1: natSet_37, Dummy_Set_37, Set_21, Dummy_Set_21, ASGoal: set(agent)start, MGoal: messageH, h: hash_funca, b, B, A, Dummy_A, A2Goal, A1Goal, i: agentKab, kab, kai, kbi: symmetric_keysection inits:initial_state init1 := iknows(start). iknows

29、(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_n

30、once,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,Dumm

31、y_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) :=

32、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_Re

33、sp(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

34、(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

35、,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) = equal(SID1,SID2)property authent