## IACR News

Updates on the COVID-19 situation are on the Announcement channel.

Here you can see all recent updates to the IACR webpage. These updates are also available:

#### 10 September 2021

###### José Carlos Bacelar Almeida, Manuel Barbosa, Karim Eldefrawy, Stéphane Graham-Lengrand, Hugo Pacheco, Vitor Pereira
ePrint Report
MPC-in-the-Head (MitH) is a general framework that enables constructing efficient zero- knowledge (ZK) protocols for NP relations from secure multiparty computation (MPC) proto- cols. In this paper we present the first machine-checked implementations of this transformation. We begin with an EasyCrypt formalization that preserves modular structure of the original MitH construction and can be instantiated with arbitrary MPC protocols, secret sharing and commitment schemes satisfying standard notions of security. We then formalize various suitable components, which we use to obtain full-fledged ZK protocols for general relations. We compare two approaches for obtaining verified exectuable implementations. The first approach realizes a fully automated extraction from EasyCrypt to OCaml. The second one reduces the trusted computing base (TCB) and provides better performance for the extracted executable by com- bining code extraction with manual formal verification of low-level components implemented in the Jasmin language. We conclude the paper with a discussion of the trade-off between formal verification effort and performance, and also discuss how our approach opens the way for fully verified implementations of state-of the-art optimized protocols based on MitH.
###### Linsheng Liu, Daniel S. Roche, Austin Theriault, Arkady Yerukhimovich
ePrint Report
Recent years have seen a strong uptick in both the prevalence and real-world consequences of false information spread through online platforms. At the same time, encrypted messaging systems such as WhatsApp, Signal, and Telegram, are rapidly gaining popularity as users seek increased privacy in their digital lives. The challenge we address is how to combat the viral spread of misinformation without compromising privacy. Our FACTS system tracks user complaints on messages obliviously, only revealing the message's contents and originator once sufficiently many complaints have been lodged. Our system is private, meaning it does not reveal anything about the senders or contents of messages which have received few or no complaints; secure, meaning there is no way for a malicious user to evade the system or gain an outsized impact over the complaint system; and scalable, as we demonstrate excellent practical efficiency for up to millions of complaints per day. Our main technical contribution is a new collaborative counting Bloom filter, a simple construction with difficult probabilistic analysis, which may have independent interest as a privacy-preserving randomized count sketch data structure. Compared to prior work on message flagging and tracing in end-to-end encrypted messaging, our novel contribution is the addition of a high threshold of multiple complaints that are needed before a message is audited or flagged. We present and carefully analyze the probabilistic performance of our data structure, provide a precise security definition and proof, and then measure the accuracy and scalability of our scheme via experimentation.
###### Kushal Babel, Philip Daian, Mahimna Kelkar, Ari Juels
ePrint Report
We introduce the Clockwork Finance Framework (CFF), a general purpose, formal verification framework for mechanized reasoning about the economic security properties of composed decentralized-finance (DeFi) smart contracts.

CFF features three key properties. It is contract complete, meaning that it can model any smart contract platform and all its contracts---Turing complete or otherwise. It does so with asymptotically optimal model size. It is also attack-exhaustive by construction, meaning that it can automatically and mechanically extract all possible economic attacks on users' cryptocurrency across modeled contracts. Thanks to these properties, CFF can support multiple goals: economic security analysis of contracts by developers, analysis of DeFi trading risks by users, and optimization of arbitrage opportunities by bots or miners. Because CFF offers composability, it can support these goals with reasoning over any desired set of potentially interacting smart contract models.

We instantiate CFF as an executable model for Ethereum contracts that incorporates a state-of-the-art deductive verifier. Building on previous work, we introduce extractable value (EV), a new formal notion of economic security in composed DeFi contracts that is both a basis for CFF analyses and of general interest.