基于串空间认证测试的DTLS协议认证性分析

泰彬彬 王俊芳

（中国电子科技集团公司第五十四研究所河北石家庄 050081）

基于串空间认证测试的DTLS协议认证性分析

泰彬彬 王俊芳

（中国电子科技集团公司第五十四研究所河北石家庄 050081）

网络通信的普及和发展使得对网络协议尤其是安全协议的需求日益增长，同时安全要求及攻击方式的多样化对网络安全协议的效率和准确性提出了更高的要求。通过对各种协议安全性分析方法进行研究，采用串空间方法对DTLS协议进行形式化建模，进而采用认证测试方法进行协议认证性证明，用简明清晰的方式验证DTLS协议的认证性，保障了数据传输的安全。

协议安全性分析 串空间 认证测试 DTLS；

1 引言

安全协议使用密码技术,实现网络环境下的身份认证和信息保密,它看似简单,但若确保正确是极其困难的。因此,对安全协议进行分析就显得十分重要，当前形式化的分析方法被公认为分析认证协议的最有效手段。

近些年来，基于UDP的应用程序不断增加，为了保障数据传输的安全性，DTLS协议应运而生，然而对DTLS协议的安全性分析十分缺乏，且大多为主观分析或模拟仿真等非形式化分析的方法，或是分析过程不够精确和严格，针对这种情况采用形式化分析方式对DTLS协议进行认证性分析。

2 形式化分析方法及比较

现状主流的安全协议分析方法有3种：基于模态逻辑技术的分析方法、基于模型检测技术的分析方法、基于定理证明的分析方法。

①基于模态逻辑技术的分析方法是一个演绎推理的过程，先定义逻辑推理规则和公理，其后对安全协议的形式化分析[1]。目前应用最为广泛，但该方法不能对保密性安全属性进行分析，并且存在规则不完善和语义不精确等问题；

②基于模型检测技术的分析方法也称为基于状态检测的方法，其优点是自动化程度高，可以借助自动分析工具来完成分析过程[2]。但其原理是对协议状态空间进行搜索，然而随着协议的增大其状态空间呈指数增长，因此总是面临着状态空间爆炸问题的困扰；

③基于定理证明的分析方法，其中最具代表性的是Paulson归纳证明法和串空间模型[2]。Paulson归纳法将协议形式化为所有可能的“迹”的集合，而“迹”是协议的通信事件序列，最终在“迹”上通过归纳的方法来证明协议的安全；串空间模型将协议运行的各个状态和整体过程转化为集合和有向图的形式进行描述，利用协议运行的特性订阅集合中各个状态间的偏序关系，通过对集合中最小元的定义和证明，确定是否存在攻击节点。

采用串空间模型法，即可以避免了模型检测方法普遍存在的状态空间爆炸问题，又把协议的执行过程用图示法表示，不仅简单直观，也有利于通过图论和算法对协议进行分析。认证测试方法是应用串空间模型的一种协议安全分析的技术，认证测试与其他协议安全分析方法相比更为简洁、直观和清晰，更易于使用。因此选择采用串空间方法建模，采用认证测试方法进行认证性分析。

3 认证测试方法及规则

认证测试方法是基于串空间模型的一种安全协议形式化分析与设计方法。在认证测试中仍然使用串空间模型中关于串、丛的定义和性质，但是将保密数据作为构造测试的标准，构造测试分量，并根据测试分量的格式分别构造入测试、出测试和主动测试，从而证明协议能够满足的认证和保密属性。其基本思想为：假设安全协议中的一个主体生成并发送了一条包含新数据的消息，而后在一个不同的加密形式中接收到，则可以断定某个拥有相关密钥的主体接收并转换了包含的消息[3]。认证测试带有一些本身所具有的规则，应用这些规则能够简化协议分析的过程。

定义1：令C为一个丛，S为一个串，n1，n2S，对于aM，aterm(n1)，并且n2产生一个新的分量t2，使得at2，若n1为负节点，n2为正节点，则n1n2为变换边，若n1为正节点，n2为负节点，则n1n2为被变换边[4]。

定义2：如果a唯一产生于节点n0，并且n0n1是a的被变换边，则n0n1是a的测试[4]。

定义4：若n0n1是对a的测试，并且KP，a在节点n0处唯一生成，同时满足t0={|h|}K是a在n0的测试分量，则称n0n1是a在t0的出测试，而t0={|h|}K是a在n0的出测试分量[5]。

若n0n1是对a的测试，并且KP，a在节点n0处唯一生成，同时满足t0={|h|}K是a在n1的测试分量，则称n0n1是a在t0的入测试，而t0={|h|}K是a在n1的入测试分量[5]。

若t={|h|}K是任何a在n中的测试分量，且KP，则负节点n是t的一个主动测试[6]。

4 DTLS协议介绍

DTLS协议由5部分组成，其中记录层为基础，握手层、密钥规格变更层、警告层和应用层为记录层所承载的数据。记录层会将承载的数据进行分段、压缩和加密（协议好密码后才进行），最后添加DTLS协议头部。DTLS协议通过明文进行握手和密钥交换，协商好密钥后应用层数据传输是加密进行的，其握手及密钥交换流程如图1所示。

图1 DTLS握手及密钥交换过程

在握手过程中，由于DTLS协议是基于UDP之上的，消息在传输过程中可能会丢失，是不可靠的。为此，DTLS协议采用接收确认这种传统的处理消息丢失的方法进行处理，保证了消息传输的可靠性。

