一种描述安全协议的形式化规范语言  

Formal Specification Language for Description of Security Protocol

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

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

出　　处：《小型微型计算机系统》2004年第7期1246-1249,共4页Journal of Chinese Computer Systems

基　　金：国家自然科学基金重大研究计划项目 (90 10 40 10 )资助;国家自然科学基金科学部主任基金项目(60 2 410 0 4)资助;教育部博士点基金项目 (2 0 0 0 0 3 5 80 2 )资助;国家 863计划项目 (2 0 0 1AA112 0 62和 2 0 0 1AA12 10 16)资助;中国科学院院长基金特别支持项

摘　　要：安全协议的设计和分析是复杂而且容易出错的 .使用形式化的语言有利于安全协议的正确性和完整性 .现有的安全协议的描述方法大多很复杂而且容易导致二义 ,从而导致协议隐含着种种的安全隐患 .引入了基于构造类别代数的形式化规范语言来规范安全协议 ,通过规则集合和公理集合对安全协议进行精确地描述 ,有利于协议设计地规范化和协议漏洞地发现 ,同时对 Needham-The analysis and design of Security Protocol is always complex and error prone. The utilization of formal methods is useful for the rightness and completeness of the protocol. Most current methods of description are too complex and ambiguous, and so as to cause some flaws of security inside the protocol intuitively. In this paper, we introduce a formal language based on Construct Categorical Algebra for specification of security protocol, we normalize the design of the protocol by introducing the rule set and axiom set, which surely improve the detection of the security holes. We also give an example of using this language on the Needham Schroedler authentication protocol.

关 键 词：安全协议 构造类别代数 形式化描述语言 

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