基于SMV的安全协议模型检验

作者：刘锋; 李舟军; 李梦君; 宋震; 张艳

来源：计算机工程与科学, 2004, (02): 28-31+62.

• 模型检验
• 安全协议
• 认证
• SMV

SMV是一个基于线性时态逻辑的符号化模型检验工具。本文利用SMV对Needham-Schmeder公钥协议的简化版本进行了验证,发现了利用消息重放进行的攻击。

• 单位
  武汉大学; 国防科技大学; 数学学院; 软件工程国家重点实验室; 四川大学