Supremum of agent number needed in analyzing security protocols based on Horn logic

To study the supremum of the number of agents needed in analyzing security protocols for properties such as secrecy and authentication, an extended trace model for security protocols and properties based on Horn logic program is introduced. Strategy vectors are added to Horn logic programs for protocols, which ensure that the intruder can have nondeterministic choices, and help to correctly and completely describe the reception of messages and consequently cover more attacks. The supremum of the number of honest agents needed to express an attack on a protocol ρ for secrecy property and authentication property is given as N_ρ(the number of roles except servers in ρ), which is fixed for each protocol. The supremum of the number of dishonest agents needed to express an attack on a protocol ρ is proved to be dependent on whether the security property being analyzed is considered as strong or weak.