计算机工程

作者：夏锐, 钱振江, 刘苇

单位：1. 苏州大学 计算机科学与技术学院, 江苏 苏州 215000;2. 常熟理工学院 计算机科学与工程学院, 江苏 常熟 215500;3. 国网电力科学研究院, 南京 211000

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

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

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

来源：2021年第1期

《计算机工程》期刊编辑部

查看计算机工程杂志2021年第1期