Time-lock puzzles are unique cryptographic primitives that use computational complexity to keep information secret for some period of time, after which security expires. This topic, while over 25 years old, is still in a state where foundations are not well understood: For example, current analysis techniques of time-lock primitives provide no sound mechanism to build composed multi-party cryptographic protocols which use expiring security as a building block. Further, there are analyses that employ idealizations and simulators of unrealistic computational power to be an acceptable sound security argument. Our goal with this short paper is to advocate for understanding what approaches may lead to sound modeling beyond idealization, and what approaches may, in fact, be hopeless at this task of sound modeling. We explain in this paper how existing attempts at this subtle problem lack either composability, a fully consistent analysis, or functionality. The subtle flaws in the existing frameworks reduce to an impossibility result by Mahmoody et al., who showed that time-lock puzzles with super-polynomial gaps (between committer and solver) cannot be constructed from random oracles alone (or any repetitive computation where the next state is completely random given the prior state); yet still the analyses of algebraic puzzles today treat the solving process as if each step is a generic or random oracle. We point out that if the generation process relies on a trapdoor function that cannot be treated as a random oracle (to allow efficient generation while avoiding this impossibility result), then, to be consistent, the analysis of the solving process should also not treat such a trapdoor function (and its intermediate states) as a random oracle. We further prove that there are no time-lock puzzles schemes with efficient generation that are based only on random oracle or generic group operations. We also delineate additional issues with the proof techniques used for time-lock puzzles. Specifically, when a time-lock puzzle must retain privacy for some amount of time, the reduction should bound the running time of the simulator. It is not a valid security argument to give the simulator more running time than the adversary would require to solve a puzzle. We survey the adherence of various attempts to this principle, as well as the properties that different attempts achieve toward composition.

Managing the timing and delays of computing events is central to distributed systems. Timed cryptography, such as time-lock puzzles (introduced almost 30 years ago) and verifiable delay functions, provides central tools for such tasks: A single party (the committer) knows a secret, commits to it publicly, and then the committed secret can be opened via a time-consuming staged computation by any observer; this process is independent of post-commitment actions by or presence of the committer. Implicit in this scenario is the requirement that the committer itself does not attack the system, and, say, prematurely selectively leak or de-commit the value, either maliciously or due to external attacks. To prevent the above attack and to expand timed-delayed cryptography to address more applications, we initiate here the study of how to distributedly hold a timed secret known neither to any individual party nor to any group smaller than a quorum. This primitive is defined in the context of multi-party computation (MPC). In fact, this implements a setting where a group of parties simultaneously learn a secret that has been kept private for a predetermined amount of time, and could have been collectively generated without a single party controlling its generation (as in distributed key generation scenarios). This new paradigm, and the ability to compose such protocols, also extends time-lock functionalities to applications where a firm commitment by a group of parties to future release is executed even without knowing the underlying secrets and even without assuming cooperation or availability of parties in the future. Sample applications requiring such delayed disclosure include accountable future scanning of software for zero-day vulnerabilities and accountable, secure sharing of clinical trial documents. We design the first secure practical protocol for Multi-party Time-lock Puzzles (MTP), a new primitive centered on the inherently needed distributed generation of a time-lock puzzle, and the inability to prematurely reconstruct the committed value unless a quorum of parties is compromised. We then leverage MTP to build Timed Multi-party Computation (TMPC), which we model as MPC with a single time-locked output.

