使用构造类别代数描述和验证密码协议

• 作者: 刘政 屈玉贵 赵保华
• 来源期刊: 通信学报
• 学科: 工学
• 关键词: 密码协议 构造类别代数 形式化描述 协议验证
• 年，卷（期）: 2004,（3）
• 所属期刊栏目: 技术报告
• 页码范围: 91-96
• 页数: 6页
• 分类号: TN915.04
• 字数: 4461字
• 语种: 中文
• DOI: 10.3321/j.issn:1000-436X.2004.03.012

摘要

密码协议必须满足安全属性的需求,对密码协议进行形式化规范需要证明其满足该属性.传统的方法或者不利于验证,或者不利于描述.本文在构造类别代数中引入时序算子,对密码协议以及协议的入侵者进行建模,在此基础上利用时序逻辑推导协议应该满足的安全属性.通过在Equicrpt协议上的应用,说明了这是一种解决密码协议描述和验证的行之有效的方法.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	屈玉贵	中国科技大学计算机科学与技术系	16	198	8.0	14.0
2	赵保华	中国科技大学计算机科学与技术系	22	234	10.0	15.0
3	刘政	中国科技大学计算机科学与技术系	2	3	1.0	1.0