基于Strand Space模型的CCITT X.509协议分析  

Analysis of CCITT X.509 Based on Strand Space Model

作　　者：蒋睿 李建华[1] 潘理[1] 

机构地区：[1]上海交通大学电子工程系,上海200030

出　　处：《上海交通大学学报》2004年第z1期169-173,共5页Journal of Shanghai Jiaotong University

基　　金：国家高技术研究发展计划(863)项目(2002AA145090);上海市科技发展基金资助项目(025115039).

摘　　要：运用前沿的安全协议形式化分析方法——StrandSpace模型理论,对CCITTX.509协议进行了分析,指出了该协议在保密性和认证正确性方面的缺陷,得到了BAN逻辑分析没有得到的保密性缺陷和相同的认证正确性缺陷.同时提出了改进的X.509协议,并用StrandSpace模型论证了改进协议的保密性和认证正确性.This paper introduced the Strand Space model, which is a front formal method for analysis of security protocols, to analyze the CCITT X.509 protocol.The paper indicated the drawbacks of the protocol on secrecy and authentication, and got the result on secrecy not got with the BAN logic and the same result on the authentication with the BAN logic. Meanwhile, it advanced an improved X.509 protocol, and demonstrated the secrecy and authentication correctness of the improved protocol with the Strand Space model.

关 键 词：STRAND Space模型 安全协议 形式化方法 CCITT X.509 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]