| 使用构造类别代数描述和验证密码协议 |
| |
| 引用本文： | 刘政,赵保华,屈玉贵.使用构造类别代数描述和验证密码协议[J].通信学报,2004,25(3):91-96. |
| |
| 作者姓名： | 刘政 赵保华 屈玉贵 |
| |
| 作者单位： | 中国科技大学,计算机科学与技术系,安徽,合肥,230027 |
| |
| 基金项目： | 自然科学基金重大计划资助项目(90104010)，自然科学基金科学部主任基金资助项目(60241004)，教育部博士点基金项目(2000035802)，国家“973”计划项目(2003-7)，国家“863”基金资助项目(2001AA112062和2001AA121016)，中国科学院院长基金特别支持资助项目(院基计字90 |
| |
| 摘 要： | 密码协议必须满足安全属性的需求，对密码协议进行形式化规范需要证明其满足该属性。传统的方法或者不利于验证，或者不利于描述。本文在构造类别代数中引入时序算子，对密码协议以及协议的入侵者进行建模，在此基础上利用时序逻辑推导协议应该满足的安全属性。通过在Equicrpt协议上的应用，说明了这是一种解决密码协议描述和验证的行之有效的方法。
|
| 关 键 词： | 密码协议 构造类别代数 形式化描述 协议验证 |
| 文章编号： | 1000-436X(2004)03-0091-06 |
| 修稿时间： | 2002年10月24 |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
