(海南大学信息科学技术学院信息安全系，海南省海口市，570228)
摘要：安全协议形式化方法大都在一个很高的抽象层次建立协议模型。但是协议的许多安全问题是在很低的抽象层次产生。本文分析了ECB工作模式下的NSL协议的安全问题，并通过破坏同态性的方法给出一种改进方案。通过扩展规则的BAN逻辑对NSL协议建模和分析，验证结果表明协议中存在着安全漏洞，新的改进方案可以避免这种攻击。
关键词：安全协议; ECB; NSL
An improved scheme for NSL protocol based on ECB mode
Wu Han Wei , Li Hong Lei, YAO Xiao Ming,Wang Ze Qun
(Department of Information Science & Technology, Hainan University,Hai-kou,570228)
Abstract: Formal Methods for Security Protocols establish protocol model in a high level of abstraction. Many of the security problems are generated at a low level of abstraction however. This paper analyzes security issues of NSL protocol which works on ECB mode, and gives an improved scheme by destroying the homomorphism. Using the extended rules of the BAN logic modeling and analysis of the NSL protocol, the result of formal analysis indicates that there exists some attacks of this protocol, the new improved scheme can avoid such attacks.
Key Words: Security Protocol; ECB;NSL
0 引言
基金项目：海南省自然科学基金(808135)、海南省教育厅高校科研基金(Hjkj2009-06)资助。作者简介：吴汉炜，男，讲师，研究方向安全协议；李红蕾，女，讲师，研究方向信息安全；姚孝明，男，副教授，研究方向信息安全；王泽群，男，讲师，研究方向信息安全。
安全协议分析是安全协议验证的一种有效实现方式，其基础是构建适用于安全协议分析方法的形式化模型。近年来，涌现出了多种安全协议分析的形式化分析方法。主要攻击者理论基础包括Dolev-Yao模型[1]和互模拟等价模型。以Dolev-Yao模型为基础的分析方法有基于定理证明的BAN类逻辑[2]、递归方法[3]和串空间[4]方法，基于模型检测的CSP[5]方法、混合系统NRL[6]分析器。Dolev-Yao模型是一个被广泛应用的安全协议攻击者模型，目前大部分有关安全
协议的研究工作都遵循Dolev和Yao的基本思想。
Dolev-Yao模型有效地界定了安全协议攻击者的行为能力，攻击者可以控制协议通信网络. 攻击者具有如下能力:(1)可以窃听所有经过网络的消息;(2)可以阻止和截获所有经过网络的消息;(3)可以存储所获得或自身创造的消息;(4)可以根据存储的消息伪造消息，并发送该消息;(5)可以作为合法的主体参与协议的运行。此外，Dolev-Yao模型另一个重要特点是将安全协议本身与安全协议所采用的密码系统分开，即在假定密码系统是“完善”的基础上讨论安全协议本身的安全属性。把问题划分为两个不同的层次：先研究安全协议本身的安全性质，然后讨论实现层次的具体细节，包括所采用的具体密码算法等。
基于Dolev-Yao模型的安全协议形式化方法大都在一个很高的抽象层次建立协议模型，在带来方便性的同时也带来安全问题。比如Dolev-Yao模型的协议验证方法无法发现基于密码原语适应性的攻击[7] [8]，包括加解密的同态、可交换性、无界性等。同态特性在密码算法中普遍存在，另外同态特性还可与其他特性结合作用。这些特性都使协议的安全性验证更加复杂。
1.基于ECB的NSL协议
1.1 ECB工作模式
电子密码本ECB(Electronic Code Book)模式是一种常见的加密工作模式。在ECB模式下，直接用分组密码算法来进行消息的加密和解密。把明文分成多个分组后，每一个明文分组被加密成一个密文分组。
假设密钥为k，明文为M=m1m2m3…mn ，密文为C=c1c2c3…cn 。ECB模式的加解密算法可以表示为：
加密：Ci=Ek(mi), i=1 , 2 ,…, n
解密：mi=Dk(ci), i=1 , 2 ,…, n
任一明文分组的加密是单独的，所以加密可以并行处理。由于加密不能隐蔽数据模式，所以系统的明文对应相同的密文，不能抵抗分组重放、插入、删除等攻击。如图1，第一和第三明文块相同时产生相同密文块。
图1.相同明文块的ECB加密结果
(责任编辑：)