5 DTLS协议认证性证明

DTLS握手协议的形式化描述如下：

结合DTLS协议交互过程，及形式化分析中对明文消息可忽略[9]，由此可将DTLS协议的串空间模型描述如下：

⑴客户端串模型

所用符号说明：

VerC和VerS为客户端和服务器端支持的协议版本号；SecC和SecS为支持的加密方法；NC和NS为协议中产生的随机数；pre-K表示客户端发送完证书后生成的主密钥；Session ID表示客户端发起会话的会话标识号；Cookie表示服务器为本次会话生成的标识号；message表示握手协议运行至发送消息为止所有消息的内容的hash；CS-K表示客户端与服务器协商的会话密钥。；CID表示客户端标识，SID表示服务器端标识；K-change为会话密钥生成的标识；MC和MS为协议中交换的消息历史；C-K和S-K为双方公钥；Certificate{signCA{S，S-K}}、Certificate{signCA{C，C-K}}为经可信中心签名的证书；signC{}为客户端用私钥签名的消息；C-height(S)表示串S在丛C中的丛高度；term(结点)为结点事件函数，sign()为结点符号函数，匚表示子项关系。

由认证测试的理论可知发起者发起通信后必定有响应者响应通信，且在交互的过程中必定存在某个带有新鲜性的变量（随机数）的不同加密形式，以确保该交互过程的唯一性及保密性[10]；每个响应者的响应必定存在发起者发起通信，且交互过程存在某个带有新鲜性的变量的不同加密形式，以确保该交互过程的唯一性及保密性[11]。

条目（1）证明

设C为丛，N为包含随机数NC的一个集合，由DTLS协议的认证过程可知，C-height(Si)=4，结点＜Si，1＞为串中NC出现的第一个结点，且NC匚term(＜Si，1＞)且NCN，所以其是集合N的入口点，所以NC起源于结点＜Si，1＞，且由假设知，每个NC均为唯一独立的，所以NC唯一起源于结点＜Si，1＞。

令结点n1=＜Si，1＞，n2=＜Si，4＞，sign(n1)=+，sign(n2)=-，NC起源于n1，且存在n2的新分量t2={NC}CS-K使得NC匚t2，所以边是NC的被变换边。

并且NC唯一起源于n1，所以边是NC的测试。

令t={NS，NC，MS}CS-K，NC匚t，且t是n2的分量，t不是其他任意结点的真子项，所以t是NC的测试分量。令P为攻击者的密钥集合，边是NC的测试，其中P，除t外，NC不在n2的任何分量中出现(唯一起源)，t是结点n2中a的测试分量。且边是NC的被变换边，称边n1n2为t中数据NC的入测试。

条目（2）证明

由上面条目（1）和（2）的证明可以看出客户端与服务器相互认证成功，从而证明了DTLS协议的认证性，从而通过形式化语言对其认证性进行了分析。

6 结束语

详细讨论了DTLS协议原理，运用形式化分析的方法对DTLS进行形式化建模，并考虑到形式化分析中存在过于复杂的证明步骤及状态空间的无限膨胀，采用认证测试的方法对DTLS协议的形式化模型进行安全性分析，降低了证明的复杂性，从而通过较为简洁的方式证明了该协议的理论安全性。

[1]冀云刚.传输层安全协议研究及应用[D].陕西:西安电子科技大学,2011.

[2]余磊.基于串空间模型的安全协议分析方法研究[D].安徽:淮北师范大学,2010.

[3]王聪，刘军，王孝国,等.安全协议原理与验证[M].北京:北京邮电大学出版社,2011.

[4]李建华.网络安全协议的形式化分析与验证[M].北京:机械工业出版社,2010.

[5]邢媛，蒋睿.基于串空间模型的UMTS AKA协议安全分析与改进[J].东南大学学报,2010(6):1163-1168.

[6]孔娟，曹利培.TLS协议认证测试模型与形式化分析[J].计算机工程与应用,2009(23):100-103.

[7]刘家芬.安全协议形式化分析中认证测试方法的研究[D].成都:电子科技大学,2009.

[8]邓荭.基于DTLS协议VPN的研究与实现[D].成都:电子科技大学,2011.

[9]周清雷，毋晓英.认证测试方法的扩展及其应用[J].郑州大学学报,2010(3):50-53.

[10]杨明，罗军舟.基于认证测试的安全协议分析[J].软件学报,2006(1):148-156.

[11]方燕萍.串空间模型及其认证测试方法的扩展与应用[D].江苏:苏州大学,2009.

[12]李谢华，李建华,杨树堂等.认证测试方法在安全协议分析中的应用[J].计算机工程,2006(2):19-22.

Analysis on DTLS Protocol Authentication Based on Strand Space Authentication Test

TAI Bin-bin WANG Jun-fang
(The 54th Research Institute of CETC,Shijiazhuang Hebei 050081,China)

The popularization and development of network communication make the demands of network protocol,especially security protocol,increase significantly.At the same time,the diversification of security requirements and attack modes require higher efficiency and accuracy of network security protocol.This paper studies various protocol security analysis methods,implements the formal modeling for DTLS protocol by strand space method,certifies the protocol authentication by authentication test method,and verifies the authentication of DTLS protocol through concise and clear way to ensure the security of data transmission.

interruption;timer;performance test;thread;event

TP39

A

1008-1739（2014）24-51-3

定稿日期：2014-11-26