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

摘要：

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

关键词： 安全协议 逻辑程序 映射 参与者个数 上确界 踪迹模型 策略向量

作者: 刘锋 李舟军 周倜

作者单位: 国防科技大学计算机学院,湖南,长沙,410073 国防科技大学计算机学院,湖南,长沙,410073;北京航空航天大学计算机科学与工程学院,北京100083

会议类型: 国内会议

会议名称: 第三届可信计算与信息安全学术会议

会议地点: 郑州

会议语种:中文

页码: 79-84

在线出版日期: 2008-10-25（万方平台首次上网日期，不代表论文的发表时间）