Time-lock puzzles are unique cryptographic primitives that use computational complexity to keep information secret for some period of time, after which security expires. This topic in cryptography is still in a state where foundations are not well understood. For example, current analysis techniques of time-lock primitives provide no sound mechanism to build (composed) multi-party cryptographic protocols which use expiring security as a building block. Further, there are analyses that employ idealizations and simulators of unrealistic computational power to be an acceptable sound security argument. Our goal with this short paper is to advocate for understanding what approaches may lead to sound modeling beyond idealization, and what approaches may, in fact, be hopeless at this task of sound modeling. We explain in this paper how existing attempts at this subtle problem lack either composability, a fully consistent analysis, or functionality. The subtle flaws in the existing frameworks reduce to an impossibility result by Mahmoody et al., who showed that time-lock puzzles with super-polynomial gaps (between committer and solver) cannot be constructed from random oracles alone (or any repetitive computation where the next state is completely random given the prior state); yet still the analyses of algebraic puzzles today treat the solving process as if each step is a generic or random oracle. We point out that if the generation process relies on a trapdoor function that cannot be treated as a random oracle (to allow efficient generation while avoiding this impossibility result), then, to be consistent, the analysis of the solving process should also not treat such a trapdoor function (and its intermediate states) as a random oracle. We also delineate additional issues with the proof techniques used for time-lock puzzles. Specifically, when a time-lock puzzle must retain privacy for some amount of time, the reduction should bound the running time of the simulator. A simulator that can "simulate" if given time that if given to an adversary allows said adversary to solve the puzzle is not a valid security argument. We survey the adherence of various attempts to this principle, as well as the properties that different attempts achieve toward composition.

Mixnets are a fundamental privacy enhancing technology in the context of anonymous communication that have been extensively studied in terms of a Global passive Adversary (GPA). However a more realistic adversary that captures only a portion of the network have not yet been studied. We call these adversaries "Adversaries with Partial Visibility (APV)" In this paper we provide a framework that models the mixnet-based system and captures different types of Adversaries with Partial Visibility. Each adversary is modeled based on their goals, prior knowledge, and capabilities. We then use this model to perform traffic analysis using the Metropolis-Hastings algorithm in conjunction with a Bayesian inference engine. To the best of our knowledge this is the first time such an adversary is explicitly defined and studied, despite this adversary model being championed as more realistic than global passive adversaries in prior work. We highlight that our framework is flexible and able to encompass a broad range of different adversaries. Naturally, our model also captures the classical global passive adversary (GPA) as a special case.

Mutual distance bounding (DB) protocols enable two distrusting parties to establish an upper-bound on the distance between them. DB has been so far mainly considered in classical settings and for classical applications, especially in wireless settings, e.g., to prevent relay attacks in wireless authentication and access control systems, and for secure localization. While recent research has started exploring DB in quantum settings, all current quantum DB (QDB) protocols employ quantum-bits (qubits) in the rapid-bit exchange phase, and only perform one-way DB. Specifically, the latest QDB proposals improve initial ones by adding resistance to photon number splitting attacks, and improving round complexity by avoiding communication from the prover to verifier in the last authentication phase. This paper presents two new QDB protocols that differ from previously proposed protocols in several aspects: (1) to the best of our knowledge, our protocols are the first to utilize entangled qubits in the rapid-bit exchange phase, previous protocols relied on sending individual qubits, not those from a pair of entangled ones; (2) our second protocol can perform mutual QDB between two parties in one execution, previous QDB protocols had to be executed twice with the prover and verifier roles reversed in each execution; (3) the use of entangled qubits in our protocols thwarts attacks that previous QDB protocols were prone to; (4) and finally, our protocols also eliminate the need for communication from the prover to the verifier in the last authentication phase, which was necessary in some previous QDB protocols. Our work paves the way for several interesting research directions.

Today, two-party secure messaging is well-understood and widely adopted, e.g., Signal and WhatsApp. Multiparty protocols for secure group messaging are less mature and many protocols with different tradeoffs exist. Generally, such protocols require parties to first agree on a shared secret group key and then periodically update it while preserving forward secrecy (FS) and post compromise security (PCS). We present a new framework, called a key lattice, for managing keys in concurrent group messaging. Our framework can be seen as a "key management" layer that enables concurrent group messaging when secure pairwise channels are available. Security of group messaging protocols defined using the key lattice incorporates both FS and PCS simply and naturally. Our framework combines both FS and PCS into directional variants of the same abstraction, and additionally avoids dependence on time-based epochs.

