A security protocol is a distributed program that can be executed by several actors. Since several runs of the protocol within the same execution are allowed, the protocol models are often infinite and very hard to analyze. In this paper we present a formal reasoning for evaluating security protocol correctness with respect to secrecy and authentication. We build a bounding model for multi-session cryptoprotocol attacks and prove that this model is appropriate for the analysis of the intruder's possible behavior and for demonstrating protocol correctness with respect to both secrecy and authentication. The result allows us to evaluate accurately the intruder's knowledge and his potential actions for building winning strategies during an attack.