Mayank Rathee

2027

1. ShannonProver: Towards Automating Formal Cryptographic Proofs

   Yiping Ma, Yu-Lin Tsai, Mayank Rathee, Deevashwer Rathee, François Dupressoir, Pierre-Yves Strub, and Raluca Ada Popa

   In IEEE Symposium on Security and Privacy, 2027

   Abs PDF Code

   Cryptographic proofs are produced at a scale that increasingly exceeds the community’s ability to verify them manually. Machine-checked proofs offer a path toward scalable proof verification, but they shift the bottleneck to writing the proofs themselves: even when the high-level proof plan is known, turning it into a proof script requires spelling out every detail the plan leaves implicit, which is laborious even for experts. This paper presents ShannonProver, an agentic system for automating cryptographic proofs. Given a protocol and its security definitions modeled by a cryptographer, ShannonProver decomposes the main theorem into intermediate games and lemmas, and constructs EasyCrypt proof scripts for those lemmas. We evaluate ShannonProver on a new dataset of lemmas in EasyCrypt. The benchmark spans textbook primitives, deployed standardized protocols, as well as recent NIST proposals, and includes expert case studies drawn from a corpus that has not previously been available online. On case studies such as ChaChaPoly1305 and MEE-CBC, ShannonProver completes within hours proof developments that historically took experts weeks to months. More broadly, this work suggests a path toward accelerating cryptographic research: as agents automate the proof-engineering burden, cryptographers can iterate more quickly on new constructions, obtain machine-checked assurance earlier, and bring protocols from design to deployment faster.

2026

1. Verifiable PIR with Small Client Storage

   Mayank Rathee, Keewoo Lee, and Raluca Ada Popa

   In IEEE Symposium on Security and Privacy, 2026

   Abs PDF Code

   Efficient Verifiable Private Information Retrieval (vPIR) protocols, and more generally Verifiable Linearly Homomorphic Encryption (vLHE), suffer from high client storage. VeriSimplePIR (USENIX Security 2024), the state-of-the-art vPIR protocol, requires clients to persistently maintain over 1 GiB of local storage to privately access an 8 GiB remote database. We present a new vPIR protocol that reduces the client state by orders of magnitude while preserving online latency. In our protocol, clients only need to store 512 KiB for an 8 GiB database, achieving a 2000x improvement. Our vPIR protocol is built over our new vLHE scheme. Unlike VeriSimplePIR, our scheme doesn’t use random oracles and relies only on standard lattice assumptions - (R)LWE and SIS. These improvements come at a 2.5x cost in server throughput over VeriSimplePIR. Despite this throughput overhead, we achieve a comparable online latency to VeriSimplePIR by implementing several optimizations including query-level preprocessing. We also introduce the notion of covert vPIR (cvPIR), where stateful clients enjoy full vPIR security, while even stateless clients benefit from covert security against a malicious server.

2024

1. Private Analytics via Streaming, Sketching, and Silently Verifiable Proofs

   Mayank Rathee, Yuwen Zhang, Henry Corrigan-Gibbs, and Raluca Ada Popa

   In IEEE Symposium on Security and Privacy, 2024

   Abs PDF Code

   We present Whisper, a system for privacy-preserving collection of aggregate statistics. Like prior systems, a Whisper deployment consists of a small set of non-colluding servers; these servers compute aggregate statistics over data from a large number of users without learning the data of any individual user. Whisper’s main contribution is that its server- to-server communication cost and its server-side storage costs scale sublinearly with the total number of users. In particular, prior systems required the servers to exchange a few bits of information to verify the well-formedness of each client submission. In contrast, Whisper uses silently verifiable proofs, a new type of proof system on secret-shared data that allows the servers to verify an arbitrarily large batch of proofs by exchanging a single 128-bit string. This improvement comes with increased client-to-server communication, which, in cloud computing, is typically cheaper (or even free) than the cost of egress for server-to-server communication. To reduce server storage, Whisper approximates certain statistics using small-space sketching data structures. Applying randomized sketches in an environment with adversarial clients requires a careful and novel security analysis. In a deployment with two servers and 100,000 clients of which 1% are malicious, Whisper can improve server-to-server communication for vector sum by three orders of magnitude while each client’s communication increases by only 10%.

