摘要： 在传统的串空间基础上引入带变量的串空间模型，对于未确定的消息项或其子项用变量表示，允许变量出现在消息项及其演算中，协议由参与协议运行的不同主体的带变量的串组成。以协议运行的迹语义为模型，提出了一个用于推理协议主体的各种行为的模态逻辑系统，给出了该逻辑的语法、公理及推理规则。基本的模态公式 表示主体A完成动作P， 是相应的结果，通过主体行为的各种组合并绑定相应逻辑公式，最终推断安全协议的秘密性和可鉴别性。用该方法分析Helsinki协议，能发现其中的安全漏洞Horng-Hsu攻击。

关键词: 安全协议, 变量, 串空间, 逻辑

Abstract: A strand space model with variables is provided based on traditional strand space, the undermined terms and subterms are expressed with variables, and the variable occurs in the message term and its calculus. The protocol consists of strands with variables belonging to different participants in the protocol running. Based on the concrete traces, the logic designed for reasoning about the principal action, consists of syntax, atoms and inference rules. The basic modal formula means that the action P is finished with the result of . By associating sequence of actions and attaching the formulas, it can prove the security properties of protocols such as secrecy and authentication. It analyzes Helsinki protocol through the method, and the logic leads directly to rediscovery of Horng-Hsu’s attack.

Key words: security protocol, variable, strand space, logic

中图分类号: 

• TP391