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

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

作　　者：夏锐 钱振江 刘苇[3] XIA Rui;QIAN Zhenjiang;LIU Wei(School of Computer Science and Technology,Soochow University,Suzhou,Jiangsu 215000,China;School of Computer Science and Engineering,Changshu Institute of Technology,Changshu,Jiangsu 215500,China;State Grid Electric Power Research Institute,Nanjing 211000,China)

机构地区：[1]苏州大学计算机科学与技术学院,江苏苏州215000 [2]常熟理工学院计算机科学与工程学院,江苏常熟215500 [3]国网电力科学研究院,南京211000

出　　处：《计算机工程》2021年第1期146-153,共8页Computer Engineering

基　　金：江苏省自然科学基金面上项目(BK20191475);2020年度江苏省第五期“333工程”科研资助项目(BRA2020306);江苏省高校“青蓝工程”中青年学术带头人培养对象资助项目(2019);国家电网公司科技项目。

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

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

分 类 号：TP301[自动化与计算机技术—计算机系统结构]