Zero-knowledge proofs (ZKPs) allow a prover to convince a verifier that they possess a secret without revealing any information about that secret. This paper formalizes a widely-used ZKP protocol, specifically the Schnorr protocol, using Probabilistic Hoare Logic (PHL) and Product Probabilistic Relational Hoare Logic ( \(\times \) PRHL). The deterministic states are defined based on the set-extension style, which captures the information change of the participants in the protocol. In particular, PHL demonstrates that the probability of a prover consistently passing the challenges posed by the verifier asymptotically approaches 1 if the prover actually holds the secret. Furthermore, we explore the Schnorr protocol within a generalized framework where the initial probabilistic state assigns a probability p for holding the secret (instead of strictly 1 or 0) and a probability \(1-p\) for not holding it (instead of strictly 0 or 1). This characterization shows that the ZKP protocol can be considered a method to “expose” the probability p of a prover holding a secret, even when p is initially unknown to anyone. \(\times \) PRHL constructs a coupled product program to prove computational indistinguishability between the real protocol and a simulator, thereby proving the zero-knowledge property. Our work provides a novel formal framework for analyzing and understanding ZKPs and highlights the advantages of probabilistic reasoning in cryptographic verification.