2023

1. ELSA: Secure Aggregation for Federated Learning with Malicious Actors

   Mayank Rathee, Conghao Shen, Sameer Wagh, and Raluca Ada Popa

   In IEEE Symposium on Security and Privacy, 2023

   Abs PDF Code

   Federated learning (FL) is an increasingly popular approach for machine learning (ML) in cases where the train- ing dataset is highly distributed. Clients perform local training on their datasets and the updates are then aggregated into the global model. Existing protocols for aggregation are either inefficient, or don’t consider the case of malicious actors in the system. This is a major barrier in making FL an ideal solution for privacy-sensitive ML applications. We present ELSA, a secure aggregation protocol for FL, which breaks this barrier - it is efficient and addresses the existence of malicious actors at the core of its design. Similar to prior work on Prio and Prio+, ELSA provides a novel secure aggregation protocol built out of distributed trust across two servers that keeps individual client updates private as long as one server is honest, defends against malicious clients and is efficient end-to-end. Compared to prior works, the distinguishing theme in ELSA is that instead of the servers generating cryptographic correlations interactively, the clients act as untrusted dealers of these correlations without compromising the protocol’s security. This leads to a much faster protocol while also achieving stronger security at that ef- ficiency compared to prior work. We introduce new techniques that retain privacy even when a server is malicious at a small added cost of 7-25% in runtime with negligible increase in communication over the case of semi-honest server. Our work improves end-to-end runtime over prior work with similar security guarantees by big margins - single-aggregator RoFL by up to 305x (for the models we consider), and distributed trust Prio by up to 8x.

2022

1. Waldo: A Private Time-Series Database from Function Secret Sharing

   Emma Dauterman, Mayank Rathee, Raluca Ada Popa, and Ion Stoica

   In IEEE Symposium on Security and Privacy, 2022

   PDF Code

2021

1. SIRNN: A Math Library for Secure RNN Inference

   Deevashwer Rathee^*, Mayank Rathee^*, Rahul Kranti Kiran Goli, Divya Gupta, Rahul Sharma, Nishanth Chandran, and Aseem Rastogi

   In IEEE Symposium on Security and Privacy, 2021

   Abs PDF Code

   Complex machine learning (ML) inference algorithms like recurrent neural networks (RNNs) use standard functions from math libraries like exponentiation, sigmoid, tanh, and reciprocal of square root. Although prior work on secure 2-party inference provides specialized protocols for convolutional neural networks (CNNs), existing secure implementations of these math operators rely on generic 2-party computation (2PC) protocols that suffer from high communication. We provide new specialized 2PC protocols for math functions that crucially rely on lookup-tables and mixed-bitwidths to address this performance overhead; our protocols for math functions communicate up to 423x less data than prior work. Some of the mixed bitwidth operations used by our math implementations are (zero and signed) extensions, different forms of truncations, multiplication of operands of mixed-bitwidths, and digit decomposition (a generalization of bit decomposition to larger digits). For each of these primitive operations, we construct specialized 2PC protocols that are more communication efficient than generic 2PC, and can be of independent interest. Furthermore, our math implementations are numerically precise, which ensures that the secure implementations preserve model accuracy of cleartext. We build on top of our novel protocols to build SIRNN, a library for end-to-end secure 2-party DNN inference, that provides the first secure implementations of an RNN operating on time series sensor data, an RNN operating on speech data, and a state-of-the-art ML architecture that combines CNNs and RNNs for identifying all heads present in images. Our evaluation shows that SIRNN achieves up to three orders of magnitude of performance improvement when compared to inference of these models using an existing state-of-the-art 2PC framework.

2. Function Secret Sharing for Mixed-Mode and Fixed-Point Secure Computation

   Elette Boyle, Nishanth Chandran, Niv Gilboa, Divya Gupta, Yuval Ishai, Nishant Kumar, and Mayank Rathee

   In EUROCRYPT, 2021

   PDF

2020

