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

• 作者: 刘苇 夏锐 钱振江
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: 通信协议 混合密钥 形式化建模 形式化验证 Isabelle/HOL定理证明辅助工具
• 年，卷（期）: 2021,（1）
• 所属期刊栏目: 网络空间安全
• 页码范围: 146-153
• 页数: 8页
• 分类号: TP301
• 语种: 中文
• DOI: 10.19678/j.issn.1000-3428.0058022

摘要

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