安全协议分析中参与者个数上确界的论证

摘要：

为了明确安全协议分析和验证中所必需的参与者个数的上确界,改进了基于Horn逻辑的踪迹模型,在该模型中增加了策略向量,描述了攻击者对消息的截留能力以及消息接收的不确定性;提出了在Herbrand域和Herbrand基上的映射,该映射将潜在无穷的参与者限制在有穷的个体内;使用该映射给出了分析安全协议的保密性所必需的参与者个数的上确界n(ψ),定义了语义保持.结果显示,对于安全协议的任意安全性质,若其Horn子句与协议程序在影射后保持原来的语义关系,则町以得出分析该性质所必需的参与者个数的上确界.

关键词：安全协议、安伞性质、逻辑程序、映射

所属期刊栏目：55

分类号：TP393(计算技术、计算机技术)

资助基金：国家自然科学基金60473057;90604007

在线出版日期：2009-04-15（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：79-84