一种基于问题求解理论的密码协议形式模型  

Formal model for cryptographic protocols based on problem-solving theory

作　　者：赵宇[1] 王亚弟[1] 韩继红[1] 范钰丹[1] 赵琦[1] 

机构地区：[1]信息工程大学电子技术学院,河南郑州450004

出　　处：《计算机应用》2007年第2期303-307,共5页journal of Computer Applications

基　　金：国家973计划项目资助(TG19990358.01)

摘　　要：提出了一种基于问题求解理论的密码协议模型,给出了模型的基本语法以及基于ρ演算的形式语义,明确了模型推理过程中涉及到的一些关键性的概念和命题。该模型具有以下特点能够对密码协议进行精确的形式化描述;具有合理可靠的可证明语义;对密码协议安全性的定义精确合理;便于实现自动化推理。所有这些均确保了基于该模型的密码协议安全性分析的合理性和有效性,为正确的分析密码协议的安全性提供了可靠依据。This paper proposed a problem-solving theory based formal model, introduced the basic syntax and ρ-calculus based semantics of the model, and presented some pivotal concepts and propositions in the deduction of the model. The model has some properties as follows： can give accurate formal specifications for cryptographic protocols; has provable semantics which is reasonable and sound; can define the security properties precisely and reasonably; is easy to realize automatic deductions. All of those aforementioned make sure that the security analysis of cryptographic protocols based on this model is reasonable and efficient, and provide a dependable basis for analyzing the security of cryptographic protocols correctly.

关 键 词：密码协议 形式模型 问题求解理论 ρ演算 运算语义 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]