Von Ahn, Hopper and Langford introduced the notion of steganographic a.k.a. covert computation, to capture distributed computation where the attackers must not be able to distinguish honest parties from entities emitting random bitstrings. This indistinguishability should hold for the duration of the computation except for what is revealed by the intended outputs of the computed functionality. An important case of covert computation is mutually authenticated key exchange, a.k.a. mutual authentication. Mutual authentication is a fundamental primitive often preceding more complex secure protocols used for distributed computation. However, standard authentication implementations are not covert, which allows a network adversary to target or block parties who engage in authentication. Therefore, mutual authentication is one of the premier use cases of covert computation and has numerous real-world applications, e.g., for enabling authentication over steganographic channels in a network controlled by a discriminatory entity. We improve on the state of the art in covert authentication by presenting a protocol that retains covertness and security under concurrent composition, has minimal message complexity, and reduces protocol bandwidth by an order of magnitude compared to previous constructions. To model the security of our scheme we develop a UC model which captures standard features of secure mutual authentication but extends them to covertness. We prove our construction secure in this UC model. We also provide a proof-of-concept implementation of our scheme.

Fully homomorphic encryption (FHE) schemes are either lightweight and can evaluate boolean circuits or are relatively heavy and can evaluate arithmetic circuits on encrypted vectors, i.e., they perform single instruction multiple data operations (SIMD). SIMD FHE schemes can either perform exact modular arithmetic in the case of the Brakerski-Gentry-Vaikuntanathan (BGV) and Brakerski-Fan-Vercauteren (BFV) schemes or approximate arithmetic in the case of the Cheon-Kim-Kim-Song (CKKS) scheme. While one can homomorphically switch between BGV/BFV and CKKS using the computationally expensive bootstrapping procedure, it is unknown how to switch between these schemes without bootstrapping. Finding more efficient methods than bootstrapping of converting between these schemes was stated as an open problem by Halevi and Shoup, Eurocrypt 2015 [ 33 , 34 ]. In this work, we provide strong evidence that homomorphic switching between BGV/BFV and CKKS is as hard as bootstrapping. In more detail, if one could efficiently switch between these SIMD schemes, then one could bootstrap these SIMD FHE schemes using a single call to a homomorphic scheme-switching algorithm without applying homomorphic linear transformations . Thus, one cannot hope to obtain significant improvements to homomorphic scheme-switching without also significantly improving the state-of-the-art for bootstrapping. We also explore the relative hardness of computing homomorphic comparison in these same SIMD FHE schemes as a secondary contribution. We show that given a comparison algorithm, one can bootstrap these schemes using a few calls to the comparison algorithm for typical parameter settings. While we focus on the comparison function in this work, the overall approach to demonstrate relative hardness of computing specific functions homomorphically extends beyond comparison to other useful functions such as min/max or ReLU.

. The introduction of time-lock puzzles initiated the study of publicly “sending information into the future.” For time-lock puzzles, the underlying security-enabling mechanism is the computational complexity of the operations needed to solve the puzzle, which must be tunable to reveal the solution after a predetermined time, and not before that time. Time-lock puzzles are typically constructed via a commitment to a secret, paired with a reveal algorithm that sequentially iterates a basic function over such commitment. One then shows that short-cutting the iterative process violates cryptographic hardness of an underlying problem. To date, and for more than twenty-five years, research on time-lock puzzles relied heavily on iteratively applying well-structured algebraic functions. However, despite the tradition of cryptography to reason about primitives in a realistic model with standard hardness assumptions (often after initial idealized assumptions), most analysis of time-lock puzzles to date still relies on cryptography modeled (in an ideal manner) as a random oracle function or a generic group function. Moreover, Mahmoody et al. showed that time-lock puzzles with superpolynomial gap cannot be constructed from random-oracles; yet still, current treatments generally use an algebraic trapdoor to efficiently construct a puzzle with a large time gap, and then apply the inconsistent (with respect to Mahmoody et al.) random-oracle idealizations to analyze the solving process. Finally, little attention has been paid to the nuances of composing multi-party computation with timed puzzles that are solved as part of the protocol . In this work, we initiate a study of time-lock puzzles in a model built upon a realistic (and falsifiable) computational framework. We present a new formal definition of residual complexity to characterize a realistic, gradual time-release for time-lock puzzles. We also present a general definition of timed multi-party computation (MPC) and both sequential and concurrent composition theorems for MPC in our model.

