期刊文献+
共找到1篇文章
< 1 >
每页显示 20 50 100
一种基于Isabelle/HOL的安全通信协议验证方法 被引量:5
1
作者 夏锐 钱振江 刘苇 《计算机工程》 CAS CSCD 北大核心 2021年第1期146-153,共8页
传统对称密钥加密协议的加密和解密速度较快,但用户无法进行身份认证,容易造成通信代理持有密钥过多导致管理困难的问题,而非对称密钥加密协议可实现用户的合法身份认证,但密钥复杂度高,使其在处理大容量消息时运行速度较慢。为解决上... 传统对称密钥加密协议的加密和解密速度较快,但用户无法进行身份认证,容易造成通信代理持有密钥过多导致管理困难的问题,而非对称密钥加密协议可实现用户的合法身份认证,但密钥复杂度高,使其在处理大容量消息时运行速度较慢。为解决上述问题,结合对称和非对称密钥加密方式,构建D_protocol混合密钥加密协议。使用Isabelle/HOL定理证明辅助工具对D_protocol协议建立通信代理和消息序列的形式化模型,采用形式化操作语义描述用户行为,通过归纳分析方式对通信协议消息交互过程涉及的相关定理展开验证,结果表明D_protocol协议在提高通信效率的同时具有较高的安全性,并且可在一定程度上抵抗外部攻击和中间人攻击。 展开更多
关键词 通信协议 混合密钥 形式化建模 形式化验证 isabelle/hol定理证明辅助工具
下载PDF
上一页 1 下一页 到第
使用帮助 返回顶部