| 安全协议分析中参与者个数上确界的论证 |
| |
| 引用本文： | 刘锋,李舟军,周倜. 安全协议分析中参与者个数上确界的论证[J]. 武汉大学学报(理学版), 2009, 55(1) |
| |
| 作者姓名： | 刘锋 李舟军 周倜 |
| |
| 作者单位： | 1. 国防科技大学计算机学院,湖南,长沙,410073
2. 国防科技大学计算机学院,湖南,长沙,410073;北京航空航天大学计算机科学与工程学院,北京100083 |
| |
| 摘 要： | 为了明确安全协议分析和验证中所必需的参与者个数的上确界,改进了基于Horn逻辑的踪迹模型,在该模型中增加了策略向量,描述了攻击者对消息的截留能力以及消息接收的不确定性;提出了在Herbrand域和Herbrand基上的映射,该映射将潜在无穷的参与者限制在有穷的个体内;使用该映射给出了分析安全协议的保密性所必需的参与者个数的上确界n(ψ),定义了语义保持.结果显示,对于安全协议的任意安全性质,若其Horn子句与协议程序在影射后保持原来的语义关系,则町以得出分析该性质所必需的参与者个数的上确界.
|
| 关 键 词： | 安全协议 安伞性质 逻辑程序 映射 |
Proof of Supremum of Agent Number in Security Protocol Analysis |
| |
| LIU Feng,LI Zhoujun,ZHOU Ti. Proof of Supremum of Agent Number in Security Protocol Analysis[J]. JOurnal of Wuhan University:Natural Science Edition, 2009, 55(1) |
| |
| Authors: | LIU Feng LI Zhoujun ZHOU Ti |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 万方数据 等数据库收录！ |
|