Despite the notable advances in the development of high-assurance, verified implementations of cryptographic protocols, such implementations typically face significant performance overheads, particularly due to the penalties induced by formal verification and automated extraction of executable code. In this paper, we address some core performance challenges facing computer-aided cryptography by presenting a formal treatment for accelerating such verified implementations based on multiple generic optimizations covering parallelism and memory access. We illustrate our techniques for addressing such performance bottlenecks using the Line-Point Zero-Knowledge (LPZK) protocol as a case study. Our starting point is a new verified implementation of LPZK that we formalize and synthesize using EasyCrypt; our first implementation is developed to reduce the proof effort and without considering the performance of the extracted executable code. We then show how such (automatically) extracted code can be optimized in three different ways to obtain a 3000x speedup and thus matching the performance of the manual implementation of LPZK of lpzkv2.[13] We obtain such performance gains by first modifying the algorithmic specifications, then by adopting a provably secure parallel execution model, and finally by optimizing the memory access structures. All optimizations are first formally verified inside EasyCrypt, and then executable code is automatically synthesized from each step of the formalization. For each optimization, we analyze performance gains resulting from it and also address challenges facing the computer-aided security proofs thereof, and challenges facing automated synthesis of executable code with such an optimization.

Secure multiparty computation (MPC) has recently been increasingly adopted to secure cryptographic keys in enterprises, cloud infrastructure, and cryptocurrency and blockchain-related settings such as wallets and exchanges. Using MPC in blockchains and other distributed systems highlights the need to consider dynamic settings. In such dynamic settings, parties, and potentially even parameters of underlying secret sharing and corruption tolerance thresholds of sub-protocols, may change over the lifetime of the protocol. In particular, stronger threat models – in which mobile adversaries control a changing set of parties (up to t out of n involved parties at any instant), and may eventually corrupt all n parties over the course of a protocol’s execution – are becoming increasingly important for such real world deployments; secure protocols designed for such models are known as Proactive MPC (PMPC). In this work, we construct the first efficient PMPC protocol for dynamic groups (where the set of parties changes over time) secure against a dishonest majority of parties. Our PMPC protocol only requires O(n^2) (amortized) communication per secret, compared to existing PMPC protocols that require O(n^4) and only consider static groups with dishonest majorities. At the core of our PMPC protocol is a new efficient technique to perform multiplication of secret shared data (shared using a bivariate scheme) with O(n √(n)) communication with security against a dishonest majority without requiring pre-computation. We also develop a new efficient bivariate batched proactive secret sharing (PSS) protocol for dishonest majorities, which may be of independent interest. This protocol enables multiple dealers to contribute different secrets that are efficiently shared together in one batch; previous batched PSS schemes required all secrets to come from a single dealer.

The interplay between cryptography and access control has been widely investigated in the literature. For example, attribute-based encryption (ABE) is a leading candidate of a cryptographic tool going beyond the all-or-nothing approach of public-key encryption by supporting fine-grained access control for encrypted data. Unfortunately, the deployment and adoption of ABE have been slow, and (to the best of our knowledge) few commercial widely-used products use it to date. In particular, selective and fine-grained control over what is shared, and with whom, is absent from common data products and formats, such as those generated by commercial authoring products, e.g., Microsoft Word documents, Excel spreadsheets, PowerPoint slides. This lack of selective and fine-grained control results in users simply not sharing. This major usability shortcoming impacts defense and military coalition operations, as well as commercial settings, such as life sciences, healthcare, and the financial sectors. This paper addresses the above usability problem head-on by proposing a crypto- graphically enforced selective access control in Microsoft Office products and similar platforms. We focus on Excel as an illustrative use-case, but note that our work is applicable to (and is already implemented for) other Microsoft products such as Word, PowerPoint, and Outlook. Using the JavaScript API for Microsoft Office, we designed and developed simple add-ins that enable cell encryption according to a policy, and requires a key that embeds attributes satisfying the policy in order to decrypt. Our performance evaluation not only shows that cryptographic-based selective sharing of information in widely-deployed and widely-used commercial authoring and collaboration platforms is possible, but also practical.

