ABSTRACT. The design of security protocols is extremely subtle and vulnerable to potentially devastating flaws. As result, many tools and techniques for the automated verification of protocol designs have been developed. Unfortunately, these tools don't have the ability to model and reason about protocols with randomization, which are becoming increasingly prevalent in systems providing privacy and anonymity guarantees. The security metrics of these systems is often formulated through a notion of indistinguishability. In this paper, we give the first algorithms for model checking indistinguishability properties of randomized security protocols against the powerful threat model of a Dolev-Yao attacker. Our techniques are implemented in the Stochastic Protocol ANalayzer (SPAN) and evaluated on several examples. As part of our evaluation, we conduct the first automated analysis of an electronic voting protocol based on the 3-ballot design.