Hmm, the algorithm used was formal proven secure: https://people.eng.unimelb.edu.au/vjteague/UniversalVerifiabilitySwissPost.pdf https://people.eng.unimelb.edu

Hmm, the algorithm used was formal proven secure: https://people.eng.unimelb.edu.au/vjteague/UniversalVerifiabilitySwissPost.pdf https://people.eng.unimelb.edu.au/vjteague/UniversalVerifiab... > How can there be a trapdoor when the system has been formally proven secure? Any formal proof of correctness for any system makes some assumptions that become axioms in the formal proof. Scytl’s formal proof of security [Scy18] simply models the mixnet as sound, based on an informal interpretation of Bayer and Groth’s security proof. It does not model the proper generation of commitment parameters. We do not see any reason to believe there is an error in Scytl’s proof, but when the axioms are mistaken the conclusions are not valid. This does not mean that formal proofs are not valuable—at an absolute minimum, they clarify assumptions and explain the reasons for trust—but it does mean that they are not a substitute for broad and open public scrutiny. It is quite possible that there are errors in the implementations of other cryptographic primitives, that their details may not be modelled in the formal proofs, and that they may affect either privacy or verifiability. There wasn't a better path to translate the proof into an implementation? How was the algorithm translated into code (Java I think)?