密码协议的符号模型检测及分析  

Symbolic model checking analysis for cryptographic protocol

作　　者：龙士工[1] 罗文俊[1] 李祥[1] 

机构地区：[1]贵州大学计算机软件与理论研究所,贵州贵阳550025

出　　处：《计算机应用》2005年第1期138-140,共3页journal of Computer Applications

基　　金：贵州省自然科学基金资助项目(20043029);贵州工业大学校内基金资助项目(2004402)

摘　　要：对密码协议模型检测的方法作了理论上的研究,并用SMV检测工具给出了一个实际分析的例子。结果表明,利用符号模型检测方法分析并发现密码协议重放攻击的漏洞是一种行之有效的方法。A method was given to analyze the cryptographic protocol using a model checker in theory. A concrete example was given using SMV kits. Results show that the method using symbol model checker can discover replay attacks upon some cryptographic protocols and is effective.

关 键 词：密码协议 符号模型检测 SMV 

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