计算机工程 ›› 2021, Vol. 47 ›› Issue (1): 146-153.doi: 10.19678/j.issn.1000-3428.0058022

• 网络空间安全 • 上一篇    下一篇

一种基于Isabelle/HOL的安全通信协议验证方法

夏锐1, 钱振江1,2, 刘苇3   

  1. 1. 苏州大学 计算机科学与技术学院, 江苏 苏州 215000;
    2. 常熟理工学院 计算机科学与工程学院, 江苏 常熟 215500;
    3. 国网电力科学研究院, 南京 211000
  • 收稿日期:2020-04-10 修回日期:2020-07-08 发布日期:2020-07-17
  • 作者简介:夏锐(1996-),男,硕士研究生,主研方向为信息安全;钱振江(通信作者),副教授、博士;刘苇,高级工程师、硕士。
  • 基金项目:
    江苏省自然科学基金面上项目(BK20191475);2020年度江苏省第五期“333工程”科研资助项目(BRA2020306);江苏省高校“青蓝工程”中青年学术带头人培养对象资助项目(2019);国家电网公司科技项目。

A Verification Method of Security Communication Protocol Based on Isabelle/HOL

XIA Rui1, QIAN Zhenjiang1,2, LIU Wei3   

  1. 1. School of Computer Science and Technology, Soochow University, Suzhou, Jiangsu 215000, China;
    2. School of Computer Science and Engineering, Changshu Institute of Technology, Changshu, Jiangsu 215500, China;
    3. State Grid Electric Power Research Institute, Nanjing 211000, China
  • Received:2020-04-10 Revised:2020-07-08 Published:2020-07-17

摘要: 传统对称密钥加密协议的加密和解密速度较快,但用户无法进行身份认证,容易造成通信代理持有密钥过多导致管理困难的问题,而非对称密钥加密协议可实现用户的合法身份认证,但密钥复杂度高,使其在处理大容量消息时运行速度较慢。为解决上述问题,结合对称和非对称密钥加密方式,构建D_protocol混合密钥加密协议。使用Isabelle/HOL定理证明辅助工具对D_protocol协议建立通信代理和消息序列的形式化模型,采用形式化操作语义描述用户行为,通过归纳分析方式对通信协议消息交互过程涉及的相关定理展开验证,结果表明D_protocol协议在提高通信效率的同时具有较高的安全性,并且可在一定程度上抵抗外部攻击和中间人攻击。

关键词: 通信协议, 混合密钥, 形式化建模, 形式化验证, Isabelle/HOL定理证明辅助工具

Abstract: Traditional symmetric key encryption protocols have a high speed in encryption and decryption,but fail to authenticate users,so they often causes the communication agent to hold too many keys to manage.The asymmetric key encryption protocols can realize the legal identity authentication of users,but the high complexity of the encryption slows the processing of large-volume messages.To solve the above problems,this paper combines the above two encryption methods to propose a hybrid key encryption protocol,D_protocol.The formal model of the communication agent and message sequence is established by using Isabelle/HOL theorem proving auxiliary tool.The user behavior is described by using formal operational semantics,and the theorems involved in the interactions between protocol messages are verified based on inductive analysis.The verification results show that D_protocol has high security while improving communication efficiency,and can resist external attacks and man in the middle attacks to a certain extent.

Key words: communication protocol, hybrid key, formal modeling, formal verification, Isabelle/HOL theorem proving auxiliary tool

中图分类号: