中文摘要：

借助形式化的方法或工具分析安全协议是非常必要而且行之有效的．进程演算具有强大的描述能力和严格的语义．能够精确刻画安全协议中各个参与者之间的交互行为．作者以进程演算为基础，嵌入消息推理系统以弥补进程演算固有的缺乏数据结构支持的特点，尝试地提出了一个基于可达关系的安全协议保密性分析模型．基于此模型，形式化地描述了安全协议的保密性，证明了一定限制条件下的可判定性．并且以TMN协议为例，给出了该模型的实例研究．

英文摘要：

The analysis and verification of security protocols are very important techniques to guarantee the security properties and the application requirements. Formal methods and automated tools are both necessary and efficient for these purposes. Security protocols are typical dis tributed concurrent systems, while process calculus is a powerful tool to model distributed concurrent systems. With strong ability of description and formal semantics, process calculus can precisely characterize the interaction between different participants of a security protocol. However, it inherently lack support of data structure. So the authors add a message inference system into process calculus. In this paper, a formal model is proposed for the secrecy analysis of security protocols based on process calculus with message inference. Using this model, the authors define two concepts, one-step reachability and multi-step reachability. Secrecy property can be formally defined and analyzed based on these teachability relations. By a case of study, the authors analyze the TMN protocol in the model. At last, the future direction to perfect the model is pointed.