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.