1. Secure Medical Image Analysis with CrypTFlow

   Javier Alvarez-Valle, Pratik Bhatu, Nishanth Chandran, Divya Gupta, Aditya Nori, Aseem Rastogi, Mayank Rathee, and 2 more authors

   In PPML@NeurIPS, 2020

   PDF
2. CrypTFlow2: Practical 2-Party Secure Inference

   Deevashwer Rathee, Mayank Rathee, Nishant Kumar, Nishanth Chandran, Divya Gupta, Aseem Rastogi, and Rahul Sharma

   In CCS, 2020

   Abs PDF Code

   We present CrypTFlow2, a cryptographic framework for secure inference over realistic Deep Neural Networks (DNNs) using secure 2-party computation. CrypTFlow2 protocols are both correct – i.e., their outputs are bitwise equivalent to the cleartext execution – and efficient – they outperform the state-of-the-art protocols in both latency and scale. At the core of CrypTFlow2, we have new 2PC protocols for secure comparison and division, designed carefully to balance round and communication complexity for secure inference tasks. Using CrypTFlow2, we present the first secure inference over ImageNet-scale DNNs like ResNet50 and DenseNet121. These DNNs are at least an order of magnitude larger than those considered in the prior work of 2-party DNN inference. Even on the benchmarks considered by prior work, CrypTFlow2 requires an order of magnitude less communication and 20x-30x less time than the state-of-the-art.

3. CrypTFlow: Secure TensorFlow Inference

   Nishant Kumar^*, Mayank Rathee^*, Nishanth Chandran, Divya Gupta, Aseem Rastogi, and Rahul Sharma

   In IEEE Symposium on Security and Privacy, 2020

   Abs PDF Video Code

   We present CrypTFlow, a first of its kind system that converts TensorFlow inference code into Secure Multi-party Computation (MPC) protocols at the push of a button. To do this, we build three components. Our first component, Athos, is an end-to-end compiler from TensorFlow to a variety of semi-honest MPC protocols. The second component, Porthos, is an improved semi-honest 3-party protocol that provides significant speedups for TensorFlow like applications. Finally, to provide malicious secure MPC protocols, our third component, Aramis, is a novel technique that uses hardware with integrity guarantees to convert any semi-honest MPC protocol into an MPC protocol that provides malicious security. The malicious security of the protocols output by Aramis relies on integrity of the hardware and semi-honest security of MPC. Moreover, our system matches the inference accuracy of plaintext TensorFlow. We experimentally demonstrate the power of our system by showing the secure inference of real-world neural networks such as ResNet50 and DenseNet121 over the ImageNet dataset with running times of about 30 seconds for semi-honest security and under two minutes for malicious security. Prior work in the area of secure inference has been limited to semi-honest security of small networks over tiny datasets such as MNIST or CIFAR. Even on MNIST/CIFAR, CrypTFlow outperforms prior work.

2019

1. Efficient private database queries using ring-LWE somewhat homomorphic encryption

   Tushar Kanti Saha, Mayank Rathee, and Takeshi Koshiba

   J. Inf. Secur. Appl., 2019

2018

1. Checking laws of the blockchain with property-based testing

   Alexander Chepurnoy and Mayank Rathee

   In IWBOSE@SANER, 2018

   Code Slides

2017

1. Efficient Protocols for Private Database Queries

   Tushar Kanti Saha, Mayank Rathee, and Takeshi Koshiba

   In DBSec, 2017
2. Private Comparison Protocol and Its Application to Range Queries

   Tushar Kanti Saha, Mayank Rathee, Deevashwer, and Takeshi Koshiba

   In IDCS, 2017

Manuscripts

2026

