In this paper we address security protocol correctness with respect to secrecy and present a formal reasoning for evaluating such correctness. The proposed framework includes a comprehensive analysis and a bounding model for multi-session attacks that is sufficient for our correctness proofs. We examine the possible behavior of the intruder and draw conclusions about how his knowledge evolves and what actions he can take to gain as much information as possible for building winning strategies for an attack.