This paper proposes a belief multisets formalism for analyzing cryptographic protocols, and the formalism is foundationally different from the previous: a participant’s beliefs should depend only on the sent or received fresh messages and the beliefs already possessed by this party. The presented security adequacy of unilateral authentication secure, mutual authentication secure, unilateral session key secure, or mutual session key secure is proved not only substantial but also necessary to meet 4 security definitions respectively under the computational model of matching conversation and indistinguishability. Illustrations and comparison show that the analysis results based on the belief multisets suggest the correctness of a protocol or the way to construct attacks intuitively from the absence of security properties. The formalism is independent of the concrete formalization of a protocol or attackers’ possible behaviors. The formalism can be developed not only by hand but also by automation.