文献类型：期刊文章

作　　者：顾永跟[1] 傅育熙[2] 朱涵[2]

机构地区：[1]湖州师范学院计算机科学与技术系,湖州313000 [2]上海交通大学计算机科学与工程系,上海200030

出　　处：《计算机学报》

基　　金：国家杰出青年科学基金(60225012);;国家"九七三"重点基础研究发展规基金(2003CB317005);国家自然科学基金(60473006)资助

年　　份：2007

卷　　号：30

期　　号：2

起止页码：255-261

语　　种：中文

收录情况：BDHX、BDHX2004、CSA、CSA-PROQEUST、CSCD、CSCD2011_2012、EI(收录号：20071610557931)、IC、INSPEC、JST、MR、RCCSE、SCOPUS、ZGKJHX、核心刊

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

关 键 词：安全协议 可达关系  进程演算  消息推理  

分 类 号：TP309]