Make cryptographic proofs more formal: case of zero-knowledge proofs and rewinding
The motivation of this work is to fill a gap in the formal verification of e-voting protocols. While several proofs were achieved formalizing them through formal methods, mixnets remained an open question. Essentially, the complexity of mixnets protocols rely on zero-knowledge proofs and complex interactions between cryptographic arguments, algebraic properties satisfied by them and complex reduction techniques such as rewinding.
To help us on this path, we study mixnets through the Computationally Complete Symbolic Attacker (CCSA) model. This model offers a good trade-off between computational guarantees and being abstract enough to capture complex chains of reductions in a reasonably simple way. This work is divided in two parts. The first one is a formal proof of security properties of shuffle protocols (protocols performed by each mix-server of a mixnet). In concrete voting protocols such as Belenios or SwissPost (the protocol used for democratic votes in Switzerland), two main shuffle protocols are used. The main difficulty was formalizing the rewinding technique, used to prove the knowledge soundness property of zero-knowledge proofs within the CCSA logic. Moreover, we notice that the CCSA logic tools logic developed for proving one shuffle protocol “easily” adapt to other shuffle protocols.
Next, having proven shuffle protocols, we propose cryptographic security games for mixnets applied to e-voting protocols and prove them from the security of shuffle protocols. Finally our work hints at the fact that logical tools developed to catch the rewinding cryptographic reduction technique seems to be precise enough to formalize fine-grained probabilistic arguments such as the ones used in the Fiat-Shamir transform, paving the way for proofs of non interactive protocols.