1. Pincer: Resource Authorization for Agents using a Digital Twin

   Mayank Rathee, Alexander Stepanov, Shalin Madabhavi, Jinhao Zhu, Raluca Ada Popa, and Ion Stoica

   Oct 2026

   arXiv preprint

   Abs arXiv PDF

   Coding agents have become increasingly long-horizon, autonomous, reliant on general-purpose shell and maintain their own persistent memory for self-improvement. While these capabilities have made the agents powerful, they have also made them harder to defend against external adversaries. Defenses that restrict this architecture — typed tools, information-flow control, or policy prediction engines — give up too much functionality to be adopted. Agents deployed today (e.g. Claude, Codex) rely on a combination of user-mediated and automode sandboxing as their primary defense. In user-mediated sandboxing, user-maintained policies decay over time and repeated permission requests cause user fatigue, while auto mode’s tool-call classifiers learn no user-specific policy and are not meant to defend against adversarial setups. Pincer is a new defense that operates at the resource layer and works alongside existing defenses at the tool-call layer like the auto mode. At the core of Pincer lies a digital twin, an isolated-context model that automatically learns and enforces dynamic user-specific least-privilege policies. The digital twin keeps continually learning the user’s preferences allowing it to act as the user’s proxy for the agent’s permission requests. To emulate the learning phase, we propose a new usercentric dataset with examples following a multi-day transcript of user-agent interaction. Our evaluation shows that Pincer performs strongly on both security and utility in comparison to several baselines which includes variants of LLM judges and adaptations of Conseca (HotOS ’25). We highlight attack types where Pincer’s design leads to a significant security improvement compared to all other baselines, while outperforming the baselines even for other types of attacks.

2. TaintTrace: Towards Deployable Multi-Hop Attribution in a Single Forward Pass

   Mayank Rathee, Piotr Mardziel, Saurabh Shintre, and Siyu Zhang

   2026

   Unpublished manuscript

Dissertation

1. Verifying Secure Execution for Systems with Untrusted Components

   Mayank Rathee

   EECS Department, University of California, Berkeley, Sep 2026

   Technical Report No. UCB/EECS-2026-288. Advisor: Raluca Ada Popa.

   Abs HTML PDF

   The question of trust lies at the center of modern systems: they rely on complex components that may be compromised by an adversary. Even when only a single component cannot be trusted, trust in the system’s behavior can fall apart. Techniques that enable verification of expected behavior address this challenge. While for many conventional systems, verification may be as straightforward as capturing the expected behavior through deterministic policies and checking them against the outputs of the components, this approach isn’t suitable for two classes of modern systems: cryptographic systems and AI systems, where the outputs are either encrypted or highly open-ended. Specialized techniques for verification exist for such systems; however, they incur significant overheads which makes them harder to adopt. To this end, we introduce new techniques for efficiently verifying secure execution across a variety of systems, from cryptographic systems for secure aggregation and private information retrieval to AI agents. First, we look at the problem of secure aggregation for federated learning and privacy-preserving telemetry. Our system, Whisper, for large-scale private telemetry in the two-server setting achieves orders of magnitude reduction in server-to-server communication when verifying that measurements are individually well-formed. After that, we look at the problem of verifiable private information retrieval (vPIR), where a client privately fetches information from a remote server while verifying that the server does not cheat. We propose a new protocol that reduces the client’s storage by orders of magnitude for standard database sizes. We introduce the notion of covert vPIR which can practically bring vPIR technology to millions of devices. Towards the end, we transition to the world of AI agents. We present Pincer, a system that augments agents with a digital twin that verifies their actions against automatically learned user preferences. This reduces the user burden dramatically while guarding the agent from going off the rails when it encounters untrusted data.

1. Private Inference in Deep Neural Network

   Nishanth Chandran, Divya Gupta, Aseem Rastogi, Rahul Sharma, Nishant Kumar, Mayank Rathee, and Deevashwer Rathee

   US 12,346,830 B2 · Microsoft Technology Licensing, LLC · Granted Jul 1, 2025

   Abs Google Patents

   A secure inference over Deep Neural Networks (DNNs) using secure two-party computation to perform privacy-preserving machine learning. The secure inference uses a particular type of comparison that can be used as a building block for various layers in the DNN including, for example, ReLU activations and divisions. The comparison securely computes a Boolean share of a bit representing whether input value x is less than input value y, where x is held by a user of the DNN, and where y is held by a provider of the DNN. Each party computing system parses their input into leaf strings of multiple bits. This is much more efficient than if the leaf strings were individual bits. Accordingly, the secure inference described herein is more readily adapted for using in complex DNNs.