Myrto Arapinis

Jingxin Qiao, Myrto Arapinis, Thomas Zacharias

Coercion-resistance (CR) is a crucial security property in e-voting systems. It ensures that an attacker cannot compel a voter to vote in a specific way by using threats or rewards. The Loki e-voting protocol, proposed by Giustolisi \emph{et al.} at IEEE S\&P (2024), introduces a novel design that mitigates last-minute coercion through a re-voting mechanism. It also aims to address the usability issues of the seminal JCJ e-voting protocol, specifically: i) the requirement that voters can store and hide pre-agreed credentials, and ii) the ability of voters to convincingly lie while being coerced. In this work, we identify two vulnerabilities in Loki. The first is a brute-force attack that compromises the integrity of the evasion strategy. Specifically, this attack allows an adversary to cast a ballot on behalf of their victim in a way that the evasion strategy cannot defend against, rendering it ineffective. The second vulnerability is a forced abstention attack, which allows an adversary to detect when their victim has complied with their instruction not to vote. We generalise the integrity attack to reveal a fundamental dilemma: without pre-agreed secret credentials, it is not possible to prevent last-minute coercion. Finally, we show how reverting to pre-agreed secret credentials fixes the aforementioned vulnerabilities and discuss the trade-off between tallying efficiency and stronger trust assumptions.

Kaushik Chakraborty, Mina Doosti, Yao Ma et al.

Physical unclonable functions(PUFs) provide a unique fingerprint to a physical entity by exploiting the inherent physical randomness. Gao et al. discussed the vulnerability of most current-day PUFs to sophisticated machine learning-based attacks. We address this problem by integrating classical PUFs and existing quantum communication technology. Specifically, this paper proposes a generic design of provably secure PUFs, called hybrid locked PUFs(HLPUFs), providing a practical solution for securing classical PUFs. An HLPUF uses a classical PUF(CPUF), and encodes the output into non-orthogonal quantum states to hide the outcomes of the underlying CPUF from any adversary. Here we introduce a quantum lock to protect the HLPUFs from any general adversaries. The indistinguishability property of the non-orthogonal quantum states, together with the quantum lockdown technique prevents the adversary from accessing the outcome of the CPUFs. Moreover, we show that by exploiting non-classical properties of quantum states, the HLPUF allows the server to reuse the challenge-response pairs for further client authentication. This result provides an efficient solution for running PUF-based client authentication for an extended period while maintaining a small-sized challenge-response pairs database on the server side. Later, we support our theoretical contributions by instantiating the HLPUFs design using accessible real-world CPUFs. We use the optimal classical machine-learning attacks to forge both the CPUFs and HLPUFs, and we certify the security gap in our numerical simulation for construction which is ready for implementation.

Yao Ma, Elham Kashefi, Myrto Arapinis et al.

We introduce a secure hardware device named a QEnclave that can secure the remote execution of quantum operations while only using classical controls. This device extends to quantum computing the classical concept of a secure enclave which isolates a computation from its environment to provide privacy and tamper-resistance. Remarkably, our QEnclave only performs single-qubit rotations, but can nevertheless be used to secure an arbitrary quantum computation even if the qubit source is controlled by an adversary. More precisely, attaching a QEnclave to a quantum computer, a remote client controlling the QEnclave can securely delegate its computation to the server solely using classical communication. We investigate the security of our QEnclave by modeling it as an ideal functionality named Remote State Rotation. We show that this resource, similar to previously introduced functionality of remote state preparation, allows blind delegated quantum computing with perfect security. Our proof relies on standard tools from delegated quantum computing. Working in the Abstract Cryptography framework, we show a construction of remote state preparation from remote state rotation preserving the security. An immediate consequence is the weakening of the requirements for blind delegated computation. While previous delegated protocols were relying on a client that can either generate or measure quantum states, we show that this same functionality can be achieved with a client that only transforms quantum states without generating or measuring them.

Mina Doosti, Mahshid Delavar, Elham Kashefi et al.

In this paper, we continue the line of work initiated by Boneh and Zhandry at CRYPTO 2013 and EUROCRYPT 2013 in which they formally define the notion of unforgeability against quantum adversaries specifically, for classical message authentication codes and classical digital signatures schemes. We develop a general and parameterised quantum game-based security model unifying unforgeability for both classical and quantum constructions allowing us for the first time to present a complete quantum cryptanalysis framework for unforgeability. In particular, we prove how our definitions subsume previous ones while considering more fine-grained adversarial models, capturing the full spectrum of superposition attacks. The subtlety here resides in the characterisation of a forgery. We show that the strongest level of unforgeability, namely existential unforgeability, can only be achieved if only orthogonal to previously queried messages are considered to be forgeries. In particular, we present a non-trivial attack if any overlap between the forged message and previously queried ones is allowed. We further show that deterministic constructions can only achieve the weaker notion of unforgeability, that is selective unforgeability, against such restricted adversaries, but that selective unforgeability breaks if general quantum adversaries (capable of general superposition attacks) are considered. On the other hand, we show that PRF is sufficient for constructing a selective unforgeable classical primitive against full quantum adversaries. Moreover, we show similar positive results relying on Pseudorandom Unitaries (PRU) for quantum primitives. These results demonstrate the generality of our framework that could be applicable to other primitives beyond the cases analysed in this paper.

Myrto Arapinis, Mahshid Delavar, Mina Doosti et al.

A Physical Unclonable Function (PUF) is a device with unique behaviour that is hard to clone hence providing a secure fingerprint. A variety of PUF structures and PUF-based applications have been explored theoretically as well as being implemented in practical settings. Recently, the inherent unclonability of quantum states has been exploited to derive the quantum analogue of PUF as well as new proposals for the implementation of PUF. We present the first comprehensive study of quantum Physical Unclonable Functions (qPUFs) with quantum cryptographic tools. We formally define qPUFs, encapsulating all requirements of classical PUFs as well as introducing a new testability feature inherent to the quantum setting only. We use a quantum game-based framework to define different levels of security for qPUFs: quantum exponential unforgeability, quantum existential unforgeability and quantum selective unforgeability. We introduce a new quantum attack technique based on the universal quantum emulator algorithm of Marvin and Lloyd to prove no qPUF can provide quantum existential unforgeability. On the other hand, we prove that a large family of qPUFs (called unitary PUFs) can provide quantum selective unforgeability which is the desired level of security for most PUF-based applications.

Myrto Arapinis, Elham Kashefi, Nikolaos Lamprou et al.

Recent advances indicate that quantum computers will soon be reality. Motivated by this ever more realistic threat for existing classical cryptographic protocols, researchers have developed several schemes to resist "quantum attacks". In particular, for electronic voting, several e-voting schemes relying on properties of quantum mechanics have been proposed. However, each of these proposals comes with a different and often not well-articulated corruption model, has different objectives, and is accompanied by security claims which are never formalized and are at best justified only against specific attacks. To address this, we propose the first formal security definitions for quantum e-voting protocols. With these at hand, we systematize and evaluate the security of previously-proposed quantum e-voting protocols; we examine the claims of these works concerning privacy, correctness and verifiability, and if they are correctly attributed to the proposed protocols. In all non-trivial cases, we identify specific quantum attacks that violate these properties. We argue that the cause of these failures lies in the absence of formal security models and references to the existing cryptographic literature.

Myrto Arapinis, Vincent Cheval, Stéphanie Delaune

Security protocols are used in many of our daily-life applications, and our privacy largely depends on their design. Formal verification techniques have proved their usefulness to analyse these protocols, but they become so complex that modular techniques have to be developed. We propose several results to safely compose security protocols. We consider arbitrary primitives modeled using an equational theory, and a rich process algebra close to the applied pi calculus. Relying on these composition results, we are able to derive some security properties on a protocol from the security analysis performed on each sub-protocol individually. We consider parallel composition and the case of key-exchange protocols. Our results apply to deal with confidentiality but also privacy-type properties (e.g. anonymity, unlinkability) expressed using a notion of equivalence. We illustrate the usefulness of our composition results on protocols from the 3G phone application and electronic passport.

Myrto Arapinis, Stéphanie Delaune, Steve Kremer

The design and verification of cryptographic protocols is a notoriously difficult task, even in symbolic models which take an abstract view of cryptography. This is mainly due to the fact that protocols may interact with an arbitrary attacker which yields a verification problem that has several sources of unboundedness (size of messages, number of sessions, etc. In this paper, we characterize a class of protocols for which deciding security for an unbounded number of sessions is decidable. More precisely, we present a simple transformation which maps a protocol that is secure for a bounded number of protocol sessions (a decidable problem) to a protocol that is secure for an unbounded number of sessions. The precise number of sessions that need to be considered is a function of the security property and we show that for several classical security properties a single session is sufficient. Therefore, in many cases our results yields a design strategy for security protocols: (i) design a protocol intended to be secure for a {single session}; and (ii) apply our transformation to obtain a protocol which is secure for an unbounded number of sessions.