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

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

传统对称密钥加密协议的加密和解密速度较快,但用户无法进行身份认证,容易造成通信代理持有密钥过多导致管理困难的问题,而非对称密钥加密协议可实现用户的合法身份认证,但密钥复杂度高,使其在处理大容量消息时运行速度较慢。为解决上述问题,结合对称和非对称密钥加密方式,构建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.