Fully Homomorphic Encryption (FHE) enables offloading computation to untrusted servers with cryptographic privacy. Despite its attractive security, FHE is not yet widely adopted due to its prohibitive overheads, about 10,000X over unencrypted computation. Recent FHE accelerators have made strides to bridge this performance gap. Unfortunately, prior accelerators only work well for simple programs, but become inefficient for complex programs, which bring additional costs and challenges. We present CraterLake, the first FHE accelerator that enables FHE programs of unbounded size (i.e., unbounded multiplicative depth). Such computations require very large ciphertexts (tens of MBs each) and different algorithms that prior work does not support well. To tackle this challenge, CraterLake introduces a new hardware architecture that efficiently scales to very large cipher-texts, novel functional units to accelerate key kernels, and new algorithms and compiler techniques to reduce data movement. We evaluate CraterLake on deep FHE programs, including deep neural networks like ResNet and LSTMs, where prior work takes minutes to hours per inference on a CPU. CraterLake outperforms a CPU by gmean 4,600X and the best prior FHE accelerator by 11.2X under similar area and power budgets. These speeds enable realtime performance on unbounded FHE programs for the first time.

Consensus protocols enable n parties, each holding some input string, to agree on a common output even in the presence of corrupted parties. Recent work has pushed to understand the problem when a majority of parties may be corrupted thus providing higher resilience, and under various forms of corruptions. Zikas, Hauser, and Maurer introduced a model in which receive-corrupt parties may not receive messages sent to them, and send-corrupt parties may have their sent messages dropped. Otherwise, receive-corrupt and send-corrupt parties behave honestly and their inputs and outputs are constrained by the security definitions. Zikas, Hauser, and Maurer gave a perfectly secure, linear-round protocol for n > t_𝗋𝖼𝗏+t_𝗌𝗇𝖽+3t_𝖻𝗒𝗓 , where t_𝗋𝖼𝗏 , t_𝗌𝗇𝖽 , and t_𝖻𝗒𝗓 represent thresholds on receive-, send-, and byzantine-corruptions. We present the first expected constant-round protocol in the general corruption model tolerating n > t_𝗋𝖼𝗏+2t_𝗌𝗇𝖽+2t_𝖻𝗒𝗓 . In comparison, all current sublinear round consensus protocols fail if there exists even a single party which cannot communicate with some honest parties, but whose output must be consistent with the honest parties. While presenting our protocol, we explore the pathology of send-corruptions and characterize the difficulty of dealing with them in sublinear-round protocols. As an illustrative and surprising example (even though not in sublinear rounds), we show that the classical Dolev-Strong broadcast protocol degrades from tolerating t_𝖻𝗒𝗓< n corruptions in the byzantine-only model to t_𝖻𝗒𝗓< n/2 - t_𝗌𝗇𝖽 when send-corrupt parties’ outputs must be consistent with honest parties; we also show why other recent dishonest-majority broadcast protocols degrade similarly. We prove that our new consensus protocol achieves an optimal threshold of n > t_𝗋𝖼𝗏+t_𝗌𝗇𝖽+2t_𝖻𝗒𝗓 when we constrain the adversary to either drop all or none of a sender’s messages in a round (we denote this model by spotty send corruptions). To our knowledge, our protocol for the spotty send corruption model is thus the first sublinear-round consensus protocol for a majority of online faulty parties in any model. Because we are unable to prove optimality of our protocol’s corruption budget in the general case, we leave open the question of optimal corruption tolerance for both send-corruptions and byzantine-corruptions.

This paper introduces two techniques that make the standard Quantum Approximate Optimization Algorithm (QAOA) more suitable for constrained optimization problems. The first technique describes how to use the outcome of a prior greedy classical algorithm to define an initial quantum state and mixing operation to adjust the quantum optimization algorithm to explore the possible answers around this initial greedy solution. The second technique is used to nudge the quantum exploration to avoid the local minima around the greedy solutions. To analyze the benefits of these two techniques we run the quantum algorithm on known hard instances of the Knapsack Problem using unit depth quantum circuits. The results show that the adjusted quantum optimization heuristics typically perform better than various classical heuristics.

We look at two basic coding theoretic and cryptographic mechanisms developed separately and investigate relationships between them and their implications. The first mechanism is Proactive Secret Sharing (PSS), which allows randomization and repair of shares using information from other shares. PSS enables constructing secure multi-party computation protocols that can withstand mobile dynamic attacks. This self-recovery and the redundancy of uncorrupted shares allows a system to overcome recurring faults throughout its lifetime, eventually finishing the computation (or continuing forever to maintain stored data). The second mechanism is Regenerating Codes (RC) which were extensively studied and adopted in distributed storage systems. RC are error correcting (or erasure handling) codes capable of recovering a block of a distributedly held codeword from other servers' blocks. This self-healing nature enables more robustness of a code distributed over different machines. Given that the two mechanisms have a built-in self-healing (leading to stabilizing) and that both can be based on Reed Solomon Codes, it is natural to formally investigate deeper relationships between them. We prove that a PSS scheme can be converted into an RC scheme, and that under some conditions RC can be utilized to instantiate a PSS scheme. This allows us, in turn, to leverage recent results enabling more efficient polynomial interpolation (due to Guruswami and Wooters) to improve the efficiency of a PSS scheme. We also show that if parameters are not carefully calibrated, such interpolation techniques (allowing partial word leakage) may be used to attack a PSS scheme over time. Secondly, the above relationships give rise to extended (de)coding notions. Our first example is mapping the generalized capabilities of adversaries (called generalized adversary structures) from the PSS realm into the RC one. Based on this we define a new variant of RC we call Generalized-decoding Regenerating Code (GRC) where not all network servers have a uniform sub-codeword (motivated by non-uniform probability of attacking different servers case). We finally highlight several interesting research directions due to our results, e.g., designing new improved GRC, and more adaptive RC re-coding techniques.

The recent work of Garg et al. from TCC’18 introduced the notion of registration based encryption (RBE). The principal motivation behind RBE is to address the key escrow issue of identity based encryption (IBE), where an IBE authority is trusted to generate private keys for all users in the system. Although RBE has excellent asymptotic properties, it is currently impractical; in our estimate, ciphertext size would be about 11 TB in an RBE deployment supporting 2 billion users. Motivated by this observation, our work attempts to reduce the concrete communication and computation cost of the current state-of-the-art construction. Our contribution is two-fold. First, we replace the usage of Merkle trees in RBE with crit-bit trees, a form of PATRICIA trie, without relaxing any of the original efficiency requirements introduced by Garg et al. This change reduces the ciphertext size by 15

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) protocols. In this paper we present the first machine-checked implementations of MitH. We begin with an EasyCrypt formalization that preserves the modular structure of the original construction and can be instantiated with arbitrary MPC protocols, and 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 executable implementations. The first uses a fully automated extraction from EasyCrypt to OCaml. The second reduces the trusted computing base (TCB) and provides better performance by combining code extraction with formally verified manual low-level components implemented in the Jasmin language. We conclude with a discussion of the trade-off between the formal verification effort and the performance of resulting executables, and how our approach opens the way for fully verified implementations of state-of the-art optimized protocols based on MitH.

Modern society is increasingly surrounded by, and accustomed to, a wide range of Cyber-Physical Systems (CPS), Internet-of-Things (IoT), and smart devices. They often perform safety-critical functions, e.g., personal medical devices, automotive CPS and industrial automation (smart factories). Some devices are small, cheap and specialized sensors and/or actuators. They tend to run simple software and operate under control of a more sophisticated central control unit. The latter is responsible for the decision-making and orchestrating the entire system. If devices are left unprotected, consequences of forged sensor readings or ignored actuation commands can be catastrophic, particularly, in safety-critical settings. This prompts the following three questions: (1) How to trust data produced by a simple remote embedded device? and (2) How to ascertain that this data was produced via execution of expected software? Furthermore, (3) Is it possible to attain (1) and (2) under the assumption that all software on the remote device could be modified or compromised? In this paper we answer these questions by designing, proving security of, and formally verifying, VAPE: Verified Architecture for Proofs of Execution. To the best of our knowledge, this is the first of its kind result for low-end embedded systems. Our work has a range of applications, especially, to authenticated sensing and trustworthy actuation, which are increasingly relevant in the context of safety-critical systems. VAPE architecture is publicly available and our evaluation demonstrates that it incurs low overhead, affordable even for lowest-end embedded devices, e.g., those based on MSP430 or ARV ATMega processors.