Proof of Supremum of Agent Number in Security Protocol Analysis
Ti Zhou · Journal of Wuhan University · 2009
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.