Cryptographic security frequently relies on formal reasoning about the probability distributions of mathematical expressions. A prominent case is threshold probing security where a modeled adversary is allowed to observe a bounded number of expressions defined over secret and random variables. Many verification tools tackle the problem of automatically assessing the security of designs by verifying that such systems of expressions have a joint probability distribution independent of secrets. We share a work-in-progress approach to this verification problem based on equivalence graphs. The use of equivalence graphs allows us to solve the intricate phase ordering problem of established language-based approaches and gain a verification that is free of false negatives.