AtheCrypt 2026

Abstract: Garbled Circuits have been a standard technique for secure two-party computation (2PC) since ancient times (1980's AD). Simple and fast, but with costs linear in circuit size, they did not change or improve much over the years, until recently. In this talk, based on joint works with David Heath (UIUC) and Lucien Ng (GT), I will discuss unexpected Garbled Circuit advances such as free branching (Stacked Garbling) and, time permitting, efficient LUTs (Look-up tables).

Abstract: Ring Signatures allow a user to sign on behalf of an ad-hoc set of public keys, while hiding their identity inside that set. Linkable Ring Signatures (LRS) add the functionality of detecting signatures originating from the same signer. They have found many applications in anonymous transactions and e-voting.
The LLRing family of linkable ring signature schemes by Hui and Chau (ESORICS 2024) is one of the more efficient LRS schemes. However, we show that it has an unlinkability vulnerability, meaning an adversary can create more unlinkable signatures than the number of secret keys they own. The vulnerability is caused by the introduction of unwanted structure to base elements used in proofs. We also find a similar attack against the Threshold Ring Referral (TRR) scheme of Ta, Hui, and Chau (Security and Privacy 2025), rendering it unsound.
We show how to achieve strong linkability with logarithmic verification complexity in the pairing based setting by first reverting the unsafe construction of base elements, and by also adjusting the arguments of knowledge used in order to maintain efficiency. Concretely, by modifying the Dory argument to fit our scheme we are able to match the performance of LLRing-P. We separate the design and analysis of the scheme from the instantiation of the knowledge arguments, which helps prevent unwanted interactions between the two, and can provide easier upgrades to more efficient proof systems. link: https://eprint.iacr.org/2025/1375

Abstract: We define and instantiate a signature-like primitive, which we term sharp anonymous multisignatures (in short, ♯AMS) that meets the needs of blockchain governance. In a nutshell, ♯AMSs allow any set of parties to generate a signature, e.g., on a proposal to be voted upon, which, if posted on the blockchain, hides the identities of the signers/voters but reveals their number. This can be seen as a generalization of threshold ring signatures (TRS).

Abstract: Payments, unlike general state-machine replication, do not require total ordering across the transactions of different accounts. This observation alone was enough to build faster, consensusless payment systems such as FastPay. These systems, however, share a critical limitation: a client can lose liveness on their own account. While the model guarantees this never happens to an honest client, in a real deployment it can still arise from benign faults such as buggy software, temporary network asynchrony, or leak of the secret key. In this talk we present an extension of FastPay that restores liveness through a recovery mechanism in the 5f+1 model. We give the construction, prove it secure, and show that the 5f+1 resilience is in fact necessary.

Abstract: When you think of a decompiler or binary lifter, do you think of it as a static analyzer? In this talk I'll explain why you should, at least in highly-challenging setups. Specifically, context-sensitive static analysis has been the basis for the most advanced decompiler of Ethereum VM smart contracts. We will see why decompilation can really be a "what will the program do for all inputs?" question and what bizarre forms of static analysis can help us with the problem.

Abstract: The field of program verification is undergoing an abrupt transformation. For decades, verifying that software does what it claims was understood to be valuable in principle and prohibitive in practice, kept out of reach by the heavy labor required to construct proofs by hand. LLMs are rapidly changing the picture: they can now generate proofs in proof assistants with minimal human guidance, in a fraction of the time a human would need. The question is no longer whether machines can help us prove programs correct, but how we should rebuild our tools to make the most of them.
This talk surveys that shift in the setting of Ethereum smart contracts. I begin with the state of the art in verifying EVM contracts: what the established techniques achieve, and the limits they keep running into. I then argue that the present moment calls for genuinely new infrastructure and tools. We need verification frameworks deliberately designed so that the mechanical bulk of proofs can be carried out by machines, while human effort is reserved for the ideas a machine cannot supply, such as high-level properties and invariants.
I conclude by presenting ongoing work in this direction: foundational translation validation for EVM bytecode. We have built a framework for expressing that bytecode is equivalent to a compact, readable specification, together with a library of theorems and tactics for mechanically proving that deployed contracts meet their specifications. Preliminary results show that LLMs can carry out such proofs unsupervised, in reasonable time, producing readable proof scripts. I discuss what an advance like this may mean for the future of verification, and how it may enable a new era of trust in smart contracts, where deployed code is accompanied by a machine-checked proof that it refines its specification.

Abstract: The security of many Proof-of-Stake (PoS) payment systems relies on quorum-based State Machine Replication (SMR) protocols. While classical analyses assume purely Byzantine faults, real-world systems must tolerate both arbitrary failures and strategic, profit-driven validators. We therefore study quorum-based SMR under a hybrid model with honest, Byzantine, and rational participants.
We first establish the fundamental limitations of traditional consensus mechanisms, proving two impossibility results: (1) in partially synchronous networks, no quorum-based protocol can achieve SMR when rational and Byzantine validators collectively exceed 1/3 of the participants; and (2) even under synchronous network assumptions, SMR remains unattainable if this coalition comprises more than 2/3 of the validator set.
Assuming a synchrony bound Δ, we show how to extend any quorum-based SMR protocol to tolerate up to 1/3 Byzantine and 1/3 rational validators by modifying only its finalization rule. Our approach enforces a necessary bound on the total transaction volume finalized within any time window Δ and introduces the strongest chain rule, which enables efficient finalization of transactions when a supermajority of honest participants provably supports execution. Empirical analysis of Ethereum and Cosmos demonstrates validator participation exceeding the required 5/6 threshold in over 99 of blocks, supporting the practicality of our design.
Finally, we present a recovery mechanism that restores safety and liveness after consistency violations, even with up to 5/9 Byzantine stake and 1/9 rational stake, guaranteeing full reimbursement of provable client losses.