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

Using construct categorical algebra language for formal description of cryptographic protocol

作　　者：刘政[1] 赵保华[1] 屈玉贵[1] 

机构地区：[1]中国科技大学计算机科学与技术系,安徽合肥230027

出　　处：《通信学报》2004年第3期91-96,共6页Journal on Communications

基　　金：自然科学基金重大计划资助项目(90104010);自然科学基金科学部主任基金资助项目(60241004);教育部博士点基金项目(2000035802);国家"973"计划项目(2003-7);国家"863"基金资助项目(2001AA112062和2001AA121016);中国科学院院长基金特别支持资助项目(院基计字90

摘　　要：密码协议必须满足安全属性的需求,对密码协议进行形式化规范需要证明其满足该属性。传统的方法或者不利于验证,或者不利于描述。本文在构造类别代数中引入时序算子,对密码协议以及协议的入侵者进行建模,在此基础上利用时序逻辑推导协议应该满足的安全属性。通过在Equicrpt协议上的应用,说明了这是一种解决密码协议描述和验证的行之有效的方法。The cryptographic protocol should always satisfy security properties, so the formal specification should give the corresponding proof method. The traditional methods may not be suitable for description or not suitable for verification. In this paper, we introduce temporal logic operator into Construct Categorical Algebra for specification and verification of cryptographic protocol, we modeling both the protocol and the intruder, and deduce its security property with the use of temporal logic. With its application on Equicrypt protocol, we conclude that its an effective method on description and verification of cryptographic protocol.

关 键 词：密码协议 构造类别代数 形式化描述 协议验证 

分 类 号：TN915.04[电子电信—通信与信息系统]