基于形式化方法的安全协议安全性分析*
2015-03-25张宝峰毛军捷毕海英
邓 辉，张宝峰，刘 晖，毛军捷，毕海英
(中国信息安全测评中心,北京，100085)
基于形式化方法的安全协议安全性分析*
邓 辉，张宝峰，刘 晖，毛军捷，毕海英
(中国信息安全测评中心,北京，100085)
协议安全是确保网络数据安全的基础。传统的基于观察的人工分析协议安全性分析已不能满足安全需求。如何研究安全协议及安全属性的性质，使两者在统一框架下实现可分析和验证是亟待解决的问题，形式化分析为解决这一问题提供了精确的数学手段和强大的分析工具。对已有的安全协议形式化分析方法进行了归纳和总结，并从等价验证、协议优化和增强分析准确度三方面提出了未来的研究设想。
安全协议;安全性分析;形式化方法;网络安全
0 引 言
互联网自诞生以来，就以惊人的速度在全世界迅速发展。互联网在人类社会及生活中的广泛引入，加快了社会信息的交互，使得现实世界中的各种系统均对应出现在互联网这个虚拟系统中。遗憾的是，互联网自身的开放性、共享性以及不稳定性引发了众多网络安全问题。近年来攻击者利用安全协议漏洞，伪装成合法的通信者窃听、更改或者重放信息，引发网络安全事件的现象层出不穷。
为确保数据通信安全，在众多安全协议中，有一类特殊的协议旨在实现不安全信道上的数据传输安全，称为安全协议。安全协议是一种运用密码技术解决网络安全问题的有效方式，在不可靠通信环境下，基于加密算法，通过加密信息交换实现保密性、完整性、认证性以及不可抵赖性。
自1976年Hellman等人提出第一个安全协议Needham-Schroeder后[1]，各种类型的安全协议例如SSL[2]、IPSec[3]、S/MIME[4]和SHITP[5]等陆续推出，并被广泛应用于身份认证和密钥分配等多个领域。目前，安全协议已成为构建高安全性网络的基础。根据实现目标的不同，安全协议可分为密码交换协议、认证协议、认证密钥交换协议、电子商务协议和安全多方计算协议。
安全协议旨在实现通信安全。但是，事实上一部分安全协议在出现之初被认为是安全的，却在很短时间内被证明是非安全的。如著名的Needham-Schroeder协议在推出三年后被证明存在安全缺陷。据统计，已公开的安全协议中有超过一半的协议不能实现所声称的安全性。大部分安全协议非安全的原因不在于所采用的加密机制，而在于在设计过程中存在漏洞，即设计过程中忽略了协议被攻击的可能性。
目前针对安全协议安全性的分析方法主要有两类：攻击检验和形式化分析。但是仅能穷举已知攻击方法对协议进行攻击测试的攻击检验法不能全面评估安全协议安全性。形式化作为全面分析目标对象行为及结构分析的有利方法，可形式化建模安全协议及安全属性，将安全性分析转化为安全协议的形式化模型是否满足安全属性对应的形式化模型的过程，此过程避免了攻击检验方法的局限性，有利于发现安全协议的未知攻击。自九十年代以来，此方法已成为安全协议分析领域的热点。
形式化方法在安全协议的安全性分析中的共同技术思想是通过建立形式化建模规则，将安全协议的某个或者某些特征进行形式化规范，最终利用数学方法实现其正确性或者非正确性推导。实践证明形式化方法在安全协议的安全性分析中发挥了很好作用。
1 已有的协议安全性形式化分析方法
安全协议形式化分析研究起源于1983年Dolev和Yao提出的完美密码假设以及Dolev-Yao模型[6]，在假设密码算法不存在任何安全问题的前提下，给出安全协议的攻击者模型，并依此讨论安全协议安全属性是否得到满足，此理论成为安全协议形式化分析方法的基本框架。目前，已有的安全协议安全性形式化分析主要从认知逻辑、模型检查、定理证明三个角度出发得以实现。
1.1 基于模态逻辑的推理方法
基于模态逻辑的推理方法是安全协议形式化分析中使用最广泛的方法，突出代表是基于知识和信仰的逻辑——BAN逻辑。此逻辑在1989年提出[7]，被应用于Needham-Schroeder、Kerberos等部分著名协议的安全性分析，并且发现部分已知和未知漏洞。
BAN逻辑是最早用于验证认证协议和密钥交换协议的形式化方法，其处理流程如图1所示，包括安全协议理想化，即将协议形式化描述为一组BAN逻辑公式；协议初始假设确定，确定安全协议正确运行的初始假设条件；协议逻辑推理，将BAN逻辑公式与初始假设条件合并进行逻辑推演，得到安全协议运行的最终结果；协议安全性分析，判断最终结果是否达到安全协议的设计目标。如果结果与目标相符，则安全协议安全性得到满足，否则即安全协议存在漏洞。
图1 基于模态逻辑的安全协议安全性分析框架
但是，BAN逻辑实现安全协议安全性分析过程中，安全协议理想化与初始假设确定均存在模糊处理，导致最终的安全分析结果在精确度上无法完全保证。为此，研究学者对BAN逻辑进行了不同程度的改造，推出了类BAN逻辑系统[8-10]，其中包括：GNY逻辑、AT逻辑、CS逻辑和KG逻辑等。类BAN逻辑在一定程度上缓解了BAN逻辑的局限性，但是并未完全解决问题。
目前仍没有一种BAN类逻辑能够完全解决BAN逻辑的所有缺陷。
1.2 基于模型的状态检验方法
模型检查由Clarke、Emerson等人在1981年提出。基于此研究，用于安全协议分析的模型检测工具陆续得到开发，如Brutus模型检测器、SMV系统、Interrogator工具、NRL协议分析器等。基于模型的状态检验方法基于自动化工具实现自动执行，并能在系统不满足性质时提供反例路径，因此在工业界备受推崇[11-16]。
模型检查在安全协议安全性分析过程中的引入，目的在于扩展自动验证技术的应用领域，同时基于其自身具有形式化方法的优势最终精确化安全协议分析的结果。
利用模型检查进行安全协议安全性分析的技术思路描述如图2所示。此图表示将安全协议形式化为一个四元组，包括状态集合、状态转移集合、状态转移规则、状态转移过程。通过前向搜索或者后向搜索判断协议是否安全。其中：
(1)前向搜索：从某个初始状态出发，看协议运行过程中是否会到达不安全状态；
(2)后向搜索：确定一个不安全状态，看是否存在一个达到合法状态的通路；
图2 基于模型检查的安全协议安全性分析框架
模型检查在协议安全分析中体现出一定的技术优势，主要包括：自动化程度高，以批处理的方式可一次性检验安全协议的多条路径；TOE安全性质采用逻辑公式书写，精确度高；当规约不被满足时，会生成一条反例路径，作为诊断信息，帮助设计者及时修正TOE错误。
但是模型检查在检测安全性的过程中需要穷举安全协议对应模型中所有可能的可达状态，可能会产生状态空间爆炸，由此，模型检查对于无穷状态空间问题不可判定。同时，模型检查处理的对象同样是TOE模型而非TOE本身，形式化过程存在模糊处理。因此，分析过程可能存在偏差，导致分析结果存在误报。
1.3 基于定理证明的安全目标验证方法
定理证明源自人工智能发展时期A.Newell等人编制出的称为逻辑理论机的数学定理证明程序。基于此，Abadi和Gordon利用 Spi演算刻画协议并运行，并利用Dolev-Yao完美加密假设和观测等价实现安全协议分析[17]。之后，Fabrega等人提出利用串空间模型描述协议合法主体的行为及攻击者的动作序列，通过分析串连接情况判断协议安全属性是否得到满足[18]。为实现基于串空间模型分析方法的自动化，工具Athena已经得到实现。但是Athena无法保证搜索过程一定终止，且需限制协议运行主体的数量[19]。
除此以外，归纳法[20]、秩函数[21]等陆续被用于实现安全协议特定安全属性的证明。但是，这些方法均难以完全自动化。
定理证明技术在协议安全性分析中的基本原理可描述如图3所示，即将安全协议描述为代数或逻辑公式，联合假定必要的公理集，证明安全性质对应的待证定理集。
从分析的角度看，与模型检查不同的是，定理证明是判断安全协议是否满足安全需求，此过程实施的是安全协议的正面分析；而模型检查是寻找安全协议可能面临的威胁有哪些，此过程实施的是安全协议的反面分析。
图3 基于定理证明的安全协议安全性分析框架
相比于其他安全分析技术，定理证明误报率很低，是众多静态分析方法中最准确的方法。此方法可以处理无限状态空间问题。
但是定理证明需要形式化描述安全协议的前置条件、后置条件以及循环不变量，此过程效率较低，较难用于复杂安全协议的验证。同时，把安全协议及其安全属性形式化转换为代数或者逻辑公式时相关特征信息存在遗漏的可能，一旦缺乏则可能导致证明结果的不精确性。
2 已有分析方法的比较
在安全协议安全性分析过程中，形式化方法相比攻击检验而言，其优点比较突出，即可以避免攻击检验中需要进行状态穷举而造成测试子集选取的不完备性。
不同的方法在安全协议安全性分析过程中的相同点和不同点，可从分析方法的目的、原理、是否可处理无限状态、以及分析角度来进行说明，具体描述如表1所示。
表1 已有的安全协议安全性形式化分析方法
3 已有分析方法面临的问题
3.1 无法有效刻画网络协议
已有的分析方法无论是从设计、实现，还是其他阶段，对网络协议利用如BAN 逻辑、串空间、Spi演算，还是更一般化的形式化方法进行刻划，都会或多或少地损失一些有用的属性信息，从而导致分析方法的有效性和可靠性被打了折扣。
3.2 优化理论未引入
已有的安全协议形式化分析方法均直接对安全协议本身或协议对应的形式化模型进行处理，并未进行任何优化处理，分析过程中容易出现“状态爆炸”现象。安全协议自身的优化实现对于优化安全协议安全性分析，提高分析效率具有实际的意义。
3.3 其他问题
基于模态逻辑的推理方法、基于模型的状态检验方法及基于定理证明的安全目标验证方法可用于判断网络协议是否满足不同的安全需求。但是，它们无法实现无限状态空间网络协议形式化分析、不安全状态定位、最大化分析不安全状态等中的部分问题是目前网络协议形式化分析需要解决的重点问题。
4 安全协议安全性形式化分析的未来
面对已有安全协议安全性形式化分析存在的不足，未来应重点关注以下三个方面的研究。
4.1 实现分级等价验证
等价验证的产生源于对门级电路设计过程中功能的一致性检测。目前，通过调研发现等价验证已经在并发系统的行为功能性验证、行为及结构一致性检测、行为及结构优化工作中得到了初步的研究并取得了一定的处理效果。
基于等价验证的一致性思想，可以被用于实现安全协议与安全性质的匹配验证，基本思路可设计为从攻击者的角度，如果不能区分安全协议与安全性质所对应的形式化模型观测等价，则表明安全性质得到满足。
整体的技术思路如图4所示。
图4 基于等价验证的安全协议安全性分析框架
提取基于等价验证的安全协议安全性分析特征后，表1可更新如表2所示。
表2 安全协议安全性形式化分析方法
通过分析表2，可以了解到等价验证在已有方法中优势较为明显，因此未来应加大这方面的研究。但是如何选择合适的等价关系是需要思考的问题。如果将协议看作为所有可能事件路径的集合，则不同协议对应的事件路径集合不同。因此，协议等价关系应该从协议运行规则的角度出发分别构建低级别的外部等价及高级别的内部等价关系。
4.2 实现协议优化
在安全协议以及安全性质的形式化建模过程中，涉及诸多规则的说明、约束和生成，导致最终获得的形式化模型通常比较复杂，因此在自动化处理中往往耗时较多，效率低下导致形式化方法在大规模工程应用中无法推广。未来需要研究形式化模型的优化方法，提高形式化方法的整体处理效率。同时，由于形式化模型的优化，对于减缓“状态爆炸”也会起到促进的作用。
4.3 提高分析准确度
形式化的过程是一个高度提炼和抽象目标特征的过程，会使安全协议以及安全性质分别与它们的形式化模型之间存在一定的误差，造成某些信息的丢失，对最终安全性分析结果的准确性造成或多或少的损失。未来需要优化形式化方法应用于安全协议安全性分析时涉及的模型转换规则，最终提高分析结果的准确性。
5 结 语
已有的安全协议形式化分析方法为网络协议的通用分析提供了一种新的途径。但是，通过本文的分析，发现已有分析方法在不同方面存在不同程度的问题，且尚未形成完整的理论体系，难以解决网络协议设计和验证领域中的许多关键问题。未来需进一步开展协议的通用形式化分析方法研究，对于促进网络通信安全具有重要的理论意义。
[1] Blanchet B. Security Protocol Verification: Symbolic and Computational Models [C]. Proceedings of the First International Conference on Principles of Security and Trust. 2012:3-29.
[2] Krawczyk H, Paterson K G, Wee H. On the Security of the TLS Protocol: A Systematic Analysis [J]. Advances in Cryptology-Crypto 2013. 2013:429-448.
[3] Singh G, Dhanda S K. Performance Analysis of Security Schemes in Wireless Sensor Network[J]. International Journal of Advanced Research in Computer and Communication Engineering. 2013, 2(8): 3217-3223.
[4] Lauter K. The Advantages of Elliptic Curve Cryptography for Wireless Security [J]. IEEE Wireless Communications. 2004, 11(1): 62-67.
[5] Martin F J, Plaza E, Rodríguez-Aguilar J A. An Infrastructure for Agent-based Systems: An Interagent Approach [J]. International Journal of Intelligent Systems. 2000, 15(3): 217-240.
[6] Dolev D, YAO A. On the Security for Public key Protocols [J]. IEEE Transaction on Information Theory. 1983, 29(2): 198-208.
[7] Meadows C A. Formal Verification of Cryptographic Protocols: A Survey [J], Springer Berlin Heidelberg. 1995.
[8] Gritzalis S, Spinellis D,Georgiadis P. Security Protocols Over Open Networks and Distributed Systems: Formal Methods for Their Analysis, Design, and Verification[J]. Computer Communications. 1999,22(8):697-709.
[9] Agray N, Van Der Hoek W, De Vink E. On BAN Logics for Industrial Security Protocols [J]. Springer Berlin Heidelberg. 2002:29-36.
[10] YUAN J J. An Enhanced Two-Factor User Authentication in Wireless Sensor Networks [J]. Telecommunication Systems.2014,55(1): 105-113.
[11] Lowe G. Breaking and Fixing the Needham-Schroder Pubic-key Protocol Using FDR[J]. In Tools and Algorithms for the Construction and Analysis of Systems. 1996, 1055: 147-166.
[12] Basagiannis S, Katsaros P, Pombortsis A. An Intruder model with Message Inspection for Model Checking Security Protocols [J]. Computers & Security. 2010, 29(1): 16-34.
[13] Donini F M, Mongiello M, Ruta M, et al. A Model Checking-based Method for Verifying Web Application Design [C]. Proceeding of the International Workshops on Web Languages and Formal Methods. 2006, 151(2): 19-32.
[14] Patel R, Borisaniya B, Patel A, et al. Comparative Analysis of Formal Model Checking Tools for Security Protocol Verification [J]. Recent Trends in Network Security and Applications. Springer Berlin Heidelberg. 2010:152-163.
[15] LIU Y C. Fairness Analysis of E-Commerce Protocols based on Strand Spaces [J]. International Journal of Grid and Utility Computing. 2013, 4(2): 128-133.
[16] Matsuo S, Miyazaki K, Otsuka A, et al. How to Evaluate the Security of Real-Life Cryptographic Protocols? [J]. Financial Cryptography and Data Security. 2010:182-194.
[17] Abadi M, Gordon A D. A Calculus for Cryptographic Protocols: The Spi Calculus [C]. Proceedings of the 4th ACM Conference on Computer and Communications Security. 1997:36-47.
[18] Fabrega F J T, Herzog J C, Guttman J D. Strand Spaces: Proving Security Protocols Correct [J]. Journal of Computer Security. 1999, 7(2): 191-230.
[19] SONG D X, Berezin S, Perrig A. Athena: A Novel Approach to Efficient Automatic Security Protocol Analysis [J]. Journal of Computer Security. 2001,9(1):47-74.
[20] Paulson L. Proving Properties of Security Protocols by Induction [C]. Proceedings of the IEEE Computer Security Foundations Workshop. 1997:70-83.
[21] Delicata R, Schneider S. A Formal Model of Diffie-Hellman Using CSP and Rank Functions[J]. 2003.
Security Protocol Analysis based on Formal Method
DENG Hui, ZHANG Bao-feng, LIU Hui, MAO Jun-jie, BI Hai-ying
(China Information Technology Security Evaluation Center, Beijing 100085, China)
Protocol security is the foundation for ensuring of network data security. Traditional methods based on manual analysis could no longer meet the requirements of data security. How to research, analyze and verify the security protocol and its security properties in the same formal framework is now a problem demanding prompt solution. Formal analysis provides an exact mathematical method and automatic tool for solving this peoblem. In this paper, the existing formal analysis methods for security protocol are reviewed and summarized. In addition, the future researches in the three fields of equivalence verification, protocol optimization, and accuracy enhancement are also suggested.
security protocol; security analysis; formal method; network security
2015-03-24；
2015-07-25 Received date:2015-03-24；Revised date：2015-07-25
国家自然科学基金(No.61472448)
Foundation Item:National Natural Science Foundation of China(No.61472448)
TP309
A
1002-0802(2015)09-1068-05
邓 辉(1985—)，女，博士，助理研究员，主要研究方向为信息安全；
张宝峰(1983—)，男，硕士，副研究员，主要研究方向为信息安全；
刘 晖(1976—)，女，博士，副研究员，主要研究方向为信息安全；
毛军捷(1982—)，男，博士，副研究员，主要研究方向为信息安全；
毕海英(1981—)，女，硕士，助理研究员，主要研究方向为信息安全。
10.3969/j.issn.1002-0802.2015.09.017
