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