Contingent payments from two-party signing and verification for abelian groups

in Conference Proceedings 2022 IEEE 35th Computer Security Foundations Symposium (CSF) (2022)

The fair exchange problem has faced for a long time the bottleneck of a required trusted third party. The recent development of blockchains introduces a new type of party to this problem, whose ... [more ▼]

The fair exchange problem has faced for a long time the bottleneck of a required trusted third party. The recent development of blockchains introduces a new type of party to this problem, whose trustworthiness relies on a public ledger and distributed computation. The challenge in this setting is to reconcile the minimalistic and public nature of blockchains with elaborate fair exchange requirements, from functionality to privacy. Zero-knowledge contingent payments (ZKCP) are a class of protocols that are promising in this direction, allowing the fair exchange of data for payment. We propose a new ZKCP protocol that, when compared to others, requires less computation from the blockchain and less interaction between parties. The protocol is based on two-party (weak) adaptor signatures, which we show how to instantiate from state of the art multiparty sign- ing protocols. We improve the symbolic definition of ZKCP security and, for automated verification with Tamarin, we propose a general security reduction from the theory of abelian groups to the theory of exclusive or. [less ▲]

Election Verifiability Revisited: Automated Security Proofs and Attacks on Helios and Belenios

in IEEE 34th Computer Security Foundations Symposium, Dubrovnik 21-25 June 2021 (2021, June)

Election verifiability aims to ensure that the outcome produced by electronic voting systems correctly reflects the intentions of eligible voters, even in the presence of an adversary that may corrupt ... [more ▼]

Election verifiability aims to ensure that the outcome produced by electronic voting systems correctly reflects the intentions of eligible voters, even in the presence of an adversary that may corrupt various parts of the voting infrastructure. Protecting such systems from manipulation is challenging because of their distributed nature involving voters, election authorities, voting servers and voting platforms. An adversary corrupting any of these can make changes that, individually, would go unnoticed, yet in the end will affect the outcome of the election. It is, therefore, important to rigorously evaluate whether the measures prescribed by election verifiability achieve their goals. We propose a formal framework that allows such an evaluation in a systematic and automated way. We demonstrate its application to the verification of various scenarios in Helios and Belenios, two prominent internet voting systems, for which we capture features and corruption models previously outside the scope of formal verification. Relying on the Tamarin protocol prover for automation, we derive new security proofs and attacks on deployed versions of these protocols, illustrating trade-offs between usability and security. [less ▲]

Private Votes on Untrusted Platforms: Models, Attacks and Provable Scheme

in Bursuc, Sergiu; Dragan, Constantin-Catalin; Kremer, Steve (Eds.) Private Votes on Untrusted Platforms: Models, Attacks and Provable Scheme (2019)