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

摘要：

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

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

所属期刊栏目：47

分类号：TP301(计算技术、计算机技术)

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

在线出版日期：2021-01-20（万方平台首次上网日期，不代表论文的发表时间）

页数：共8页

页码：146-153