CCITT X.509协议的形式化分析及其改进  

Formal Analysis and Improvement of CCITT X.509 Protocol

作　　者：解颜铭[1,2] 石曙东[2] 翁艳琴[1,2] 

机构地区：[1]湖北师范学院数学与统计学院,湖北黄石435000 [2]湖北师范学院计算机科学与技术学院,湖北黄石435000

出　　处：《计算机安全》2012年第6期50-53,共4页Network & Computer Security

基　　金：湖北省自然科学基金NO.2006ABA056;湖北省教育厅重点项目NO.D20092203;湖北省教育厅青年项目NO.Q20102503~~

摘　　要：串空间模型是一种新兴的密码协议形式化分析工具,基于串空间模型的协议认证分析方法是比较常用的验证方法。概述了串空间模型理论和基于串空间模型的认证测试理论,并利用此理论对CCITT X.509协议进行了形式化的分析。该协议存在缺陷并对此进行了改进。Strand space model is a new cryptographic protocol analysis tool,certification test method which is based on strand space model is a more commonly used method.This article provides an overview of the strand space model theory,and certification testing theory based on strand space model.And we use this theory to formally analyze the CCITT X.509 protocol.We find that this protocol has flaws,and we improve it.

关 键 词：安全协议 CCITT X.509协议 串空间模型 认证测试 

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