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

Proof of Supremum of Agent Number in Security Protocol Analysis

作　　者：刘锋[1] 李舟军[1,2] 周倜[1] 

机构地区：[1]国防科技大学计算机学院,湖南长沙410073 [2]北京航空航天大学计算机科学与工程学院,北京100083

出　　处：《武汉大学学报（理学版）》2009年第1期79-84,共6页Journal of Wuhan University:Natural Science Edition

基　　金：国家自然科学基金资助项目(60473057,90604007)

摘　　要：为了明确安全协议分析和验证中所必需的参与者个数的上确界,改进了基于Horn逻辑的踪迹模型,在该模型中增加了策略向量,描述了攻击者对消息的截留能力以及消息接收的不确定性;提出了在Herbrand域和Herbrand基上的映射,该映射将潜在无穷的参与者限制在有穷的个体内;使用该映射给出了分析安全协议的保密性所必需的参与者个数的上确界n(φ),定义了语义保持.结果显示,对于安全协议的任意安全性质,若其Horn子句与协议程序在影射后保持原来的语义关系,则可以得出分析该性质所必需的参与者个数的上确界.In order to determine the supremum of the number of the agents needed in analyzing and verifing security protocols,the trace model based on Horn logic is improved.Strategy vector is added into the model to describe the actions of intruders more completely,especially the ability of the intruders to detain messages and the nondeterministic reception of messages.A projection on Herbrand universe and Herbrand base is constructed,which limits the latently infinite agents to some finite ones.By this projection,the supremum of the number of agents needed in analyzing security property is proved to be n（）.For any security property,if the semantical relationship between the Horn clause for the property and the Horn logic program for the protocol is preserved under the projection,then the supremum of the agent number necessary in analyzing this property can be concluded.

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

分 类 号：TP393[自动化与计算机技术—计算机应用技术]