期刊导航
期刊开放获取
cqvip
退出
期刊文献
+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
检索
高级检索
期刊导航
共找到
1
篇文章
<
1
>
每页显示
20
50
100
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
显示方式:
文摘
详细
列表
相关度排序
被引量排序
时效性排序
一种基于Isabelle/HOL的安全通信协议验证方法
被引量:
5
1
作者
夏锐
钱振江
刘苇
《计算机工程》
CAS
CSCD
北大核心
2021年第1期146-153,共8页
传统对称密钥加密协议的加密和解密速度较快,但用户无法进行身份认证,容易造成通信代理持有密钥过多导致管理困难的问题,而非对称密钥加密协议可实现用户的合法身份认证,但密钥复杂度高,使其在处理大容量消息时运行速度较慢。为解决上...
传统对称密钥加密协议的加密和解密速度较快,但用户无法进行身份认证,容易造成通信代理持有密钥过多导致管理困难的问题,而非对称密钥加密协议可实现用户的合法身份认证,但密钥复杂度高,使其在处理大容量消息时运行速度较慢。为解决上述问题,结合对称和非对称密钥加密方式,构建D_protocol混合密钥加密协议。使用Isabelle/HOL定理证明辅助工具对D_protocol协议建立通信代理和消息序列的形式化模型,采用形式化操作语义描述用户行为,通过归纳分析方式对通信协议消息交互过程涉及的相关定理展开验证,结果表明D_protocol协议在提高通信效率的同时具有较高的安全性,并且可在一定程度上抵抗外部攻击和中间人攻击。
展开更多
关键词
通信协议
混合密钥
形式化建模
形式化验证
isabelle
/
hol
定理证明辅助工具
下载PDF
职称材料
题名
一种基于Isabelle/HOL的安全通信协议验证方法
被引量:
5
1
作者
夏锐
钱振江
刘苇
机构
苏州大学计算机科学与技术学院
常熟理工学院计算机科学与工程学院
国网电力科学研究院
出处
《计算机工程》
CAS
CSCD
北大核心
2021年第1期146-153,共8页
基金
江苏省自然科学基金面上项目(BK20191475)
2020年度江苏省第五期“333工程”科研资助项目(BRA2020306)
+1 种基金
江苏省高校“青蓝工程”中青年学术带头人培养对象资助项目(2019)
国家电网公司科技项目。
文摘
传统对称密钥加密协议的加密和解密速度较快,但用户无法进行身份认证,容易造成通信代理持有密钥过多导致管理困难的问题,而非对称密钥加密协议可实现用户的合法身份认证,但密钥复杂度高,使其在处理大容量消息时运行速度较慢。为解决上述问题,结合对称和非对称密钥加密方式,构建D_protocol混合密钥加密协议。使用Isabelle/HOL定理证明辅助工具对D_protocol协议建立通信代理和消息序列的形式化模型,采用形式化操作语义描述用户行为,通过归纳分析方式对通信协议消息交互过程涉及的相关定理展开验证,结果表明D_protocol协议在提高通信效率的同时具有较高的安全性,并且可在一定程度上抵抗外部攻击和中间人攻击。
关键词
通信协议
混合密钥
形式化建模
形式化验证
isabelle
/
hol
定理证明辅助工具
Keywords
communication
protocol
hybrid
key
formal
modeling
formal
verification
isabelle
/
hol
theorem
proving
auxiliary
tool
分类号
TP301 [自动化与计算机技术—计算机系统结构]
下载PDF
职称材料
题名
作者
出处
发文年
被引量
操作
1
一种基于Isabelle/HOL的安全通信协议验证方法
夏锐
钱振江
刘苇
《计算机工程》
CAS
CSCD
北大核心
2021
5
下载PDF
职称材料
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
上一页
1
下一页
到第
页
确定
用户登录
登录
IP登录
使用帮助
返回顶部