计算机应用 ›› 2005, Vol. 25 ›› Issue (01): 138-140.DOI: 10.3724/SP.J.1087.2005.0138

• 信息安全 • 上一篇    下一篇

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

龙士工,罗文俊,李祥   

  1. 贵州大学计算机软件与理论研究所
  • 出版日期:2005-01-01 发布日期:2005-01-01
  • 基金资助:

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

Symbolic model checking analysis for cryptographic protocol

LONG Shi-gong, LUO Wen-jun, LI Xiang   

  1. Institute of Computer Science, Guizhou University
  • Online:2005-01-01 Published:2005-01-01

摘要: 对密码协议模型检测的方法作了理论上的研究,并用SMV检测工具给出了一个实际分析的例子。结果表明,利用符号模型检测方法分析并发现密码协议重放攻击的漏洞是一种行之有效的方法。

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

Abstract:  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.

Key words: cryptographic protocol, symbolic model checking, SMV

中图分类号: