Shaken, not Stirred - Automated Discovery of Subtle Attacks on Protocols using Mix-Nets

Mix-Nets are used to provide anonymity by passing a list of inputs through a collection of mix servers. Each server mixes the entries to create a new anonymized list, so that the correspondence between the output and the input is hidden. These Mix-Nets are used in numerous protocols in which the anonymity of participants is required, for example voting or electronic exam protocols. Some of these protocols have been proven secure using automated tools such as the cryptographic protocol verifier ProVerif, although they use the Mix-Net incorrectly. We propose a more detailed formal model of exponentiation and re-encryption Mix-Nets in the applied Π-Calculus, the language used by ProVerif, and show that using this model we can automatically discover attacks based on the incorrect use of the Mix-Net. In particular, we (re-)discover attacks on four cryptographic protocols using ProVerif: we show that an electronic exam protocol, two electronic voting protocols, and the "Crypto Santa" protocol do not satisfy the desired privacy properties. We then fix the vulnerable protocols by adding missing zero-knowledge proofs and analyze the resulting protocols using ProVerif. Again, in addition to the common abstract modeling of Zero Knowledge Proofs (ZKP), we also use a special model corresponding to weak (malleable) ZKPs. We show that in this case all attacks persist, and that we can again (re)discover these attacks automatically.