263 results sorted by ID
Key-Homomorphic and Aggregate Verifiable Random Functions
Giulio Malavolta
Public-key cryptography
A verifiable random function (VRF) allows one to compute a random-looking image, while at the same time providing a unique proof that the function was evaluated correctly. VRFs are a cornerstone of modern cryptography and, among other applications, are at the heart of recently proposed proof-of-stake consensus protocols. In this work we initiate the formal study of aggregate VRFs, i.e., VRFs that allow for the aggregation of proofs/images into a small di- gest, whose size is independent of...
An Efficient Adaptive Attack Against FESTA
Guoqing Zhou, Maozhi Xu
Attacks and cryptanalysis
At EUROCRYPT’23, Castryck and Decru, Maino et al., and Robert present efficient attacks against supersingular isogeny Diffie-Hellman key exchange protocol (SIDH). Drawing inspiration from these attacks, Andrea Basso, Luciano Maino, and Giacomo Pope introduce FESTA, an isogeny-based trapdoor function, along with a corresponding IND-CCA secure public key encryption (PKE) protocol at ASIACRYPT’23. FESTA incorporates either a diagonal or circulant matrix into the secret key to mask torsion...
Formal Verification of Emulated Floating-Point Arithmetic in Falcon
Vincent Hwang
Implementation
We show that there is a discrepancy between the emulated floating-point multiplications in the submission package of Falcon and the claimed behavior. In particular, we show that floating-point products with absolute values the smallest normal positive floating-point number are incorrectly zeroized. However, we show that the discrepancy doesn’t effect the complex fast Fourier transform by modeling the floating-point addition, subtraction, and multiplication in CryptoLine. We later implement...
Polynomial Commitments from Lattices: Post-Quantum Security, Fast Verification and Transparent Setup
Valerio Cini, Giulio Malavolta, Ngoc Khanh Nguyen, Hoeteck Wee
Cryptographic protocols
Polynomial commitment scheme allows a prover to commit to a polynomial $f \in \mathcal{R}[X]$ of degree $L$, and later prove that the committed function was correctly evaluated at a specified point $x$; in other words $f(x)=u$ for public $x,u \in\mathcal{R}$. Most applications of polynomial commitments, e.g. succinct non-interactive arguments of knowledge (SNARKs), require that (i) both the commitment and evaluation proof are succinct (i.e., polylogarithmic in the degree $L$) - with the...
zkPi: Proving Lean Theorems in Zero-Knowledge
Evan Laufer, Alex Ozdemir, Dan Boneh
Applications
Interactive theorem provers (ITPs), such as Lean and Coq, can express
formal proofs for a large category of theorems, from abstract math to
software correctness. Consider Alice who has a Lean proof for some
public statement $T$. Alice wants to convince the world that she has
such a proof, without revealing the actual proof. Perhaps the proof
shows that a secret program is correct or safe, but the proof itself
might leak information about the program's source code. A natural way
for...
Fault-Resistant Partitioning of Secure CPUs for System Co-Verification against Faults
Simon Tollec, Vedad Hadžić, Pascal Nasahl, Mihail Asavoae, Roderick Bloem, Damien Couroussé, Karine Heydemann, Mathieu Jan, Stefan Mangard
Implementation
To assess the robustness of CPU-based systems against fault injection attacks, it is necessary to analyze the consequences of the fault propagation resulting from the intricate interaction between the software and the processor. However, current formal methodologies that combine both hardware and software aspects experience scalability issues, primarily due to the use of bounded verification techniques.
This work formalizes the notion of $k$-fault resistant partitioning as an inductive...
Alba: The Dawn of Scalable Bridges for Blockchains
Giulia Scaffino, Lukas Aumayr, Mahsa Bastankhah, Zeta Avarikioti, Matteo Maffei
Cryptographic protocols
Over the past decade, cryptocurrencies have garnered attention from academia and industry alike, fostering a diverse blockchain ecosystem and novel applications. The inception of bridges improved interoperability, enabling asset transfers across different blockchains to capitalize on their unique features. Despite their surge in popularity and the emergence of Decentralized Finance (DeFi), trustless bridge protocols remain inefficient, either relaying too much information (e.g.,...
Efficient ECDSA-based Adaptor Signature for Batched Atomic Swaps
Binbin Tu, Min Zhang, Yu Chen
Public-key cryptography
Adaptor signature is a novel cryptographic primitive which ties together the signature and the leakage of a secret value. It has become an important tool for solving the scalability and interoperability problems in the blockchain. Aumayr et al. (Asiacrypt 2021) recently provide the formalization of the adaptor signature and present a provably secure ECDSA-based adaptor signature, which requires zero-knowledge proof in the pre-signing phase to ensure the signer works correctly. However, the...
Automatic Verification of Cryptographic Block Function Implementations with Logical Equivalence Checking
Li-Chang Lai, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
Implementation
Given a fixed-size block, cryptographic block functions gen-
erate outputs by a sequence of bitwise operations. Block functions are
widely used in the design of hash functions and stream ciphers. Their
correct implementations hence are crucial to computer security. We pro-
pose a method that leverages logic equivalence checking to verify assem-
bly implementations of cryptographic block functions. Logic equivalence
checking is a well-established technique from hardware verification....
Lattice-based Programmable Hash Functions and Applications
Jiang Zhang, Yu Chen, Zhenfeng Zhang
Public-key cryptography
Driven by the open problem raised by Hofheinz and Kiltz
(Journal of Cryptology, 2012), we study the formalization of lattice-based programmable hash function (PHF), and give three types of concrete constructions by using several techniques such as a novel combination of cover-free sets and lattice trapdoors. Under the Inhomogeneous Small Integer Solution (ISIS) assumption, we show that any (non-trivial) lattice-based PHF is a collision-resistant hash function, which gives a direct...
ZKSMT: A VM for Proving SMT Theorems in Zero Knowledge
Daniel Luick, John Kolesar, Timos Antonopoulos, William R. Harris, James Parker, Ruzica Piskac, Eran Tromer, Xiao Wang, Ning Luo
Cryptographic protocols
Verification of program safety is often reducible to proving the unsatisfiability (i.e., validity) of a formula in Satisfiability Modulo Theories (SMT): Boolean logic combined with theories that formalize arbitrary first-order fragments. Zero-knowledge (ZK) proofs allow SMT formulas to be validated without revealing the underlying formulas or their proofs to other parties, which is a crucial building block for proving the safety of proprietary programs. Recently, Luo et al. (CCS 2022)...
2023/1753
Last updated: 2023-11-27
Formal verification of the post-quantum security properties of IKEv2 PPK (RFC 8784) using the Tamarin Prover
Sophie Stevens
Cryptographic protocols
The Internet Key Exchange version 2 (IKEv2) (RFC 7296) is a component of IPsec used to authenticate two parties (the initiator and responder) to each other and to establish a set of security parameters for the communications. The security parameters include secret keys to encrypt and authenticate data as well as the negotiation of a set of cryptographic algorithms. The core documentation uses exclusively Diffie-Hellman exchanges to agree the security information. However, this is not a...
Memory Checking for Parallel RAMs
Surya Mathialagan
Cryptographic protocols
When outsourcing a database to an untrusted remote server, one might want to verify the integrity of contents while accessing it. To solve this, Blum et al. [FOCS `91] propose the notion of memory checking. Memory checking allows a user to run a RAM program on a remote server, with the ability to verify integrity of the storage with small local storage.
In this work, we define and initiate the formal study of memory checking for Parallel RAMs (PRAMs). The parallel RAM...
Predicate Aggregate Signatures and Applications
Tian Qiu, Qiang Tang
Public-key cryptography
Motivated by applications in anonymous reputation systems and blockchain governance, we initiate the study of predicate aggregate signatures (PAS), which is a new primitive that enables users to sign multiple messages, and these individual signatures can be aggregated by a combiner, preserving the anonymity of the signers. The resulting PAS discloses only a brief description of signers for each message and provides assurance that both the signers and their description satisfy the specified...
Comparse: Provably Secure Formats for Cryptographic Protocols
Théophile Wallez, Jonathan Protzenko, Karthikeyan Bhargavan
Cryptographic protocols
Data formats used for cryptographic inputs have historically been the source of many attacks on cryptographic protocols, but their security guarantees remain poorly studied. One reason is that, due to their low-level nature, formats often fall outside of the security model. Another reason is that studying all of the uses of all of the formats within one protocol is too difficult to do by hand, and requires a comprehensive, automated framework.
We propose a new framework, “Comparse”, that...
Combined Private Circuits - Combined Security Refurbished
Jakob Feldtkeller, Tim Güneysu, Thorben Moos, Jan Richter-Brockmann, Sayandeep Saha, Pascal Sasdrich, François-Xavier Standaert
Implementation
Physical attacks are well-known threats to cryptographic implementations. While countermeasures against passive Side-Channel Analysis (SCA) and active Fault Injection Analysis (FIA) exist individually, protecting against their combination remains a significant challenge. A recent attempt at achieving joint security has been published at CCS 2022 under the name CINI-MINIS. The authors introduce relevant security notions and aim to construct arbitrary-order gadgets that remain trivially...
Layered Symbolic Security Analysis in DY$^\star$
Karthikeyan Bhargavan, Abhishek Bichhawat, Pedram Hosseyni, Ralf Kuesters, Klaas Pruiksma, Guido Schmitz, Clara Waldmann, Tim Würtele
Foundations
While cryptographic protocols are often analyzed in isolation, they are typically deployed within a stack of protocols, where each layer relies on the security guarantees provided by the protocol layer below it, and in turn provides its own security functionality to the layer above. Formally analyzing the whole stack in one go is infeasible even for semi-automated verification tools, and impossible for pen-and-paper proofs. The DY$^\star$ protocol verification framework offers a modular and...
Boosting the Performance of High-Assurance Cryptography: Parallel Execution and Optimizing Memory Access in Formally-Verified Line-Point Zero-Knowledge
Samuel Dittmer, Karim Eldefrawy, Stéphane Graham-Lengrand, Steve Lu, Rafail Ostrovsky, Vitor Pereira
Cryptographic protocols
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...
Compositional Formal Verification of Zero-Knowledge Circuits
Alessandro Coglio, Eric McCarthy, Eric Smith, Collin Chin, Pranav Gaddamadugu, Michel Dellepere
Applications
We provide a preliminary report of our ongoing work in formally defining and verifying, in a compositional way, the R1CS gadgets generated by Aleo's snarkVM. The approach is applicable to other systems that generate gadgets in a similar manner, and that may use non-R1CS representations.
Faster constant-time evaluation of the Kronecker symbol with application to elliptic curve hashing
Diego F. Aranha, Benjamin Salling Hvass, Bas Spitters, Mehdi Tibouchi
Implementation
We generalize the Bernstein-Yang (BY) algorithm for constant-time modular inversion to compute the Kronecker symbol, of which the Jacobi and Legendre symbols are special cases. We start by developing a basic and easy-to-implement divstep version of the algorithm defined in terms of full-precision division steps. We then describe an optimized version due to Hamburg over word-sized inputs, similar to the jumpdivstep version of the BY algorithm, and formally verify its correctness. Along the...
Privacy-Preserving Outsourced Certificate Validation
Tarek Galal, Anja Lehmann
Cryptographic protocols
Digital Covid certificates are the first widely deployed end-user cryptographic certificates. For service providers, such as airlines or event ticket vendors, that needed to check that their (global) customers satisfy certain health policies, the verification of such Covid certificates was challenging though - not because of the cryptography involved, but due to the multitude of issuers, different certificate types and the evolving nature of country-specific policies that had to be...
A Methodology to Achieve Provable Side-Channel Security in Real-World Implementations
Sonia Belaïd, Gaëtan Cassiers, Camille Mutschler, Matthieu Rivain, Thomas Roche, François-Xavier Standaert, Abdul Rahman Taleb
Physical side-channel attacks exploit a device's emanations to compromise the security of cryptographic implementations.
Many countermeasures have been proposed against these attacks, especially the widely-used and efficient masking countermeasure.
While theoretical models offer formal security proofs, they often rest on unrealistic assumptions, leading current approaches to prove the security of masked implementations to primarily rely on empirical verification.
Consequently, the...
An Anonymous Authenticated Key Agreement Protocol Secure in Partially Trusted Registration Server Scenario for Multi-Server Architectures
Inam ul Haq, Jian Wang, Youwen Zhu, Sheharyar Nasir
Cryptographic protocols
The accelerated advances in information communication technologies have made it possible for enterprises to deploy large scale applications in a multi-server architecture (also known as cloud computing environment). In this architecture, a mobile user can remotely obtain desired services over the Internet from multiple servers by initially executing a single registration on a trusted registration server (RS). Due to the hazardous nature of the Internet, to protect user privacy and online...
Benchmarking the Setup of Updatable zk-SNARKs
Karim Baghery, Axel Mertens, Mahdi Sedaghat
Cryptographic protocols
Subversion-resistant zk-SNARKs allow the provers to verify the Structured Reference String (SRS), via an SRS Verification (SV) algorithm and bypass the need for a Trusted Third Party (TTP). Pairing-based zk-SNARKs with \(updatable\) and \(universal\) SRS are an extension of subversion-resistant ones which additionally allow the verifiers to update the SRS, via an SRS Updating (SU) algorithm, and similarly bypass the need for a TTP. In this paper, we examine the setup of these zk-SNARKs by...
Post Quantum Fuzzy Stealth Signatures and Applications
Sihang Pu, Sri AravindaKrishnan Thyagarajan, Nico Döttling, Lucjan Hanzlik
Public-key cryptography
Private payments in blockchain-based cryptocurrencies have been a topic of research, both academic and industrial, ever since the advent of Bitcoin. Stealth address payments were proposed as a solution to improve payment privacy for users and are, in fact, deployed in several major cryptocurrencies today. The mechanism lets users receive payments so that none of these payments are linkable to each other or the recipient. Currently known stealth address mechanisms either (1) are insecure in...
Moving a Step of ChaCha in Syncopated Rhythm
Shichang Wang, Meicheng Liu, Shiqi Hou, Dongdai Lin
Attacks and cryptanalysis
The stream cipher ChaCha is one of the most widely used ciphers in the real world, such as in TLS, SSH and so on. In this paper, we study the security of ChaCha via differential cryptanalysis based on probabilistic neutrality bits (PNBs). We introduce the \textit{syncopation} technique for the PNB-based approximation in the backward direction, which significantly amplifies its correlation by utilizing the property of ARX structure. In virtue of this technique, we present a new and efficient...
Automated Analysis of Halo2 Circuits
Fatemeh Heidari Soureshjani, Mathias Hall-Andersen, MohammadMahdi Jahanara, Jeffrey Kam, Jan Gorzny, Mohsen Ahmadvand
Applications
Zero-knowledge proof systems are becoming increasingly prevalent and being widely used to secure decentralized financial systems and protect the privacy of users. Given the sensitivity of these applications, zero-knowledge proof systems are a natural target for formal verification methods. We describe methods for checking one such proof system: Halo2. We use abstract interpretation and an SMT solver to check various properties of Halo2 circuits. Using abstract interpretation, we can detect...
Arithmetic Sketching
Dan Boneh, Elette Boyle, Henry Corrigan-Gibbs, Niv Gilboa, Yuval Ishai
Cryptographic protocols
This paper introduces arithmetic sketching, an abstraction of a primitive that several previous works use to achieve lightweight, low-communication zero-knowledge verification of secret-shared vectors. An arithmetic sketching scheme for a language $\mathcal{L} \in \mathbb{F}^n$ consists of (1) a randomized linear function compressing a long input x to a short “sketch,” and (2) a small arithmetic circuit that accepts the sketch if and only if $x \in \mathcal{L}$, up to some small error. If...
VSS from Distributed ZK Proofs and Applications
Shahla Atapoor, Karim Baghery, Daniele Cozzo, Robi Pedersen
Foundations
Non-Interactive Verifiable Secret Sharing (NI-VSS) is a technique for distributing a secret among a group of individuals in a verifiable manner, such that shareholders can verify the validity of their received share and only a specific number of them can access the secret. VSS is a fundamental tool in cryptography and distributed computing. In this paper, we present an extremely efficient NI-VSS scheme using Zero-Knowledge (ZK) proofs on secret shared data. While prior VSS schemes have...
To Pass or Not to Pass: Privacy-Preserving Physical Access Control
Jesús García-Rodríguez, Stephan Krenn, Daniel Slamanig
Cryptographic protocols
Anonymous or attribute-based credential (ABC) systems are a versatile and important cryptographic tool to achieve strong access control guarantees while simultaneously respecting the privacy of individuals. A major problem in the practical adoption of ABCs is their transferability, i.e., such credentials can easily be duplicated, shared or lent. One way to counter this problem is to tie ABCs to biometric features of the credential holder and to require biometric verification on every use....
How to Bind Anonymous Credentials to Humans
Julia Hesse, Nitin Singh, Alessandro Sorniotti
Applications
Digital and paper-based authentication are the two predominant mechanisms that have been deployed in the real world to authenticate end-users. When verification of a digital credential is performed in person (e.g. the authentication that was often required to access facilities at the peak of the COVID global pandemic), the two mechanisms are often deployed together: the verifier checks government-issued ID to match the picture on the ID to the individual holding it, and then checks the...
Unifying Freedom and Separation for Tight Probing-Secure Composition
Sonia Belaïd, Gaëtan Cassiers, Matthieu Rivain, Abdul Rahman Taleb
The masking countermeasure is often analyzed in the probing model. Proving the probing security of large circuits at high masking orders is achieved by composing gadgets that satisfy security definitions such as non-interference (NI), strong non-interference (SNI) or free SNI. The region probing model is a variant of the probing model, where the probing capabilities of the adversary scale with the number of regions in a masked circuit. This model is of interest as it allows better reductions...
Automated Generation of Masked Nonlinear Components: From Lookup Tables to Private Circuits
Lixuan Wu, Yanhong Fan, Bart Preneel, Weijia Wang, Meiqin Wang
Implementation
Masking is considered to be an essential defense mechanism against side-channel attacks, but it is challenging to be adopted for hardware cryptographic implementations, especially for high security orders. Recently, Knichel et al. proposed an automated tool called AGEMA that enables the generation of masked implementations in hardware for arbitrary security orders using composable gadgets. This accelerates the construction and practical application of masking schemes. This article proposes a...
Password-Based Credentials with Security against Server Compromise
Dennis Dayanikli, Anja Lehmann
Cryptographic protocols
Password-based credentials (PBCs), introduced by Zhang et al. (NDSS'20), provide an elegant solution to secure, yet convenient user authentication. Therein the user establishes a strong cryptographic access credential with the server. To avoid the assumption of secure storage on the user side, the user does not store the credential directly, but only a password-protected version of it. The ingenuity of PBCs is that the password-based credential cannot be offline attacked, offering...
Schnorr protocol in Jasmin
José Bacelar Almeida, Denis Firsov, Tiago Oliveira, Dominique Unruh
Implementation
We implement the Schnorr protocol in assembler via the Jasmin toolchain, and prove the security (proof-of-knowledge and zero-knowledge properties) and the absence of leakage through timing side-channels of that implementation in EasyCrypt.
In order to do so, we provide a semantic characterization of leakage-freeness for probabilistic Jasmin programs (that are not constant-time). We design a library for multiple-precision integer arithmetic in Jasmin -- the "libjbn'' library. Among others,...
Secure Context Switching of Masked Software Implementations
Barbara Gigerl, Robert Primas, Stefan Mangard
Implementation
Cryptographic software running on embedded devices requires protection against physical side-channel attacks such as power analysis. Masking is a widely deployed countermeasure against these attacksand is directly implemented on algorithmic level. Many works study the security of masked cryptographic software on CPUs, pointing out potential problems on algorithmic/microarchitecture-level, as well as corresponding solutions, and even show masked software can be implemented efficiently and...
Ou: Automating the Parallelization of Zero-Knowledge Protocols
Yuyang Sang, Ning Luo, Samuel Judson, Ben Chaimberg, Timos Antonopoulos, Xiao Wang, Ruzica Piskac, Zhong Shao
Implementation
A zero-knowledge proof (ZKP) is a powerful cryptographic primitive used in many decentralized or privacy-focused applications. However, the high overhead of ZKPs can restrict their practical applicability. We design a programming language, Ou, aimed at easing the programmer's burden when writing efficient ZKPs, and a compiler framework, Lian, that automates the analysis and distribution of statements to a computing cluster. Lian uses programming language semantics, formal methods, and...
Certifying Zero-Knowledge Circuits with Refinement Types
Junrui Liu, Ian Kretz, Hanzhi Liu, Bryan Tan, Jonathan Wang, Yi Sun, Luke Pearson, Anders Miltner, Işıl Dillig, Yu Feng
Implementation
Zero-knowledge (ZK) proof systems have emerged as a promising solution for building security-sensitive applications. However, bugs in ZK applications are extremely difficult to detect and can allow a malicious party to silently exploit the system without leaving any observable trace. This paper presents Coda, a novel statically-typed language for building zero-knowledge applications. Critically, Coda makes it possible to formally specify and statically check properties of a ZK application...
Owl: Compositional Verification of Security Protocols via an Information-Flow Type System
Joshua Gancher, Sydney Gibson, Pratap Singh, Samvid Dharanikota, Bryan Parno
Cryptographic protocols
Computationally sound protocol verification tools promise to deliver full-strength cryptographic proofs for security protocols. Unfortunately, current tools lack either modularity or automation.
We propose a new approach based on a novel use of information flow and refinement types for sound cryptographic proofs. Our framework, Owl, allows type-based modular descriptions of security protocols, wherein disjoint subprotocols can be programmed and automatically proved secure separately....
QuantumCharge: Post-Quantum Cryptography for Electric Vehicle Charging
Dustin Kern, Christoph Krauß, Timm Lauser, Nouri Alnahawi, Alexander Wiesmaier, Ruben Niederhagen
Applications
ISO 15118 enables charging and billing of Electric Vehicles
(EVs) without user interaction by using locally installed cryptographic credentials that must be secure over the long lifetime of vehicles. In the dawn of quantum computers, Post-Quantum Cryptography (PQC) needs to be integrated into the EV charging infrastructure. In this paper, we propose QuantumCharge, a PQC extension for ISO 15118, which includes concepts for migration, crypto-agility, verifiable security, and the use of...
A Note on Hybrid Signature Schemes
Nina Bindel, Britta Hale
Public-key cryptography
This draft presents work-in-progress concerning hybrid/composite signature schemes. More concretely, we give several tailored combinations of Fiat-Shamir based signature schemes (such as Dilithium) or Falcon with RSA or DSA. We observe that there are a number of signature hybridization goals, few of which are not achieved through parallel signing or concatenation approaches. These include proof composability (that the post-quantum hybrid signature security can easily be linked to the...
Interactive Oracle Arguments in the QROM and Applications to Succinct Verification of Quantum Computation
Islam Faisal
Cryptographic protocols
This work is motivated by the following question: can an untrusted quantum server convince a classical verifier of the answer to an efficient quantum computation using only polylogarithmic communication? We show how to achieve this in the quantum random oracle model (QROM), after a non-succinct instance-independent setup phase.
We introduce and formalize the notion of post-quantum interactive oracle arguments for languages in QMA, a generalization of interactive oracle proofs...
Machine-Checked Security for $\mathrm{XMSS}$ as in RFC 8391 and $\mathrm{SPHINCS}^{+}$
Manuel Barbosa, François Dupressoir, Benjamin Grégoire, Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub
Public-key cryptography
This work presents a novel machine-checked tight security
proof for $\mathrm{XMSS}$ — a stateful hash-based signature scheme that is (1) standardized in RFC 8391 and NIST SP 800-208, and (2) employed as a primary building block of $\mathrm{SPHINCS}^{+}$, one of the signature schemes recently selected for standardization as a result of NIST’s post-quantum competition.
In 2020, Kudinov, Kiktenko, and Fedoro pointed out a flaw affecting the tight security proofs of $\mathrm{SPHINCS}^{+}$ and...
Programmable Payment Channels
Yibin Yang, Mohsen Minaei, Srinivasan Raghuraman, Ranjit Kumaresan, Duc V. Le, Mahdi Zamani
Applications
One approach for scaling blockchains is to create bilateral, offchain channels, known as payment/state channels, that can protect parties against cheating via onchain collateralization. While such channels have been studied extensively, not much attention has been given to programmability, where the parties can agree to dynamically enforce arbitrary conditions over their payments without going onchain.
We introduce the notion of a programmable payment channel ($\mathsf{PPC}$) that allows...
Towards A Correct-by-Construction FHE Model
Zhenkun Yang, Wen Wang, Jeremy Casas, Pasquale Cocchini, Jin Yang
Implementation
This paper presents a correct-by-construction method of designing an FHE model based on the automated program verifier Dafny. We model FHE operations from the ground up, including fundamentals like GCD, coprimality, Montgomery multiplications, and polynomial operations, etc., and higher level optimizations such as Residue Number System (RNS) and Number Theoretic Transform (NTT). The fully formally verified FHE model serves as a reference design for both software stack development and...
Obfuscation of Pseudo-Deterministic Quantum Circuits
James Bartusek, Fuyuki Kitagawa, Ryo Nishimaki, Takashi Yamakawa
Foundations
We show how to obfuscate pseudo-deterministic quantum circuits in the classical oracle model, assuming the quantum hardness of learning with errors. Given the classical description of a quantum circuit $Q$, our obfuscator outputs a quantum state $\ket{\widetilde{Q}}$ that can be used to evaluate $Q$ repeatedly on arbitrary inputs.
Instantiating the classical oracle using any candidate post-quantum indistinguishability obfuscator gives us the first candidate construction of...
Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium
Manuel Barbosa, Gilles Barthe, Christian Doczkal, Jelle Don, Serge Fehr, Benjamin Grégoire, Yu-Hsuan Huang, Andreas Hülsing, Yi Lee, Xiaodi Wu
Public-key cryptography
We extend and consolidate the security justification for the Dilithium signature scheme. In particular, we identify a subtle but crucial gap that appears in several ROM and QROM security proofs for signature schemes that are based on the Fiat-Shamir with aborts paradigm, including Dilithium. The gap lies in the CMA-to-NMA reduction and was uncovered when trying to formalize a variant of the QROM security proof by Kiltz, Lyubashevsky, and Schaffner (Eurocrypt 2018). The gap was confirmed by...
Formally verifying Kyber Episode IV: Implementation Correctness
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Antoine Séré, Pierre-Yves Strub
Implementation
In this paper we present the first formally verified implementations of Kyber and, to the best of our knowledge, the first such implementations of any post-quantum cryptosystem. We give a (readable) formal specification of Kyber in the EasyCrypt proof assistant, which is syntactically very close to the pseudocode description of the scheme as given in the most recent version of the NIST submission. We present high-assurance open-source implementations of Kyber written in the Jasmin language,...
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography
Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Catalin Hritcu, Bas Spitters
Implementation
The field of high-assurance cryptography is quickly maturing, yet a unified foundational framework for end-to-end formal verification of efficient cryptographic implementations is still missing. To address this gap, we use the Coq proof assistant to formally connect three existing tools: (1) the Hacspec emergent cryptographic specification language; (2) the Jasmin language for efficient, high-assurance cryptographic implementations; and (3) the SSProve foundational verification framework for...
Verification of Correctness and Security Properties for CRYSTALS-KYBER
Katharina Kreuzer
Public-key cryptography
Since the post-quantum crypto system CRYSTALS-KYBER has been chosen for standardization by the National Institute for Standards and Technology (US), a formal verification of its correctness and security properties becomes even more relevant.
Using the automated theorem prover Isabelle, we are able to formalize the algorithm specifications and parameter sets of Kyber's public key encryption scheme and verify the $\delta$-correctness and indistinguishability under chosen plaintext attack...
Specialized Proof of Confidential Knowledge (SPoCK)
Tarak Ben Youssef, Riad S. Wahby
Cryptographic protocols
Flow is a high-throughput blockchain with a dedicated step for executing the transactions in a block and a subsequent verification step performed by Verification Nodes. To enforce integrity of the blockchain, the protocol requires a component that prevents Verification Nodes from approving execution results without checking. In our preceding work, we have sketched out an approach called Specialized Proof of Confidential Knowledge (SPoCK). Using SPoCK, nodes can provide evidence to a third...
DY Fuzzing: Formal Dolev-Yao Models Meet Cryptographic Protocol Fuzz Testing
Max Ammann, Lucca Hirschi, Steve Kremer
Cryptographic protocols
Critical and widely used cryptographic protocols have repeatedly been found to contain flaws in their design and their implementation. A prominent class of such vulnerabilities is logical attacks, e.g. attacks that exploit flawed protocol logic. Automated formal verification methods, based on the Dolev-Yao (DY) attacker, formally define and excel at finding such flaws, but operate only on abstract specification models. Fully automated verification of existing protocol implementations is...
On the Incoercibility of Digital Signatures
Ashley Fraser, Lydia Garms, Elizabeth A. Quaglia
Foundations
We introduce incoercible digital signature schemes, a variant of a standard digital signature. Incoercible signatures enable signers, when coerced to produce a signature for a message chosen by an attacker, to generate fake signatures that are indistinguishable from real signatures, even if the signer is compelled to reveal their full history (including their secret signing keys and any randomness used to produce keys/signatures) to the attacker. Additionally, we introduce an authenticator...
Complete Knowledge: Preventing Encumbrance of Cryptographic Secrets
Mahimna Kelkar, Kushal Babel, Philip Daian, James Austgen, Vitalik Buterin, Ari Juels
Most cryptographic protocols model a player’s knowledge of secrets in a simple way. Informally, the player knows a secret in the sense that she can directly furnish it as a (private) input to a protocol, e.g., to digitally sign a message.
The growing availability of Trusted Execution Environments (TEEs) and secure multiparty computation, however, undermines this model of knowledge. Such tools can encumber a secret sk and permit a chosen player to access sk conditionally, without actually...
PROLEAD_SW - Probing-Based Software Leakage Detection for ARM Binaries
Jannik Zeitschner, Nicolai Müller, Amir Moradi
Applications
A decisive contribution to the all-embracing protection of cryptographic software, especially on embedded devices, is the protection against SCA attacks. Masking countermeasures can usually be integrated into the software during the design phase. In theory, this should provide reliable protection against such physical attacks. However, the correct application of masking is a non-trivial task that often causes even experts to make mistakes. In addition to human-caused errors,...
Verification of the (1–δ)-Correctness Proof of CRYSTALS-KYBER with Number Theoretic Transform
Katharina Kreuzer
Public-key cryptography
This paper describes a formalization of the specification and the algorithm of the cryptographic scheme CRYSTALS-KYBER as well as the verification of its (1 − δ)-correctness proof. During the formalization, a problem in the correctness proof was uncovered. In order to amend this
issue, a necessary property on the modulus parameter of the CRYSTALS-KYBER algorithm was introduced. This property is already implicitly fulfilled by the structure of the modulus prime used in the number theoretic...
Verifying Classic McEliece: examining the role of formal methods in post-quantum cryptography standardisation
Martin Brain, Carlos Cid, Rachel Player, Wrenna Robson
Implementation
Developers of computer-aided cryptographic tools are optimistic that formal methods will become a vital part of developing new cryptographic systems. We study the use of such tools to specify and verify the implementation of Classic McEliece, one of the code-based cryptography candidates in the fourth round of the NIST Post-Quantum standardisation Process. From our case study we draw conclusions about the practical applicability of these methods to the development of novel cryptography.
Secure Single-Server Fuzzy Deduplication without Interactive Proof-of-Ownership in Cloud
Shuai Cheng, Shengke Zeng, Haoyu Zeng, Yawen Feng, Jixiang Xiao
The redundant of multimedia data made an unnecessary waste in encrypted cloud storage, unlike text with completely consistent content, multimedia data allows a certain degree of similarity in deduplication, In this work, we focus on the multimedia data which takes a seriously proportion of storage in scenarios such as data outsourcing to propose secure fuzzy deduplication without the additional servers based on Convergent Encryption(CE), say the Single-server Fuzzy Deduplication (SSFD)....
PoRt: Non-Interactive Continuous Availability Proof of Replicated Storage
Reyhaneh Rabaninejad, Bin Liu, Antonis Michalas
Cryptographic protocols
Secure cryptographic storage is one of the most important issues
that both businesses and end-users take into account before moving
their data to either centralized clouds or blockchain-based decen-
tralized storage marketplace. Recent work [4 ] formalizes the notion
of Proof of Storage-Time (PoSt) which enables storage servers to
demonstrate non-interactive continuous availability of outsourced
data in a publicly verifiable way. The work also proposes a stateful
compact PoSt...
Ring Signatures with User-Controlled Linkability
Dario Fiore, Lydia Garms, Dimitris Kolonelos, Claudio Soriente, Ida Tucker
Public-key cryptography
Anonymous authentication primitives, e.g., group or ring signatures, allow one to realize privacy-preserving data collection applications, as they strike a balance between authenticity of data being collected and privacy of data providers. At PKC 2021, Diaz and Lehmann defined group signatures with User-Controlled Linkability (UCL) and provided an instantiation based on BBS+ signatures. In a nutshell, a signer of a UCL group signature scheme can link any of her signatures: linking evidence...
Formal Analysis of Session-Handling in Secure Messaging: Lifting Security from Sessions to Conversations
Cas Cremers, Charlie Jacomme, Aurora Naska
Cryptographic protocols
The building blocks for secure messaging apps, such as Signal’s X3DH and Double Ratchet (DR) protocols, have received a lot of attention from the research community. They have notably been proved to meet strong security properties even in the case of compromise such as Forward Secrecy (FS) and Post-Compromise Security (PCS). However, there is a lack of formal study of these properties at the application level. Whereas the research works have studied such properties in the context of a single...
Careful with MAc-then-SIGn: A Computational Analysis of the EDHOC Lightweight Authenticated Key Exchange Protocol
Felix Günther, Marc Ilunga Tshibumbu Mukendi
Cryptographic protocols
EDHOC is a lightweight authenticated key exchange protocol for IoT communication, currently being standardized by the IETF. Its design is a trimmed-down version of similar protocols like TLS 1.3, building on the SIGn-then-MAc (SIGMA) rationale. In its trimming, however, EDHOC notably deviates from the SIGMA design by sending only short, non-unique credential identifiers, and letting recipients perform trial verification to determine the correct communication partner. Done naively, this can...
Another Round of Breaking and Making Quantum Money: How to Not Build It from Lattices, and More
Jiahui Liu, Hart Montgomery, Mark Zhandry
Foundations
Public verification of quantum money has been one of the central objects in quantum cryptography ever since Wiesner's pioneering idea of using quantum mechanics to construct banknotes against counterfeiting. So far, we do not know any publicly-verifiable quantum money scheme that is provably secure from standard assumptions.
In this work, we provide both negative and positive results for publicly verifiable quantum money.
**In the first part, we give a general theorem, showing that a...
Ligero: Lightweight Sublinear Arguments Without a Trusted Setup
Scott Ames, Carmit Hazay, Yuval Ishai, Muthuramakrishnan Venkitasubramaniam
Cryptographic protocols
We design and implement a simple zero-knowledge argument protocol for $\mathsf{NP}$ whose communication complexity is proportional to the square-root of the verification circuit size. The protocol can be based on any collision-resistant hash function. Alternatively, it can be made non-interactive in the random oracle model, yielding concretely efficient zk-SNARKs that do not require a trusted setup or public-key cryptography. Our protocol is obtained by applying an optimized version of the...
Universal Ring Signatures in the Standard Model
Pedro Branco, Nico Döttling, Stella Wohnig
Cryptographic protocols
Ring signatures allow a user to sign messages on behalf of an ad hoc set of users - a ring - while hiding her identity. The original motivation for ring signatures was whistleblowing [Rivest et al. ASIACRYPT'01]: a high government employee can anonymously leak sensitive information while certifying that it comes from a reliable source, namely by signing the leak. However, essentially all known ring signature schemes require the members of the ring to publish a structured verification key...
Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co
Constantin Cătălin Drăgan, François Dupressoir, Ehsan Estaji, Kristian Gjøsteen, Thomas Haines, Peter Y. A. Ryan, Peter B. Rønne, Morten Rotvold Solberg
Cryptographic protocols
Privacy is a notoriously difficult property to achieve in complicated systems and especially in electronic voting schemes. Moreover, electronic voting schemes is a class of systems that require very high assurance. The literature contains a number of ballot privacy definitions along with security proofs for common systems. Some machine-checked security proofs have also appeared. We define a new ballot privacy notion that captures a larger class of voting schemes. This notion improves on the...
Automatic Certified Verification of Cryptographic Programs with COQCRYPTOLINE
Ming-Hsien Tsai, Yu-Fu Fu, Xiaomu Shi, Jiaxiang Liu, Bow-Yaw Wang, Bo-Yin Yang
Implementation
COQCRYPTOLINE is an automatic certified verification tool for cryptographic programs. It is built on OCAML programs extracted from algorithms fully certified in COQ with SS- REFLECT. Similar to other automatic tools, COQCRYPTO- LINE calls external decision procedures during verification. To ensure correctness, all answers from external decision procedures are validated by certified certificate checkers in COQCRYPTOLINE. We evaluate COQCRYPTOLINE on cryp- tographic programs from BITCOIN,...
A tale of two models: formal verification of KEMTLS via Tamarin
Sofía Celi, Jonathan Hoyland, Douglas Stebila, Thom Wiggers
Public-key cryptography
KEMTLS is a proposal for changing the TLS handshake to authenticate the handshake using long-term key encapsulation mechanism keys instead of signatures, motivated by trade-offs in the characteristics of post-quantum algorithms. Prior proofs of security of KEMTLS and its variant KEMTLS-PDK have been hand-written proofs in the reductionist model under computational assumptions. In this paper, we present computer-verified symbolic analyses of KEMTLS and KEMTLS-PDK using two distinct Tamarin...
FIDO2, CTAP 2.1, and WebAuthn 2: Provable Security and Post-Quantum Instantiation
Nina Bindel, Cas Cremers, Mang Zhao
Cryptographic protocols
The FIDO2 protocol is a globally used standard for passwordless authentication, building on an alliance between major players in the online authentication space. While already widely deployed, the standard is still under active development. Since version 2.1 of its CTAP sub-protocol, FIDO2 can potentially be instantiated with post-quantum secure primitives.
We provide the first formal security analysis of FIDO2 with the CTAP 2.1 and WebAuthn 2 sub-protocols. Our security models build on...
PROLEAD - A Probing-Based Hardware Leakage Detection Tool
Nicolai Müller, Amir Moradi
Applications
Even today, SCA attacks pose a serious threat to the security of cryptographic implementations fabricated with low-power and nano-scale feature technologies. Fortunately, the masking countermeasures offer reliable protection against such attacks based on simple security assumptions. However, the practical application of masking to a cryptographic algorithm is not trivial, and the designer may overlook possible security flaws, especially when masking a complex circuit. Moreover, abstract...
Succinct Classical Verification of Quantum Computation
James Bartusek, Yael Tauman Kalai, Alex Lombardi, Fermi Ma, Giulio Malavolta, Vinod Vaikuntanathan, Thomas Vidick, Lisa Yang
Foundations
We construct a classically verifiable succinct interactive argument for quantum computation (BQP) with communication complexity and verifier runtime that are poly-logarithmic in the runtime of the BQP computation (and polynomial in the security parameter). Our protocol is secure assuming the post-quantum security of indistinguishability obfuscation (iO) and Learning with Errors (LWE). This is the first succinct argument for quantum computation in the plain model; prior work...
Formal Verification of Arithmetic Masking in Hardware and Software
Barbara Gigerl, Robert Primas, Stefan Mangard
Applications
Masking is a popular secret-sharing technique that is used to protect cryptographic implementations against physical attacks like differential power analysis. So far, most research in this direction has focused on finding efficient Boolean masking schemes for well-known symmetric cryptographic algorithms like AES and Keccak. However, especially with the advent of post-quantum cryptography (PQC), arithmetic masking has received increasing attention from the research community. In practice,...
Privacy Preserving Opinion Aggregation
Aggelos Kiayias, Vanessa Teague, Orfeas Stefanos Thyfronitis Litos
Cryptographic protocols
There are numerous settings in which people's preferences are aggregated outside of formal elections, and where privacy and verification are important but the stringent authentication and coercion-resistant properties of government elections do not apply, a prime example being social media platforms. These systems are often iterative and have no trusted authority, in contrast to the centrally organised, single-shot elections on which most of the literature is focused. Moreover, they require...
Sapic+: protocol verifiers of the world, unite!
Vincent Cheval, Charlie Jacomme, Steve Kremer, Robert Künnemann
Cryptographic protocols
Symbolic security protocol verifiers have reached a high degree of automation and maturity. Today, experts can model real-world protocols, but this often requires model-specific encodings and deep insight into the strengths and weaknesses of each of those tools. With Sapic+ , we introduce a protocol verification platform that lifts this burden and permits choosing the right tool for the job, at any development stage. We build on the existing compiler from Sapic to Tamarin, and extend it with...
Contingent payments from two-party signing and verification for abelian groups
Sergiu Bursuc, Sjouke Mauw
Cryptographic protocols
The fair exchange problem has faced for a long time the bottleneck of a required trusted third party. The recent development of blockchains introduces a new type of party to this problem, whose trustworthiness relies on a public ledger and distributed computation. The challenge in this setting is to reconcile the minimalistic and public nature of blockchains with elaborate fair exchange requirements, from functionality to privacy. Zero-knowledge contingent payments (ZKCP) are a class of...
CENSOR: Privacy-preserving Obfuscation for Outsourcing SAT formulas
Tassos Dimitriou, Khazam Alhamdan
Applications
We propose a novel obfuscation technique that can be used to outsource hard satisfiability (SAT) formulas to the cloud. Servers with large computational power are typically used to solve SAT instances that model real-life problems in task scheduling, AI planning, circuit verification and more. However, outsourcing data to the cloud may lead to privacy and information breaches since satisfying assignments may reveal considerable information about the underlying problem modeled by SAT.
In...
Enforcing fine-grained constant-time policies
Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya
Cryptographic constant-time (CT) is a popular programming disci- pline used by cryptographic libraries to protect themselves against timing attacks. The CT discipline aims to enforce that program ex- ecution does not leak secrets, where leakage is defined by a formal leakage model. In practice, different leakage models coexist, some- times even within a single library, both to reflect different architec- tures and to accommodate different security-efficiency trade-offs. Constant-timeness is...
Breaking the $t< n/3$ Consensus Bound: Asynchronous Dynamic Proactive Secret Sharing under Honest Majority
Christophe Levrat, Matthieu Rambaud, Antoine Urban
Cryptographic protocols
A proactive secret sharing scheme (PSS), expressed in the dynamic-membership setting, enables a committee of n holders of secret-shares, dubbed as players, to securely hand-over new shares of the same secret to a new committee. We dub such a sub-protocol as a Refresh. All existing PSS under an honest majority, require the use of a broadcast (BC) in each refresh. BC is costly to implement, and its security relies on timing assumptions on the network. So the privacy of the secret and/or its...
Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations (Long Version)
Son Ho, Jonathan Protzenko, Abhishek Bichhawat, Karthikeyan Bhargavan
Implementation
The Noise protocol framework defines a succinct notation and execution
framework for a large class of 59+ secure channel protocols, some of
which are used in popular applications such as WhatsApp and WireGuard.
We present a verified implementation of a Noise
protocol compiler that takes any Noise protocol, and produces
an optimized C implementation with extensive correctness and security
guarantees. To this end, we formalize the complete Noise stack in
F*, from the low-level cryptographic...
Power Contracts: Provably Complete Power Leakage Models for Processors
Roderick Bloem, Barbara Gigerl, Marc Gourjon, Vedad Hadžić, Stefan Mangard, Robert Primas
Foundations
The protection of cryptographic software implementations against power-analysis attacks is critical for applications in embedded systems.
A commonly used algorithmic countermeasure against these attacks is masking, a secret-sharing scheme that splits a sensitive computation into computations on multiple random shares.
In practice, the security of masking schemes relies on several assumptions that are often violated by microarchitectural side-effects of CPUs.
Many past works address this...
Riding the Waves Towards Generic Single-Cycle Masking in Hardware
Rishub Nagpal, Barbara Gigerl, Robert Primas, Stefan Mangard
Implementation
Research on the design of masked cryptographic hardware circuits in the
past has mostly focused on reducing area and randomness requirements. However,
many embedded devices like smart cards and IoT nodes also need to meet certain
performance criteria, which is why the latency of masked hardware circuits also
represents an important metric for many practical applications.
The root cause of latency in masked hardware circuits is the need for additional register stages that synchronize the...
VERICA - Verification of Combined Attacks: Automated formal verification of security against simultaneous information leakage and tampering
Jan Richter-Brockmann, Jakob Feldtkeller, Pascal Sasdrich, Tim Güneysu
Applications
Physical attacks, including passive Side-Channel Analysis and active Fault Injection Analysis, are considered among the most powerful threats against physical cryptographic implementations. These attacks are well known and research provides many specialized countermeasures to protect cryptographic implementations against them. Still, only a limited number of combined countermeasures, i.e., countermeasures that protect implementations against multiple attacks simultaneously, were proposed in...
Armistice: Micro-Architectural Leakage Modelling for Masked Software Formal Verification
Arnaud de Grandmaison, Karine Heydemann, Quentin L. Meunier
Implementation
Side channel attacks are powerful attacks for retrieving secret data by exploiting physical measurements such as power consumption or electromagnetic emissions. Masking is a popular countermeasure as it can be proven secure against an attacker model. In practice, software masked implementations suffer from a security reduction due to a mismatch between the considered leakage sources in the security proof and the real ones, which depend on the micro-architecture.
We present the model of a...
Formal Verification of Saber's Public-Key Encryption Scheme in EasyCrypt
Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub
Public-key cryptography
In this work, we consider the formal verification of the public-key encryption scheme of Saber, one of the selected few post-quantum cipher suites currently considered for potential standardization. We formally verify this public-key encryption scheme's IND-CPA security and $\delta$-correctness properties, i.e., the properties required to transform the public-key encryption scheme into an IND-CCA2 secure and $\delta$-correct key encapsulation mechanism, in EasyCrypt. To this end, we...
Composable Dynamic Secure Emulation
Pierre Civit, Maria Potop-Butucaru
Foundations
This work extends the composable secure-emulation of Canetti et al. to dynamic settings. Our work builds on top of dynamic probabilistic I/O automata, a recent framework introduced to model dynamic probabilistic systems. Our extension is an important tool towards the formal verification of protocols combining probabilistic distributed systems and cryptography in dynamic settings (e.g. blockchains, secure distributed computation, cybersecure distributed protocols etc).
Handcrafting: Improving Automated Masking in Hardware with Manual Optimizations
Charles Momin, Gaëtan Cassiers, François-Xavier Standaert
Implementation
Masking is an important countermeasure against side-channel attacks, but its secure implementation is known to be error-prone. The automated verification and generation of masked designs is therefore an important theoretical and practical challenge. In a recent work, Knichel et al. proposed a tool for the automated generation of masked hardware implementations satisfying strong security properties (e.g., glitch-freeness and composability). In this paper, we study the possibility to improve...
Proving UNSAT in Zero Knowledge
Ning Luo, Timos Antonopoulos, William Harris, Ruzica Piskac, Eran Tromer, Xiao Wang
Cryptographic protocols
Zero-knowledge (ZK) protocols enable one party to prove to others that it knows a fact without revealing any information about the evidence for such knowledge. There exist ZK protocols for all problems in NP, and recent works developed highly efficient protocols for proving knowledge of satisfying assignments to Boolean formulas, circuits and other NP formalisms. This work shows an efficient protocol for the the converse: proving formula *unsatisfiability* in ZK (when the prover posses a...
GMHL: Generalized Multi-Hop Locks for Privacy-Preserving Payment Channel Networks
Zilin Liu, Anjia Yang, Jian Weng, Tao Li, Huang Zeng, Xiaojian Liang
Payment channel network (PCN), not only improving the transaction throughput of blockchain but also realizing cross-chain payment, is a very promising solution to blockchain scalability problem. Most existing PCN constructions focus on either atomicity or privacy properties. Moreover, they are built on specific scripting features of the underlying blockchain such as HTLC or are tailored to several signature algorithms like ECDSA and Schnorr. In this work, we devise a Generalized Multi-Hop...
Transitional Leakage in Theory and Practice - Unveiling Security Flaws in Masked Circuits
Nicolai Müller, David Knichel, Pascal Sasdrich, Amir Moradi
Applications
Accelerated by the increased interconnection of highly accessible devices, the demand for effective and efficient protection of hardware designs against SCA is ever rising, causing its topical relevance to remain immense in both, academia and industry. Among a wide range of proposed countermeasures against SCA, masking is a highly promising candidate due to its sound foundations and well-understood security requirements. In addition, formal adversary models have been introduced, aiming to...
Beating Classical Impossibility of Position Verification
Jiahui Liu, Qipeng Liu, Luowen Qian
Cryptographic protocols
Chandran et al. (SIAM J. Comput.'14) formally introduced the cryptographic task of position verification, where they also showed that it cannot be achieved by classical protocols. In this work, we initiate the study of position verification protocols with classical verifiers. We identify that proofs of quantumness (and thus computational assumptions) are necessary for such position verification protocols. For the other direction, we adapt the proof of quantumness protocol by Brakerski et al....
SecNDP: Secure Near-Data Processing with Untrusted Memory
Wenjie Xiong, Liu Ke, Dimitrije Jankov, Michael Kounavis, Xiaochen Wang, Eric Northup, Jie Amy Yang, Bilge Acun, Carole-Jean Wu, Ping Tak Peter Tang, G. Edward Suh, Xuan Zhang, Hsien-Hsin S. Lee.
Secret-key cryptography
Today's data-intensive applications increasingly suffer from significant performance bottlenecks due to the limited memory bandwidth of the classical von Neumann architecture. Near-Data Processing (NDP) has been proposed to perform computation near memory or data storage to reduce data movement for improving performance and energy consumption. However, the untrusted NDP processing units (PUs) bring in new threats to workloads that are private and sensitive, such as private database queries...
Information Dispersal with Provable Retrievability for Rollups
Kamilla Nazirkhanova, Joachim Neu, David Tse
Cryptographic protocols
The ability to verifiably retrieve transaction or state data stored off-chain is crucial to blockchain scaling techniques such as rollups or sharding. We formalize the problem and design a storage- and communication-efficient protocol using linear erasure-correcting codes and homomorphic vector commitments. Motivated by application requirements for rollups, our solution Semi-AVID-PR departs from earlier Verifiable Information Dispersal schemes in that we do not require comprehensive...
Security evaluation against side-channel analysis at compilation time
Nicolas Bruneau, Charles Christen, Jean-Luc Danger, Adrien Facon, Sylvain Guilley
Implementation
Masking countermeasure is implemented to thwart side-channel attacks.
The maturity of high-order masking schemes has reached the level where the concepts are sound and proven.
For instance, Rivain and Prouff proposed a full-fledged AES at CHES 2010.
Some non-trivial fixes regarding refresh functions were needed though.
Now, industry is adopting such solutions, and for the sake of both quality and certification requirements,
masked cryptographic code shall be checked for correctness using the...
A Cryptographic View of Deep-Attestation, or how to do Provably-Secure Layer-Linking
Ghada Arfaoui, Pierre-Alain Fouque, Thibaut Jacques, Pascal Lafourcade, Adina Nedelcu, Cristina Onete, Léo Robert
Cryptographic protocols
Deep attestation is a particular case of remote attestation, i.e.,
verifying the integrity of a platform with a remote verification
server. We focus on the remote attestation of hypervisors and their
hosted virtual machines (VM), for which two solutions are currently
supported by ETSI. The first is single-channel attestation, requiring
for each VM an attestation of that VM and the underlying hypervisor
through the physical TPM. The second, multi-channel attestation,
allows to attest VMs via...
LeakageVerif: Scalable and Efficient Leakage Verification in Symbolic Expressions
Quentin L. Meunier, Etienne Pons, Karine Heydemann
Implementation
Side-channel attacks are a powerful class of attacks targeting cryptographic devices. Masking is a popular protection technique to thwart such attacks as it can be theoretically proven secure. However, correctly implementing masking schemes is a non-trivial task and error-prone. If several techniques have been proposed to formally verify masked implementations, they all come with limitations regarding expressiveness, scalability or accuracy. In this work, we propose a symbolic approach,...
UC Secure Private Branching Program and Decision Tree Evaluation
Keyu Ji, Bingsheng Zhang, Tianpei Lu, Lichun Li, Kui Ren
Cryptographic protocols
Branching program (BP) is a DAG-based non-uniform computational model for L/poly class. It has been widely used in formal verification, logic synthesis, and data analysis. As a special BP, a decision tree is a popular machine learning classifier for its effectiveness and simplicity. In this work, we propose a UC-secure efficient 3-party computation platform for outsourced branching program and/or decision tree evaluation. We construct a constant-round protocol and a linear-round protocol. In...
Orca: Blocklisting in Sender-Anonymous Messaging
Nirvan Tyagi, Julia Len, Ian Miers, Thomas Ristenpart
Cryptographic protocols
Sender-anonymous end-to-end encrypted messaging allows sending messages to a recipient without revealing the sender’s identity to the messaging platform. Signal recently introduced a sender anonymity feature that includes an abuse mitigation mechanism meant to allow the platform to block malicious senders on behalf of a recipient. We explore the tension between sender anonymity and abuse mitigation. We start by showing limitations of Signal’s deployed mechanism, observing that it results in...
EasyPQC: Verifying Post-Quantum Cryptography
Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grégoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu, Li Zhou
Public-key cryptography
EasyCrypt is a formal verification tool used extensively for formalizing concrete security proofs of cryptographic constructions. However, the EasyCrypt formal logics consider only classical attackers, which means that post-quantum security proofs cannot be formalized and machine-checked with this tool. In this paper we prove that a natural extension of the EasyCrypt core logics permits capturing a wide class of post-quantum cryptography proofs, settling a question raised by (Unruh, POPL...
Provably Improving Election Verifiability in Belenios
Sevdenur Baloglu, Sergiu Bursuc, Sjouke Mauw, Jun Pang
Cryptographic protocols
Belenios is an online voting system that provides a strong notion of election verifiability, where no single party has to be trusted, and security holds as soon as either the voting registrar or the voting server is honest. It was formally proved to be secure, making the assumption that no further ballots are cast on the bulletin board after voters verified their ballots. In practice, however, revoting is allowed and voters can verify their ballots anytime. This gap between formal proofs and...
Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head
José Bacelar Almeida, Manuel Barbosa, Manuel L Correia, Karim Eldefrawy, Stéphane Graham-Lengrand, Hugo Pacheco, Vitor Pereira
Implementation
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 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...
A verifiable random function (VRF) allows one to compute a random-looking image, while at the same time providing a unique proof that the function was evaluated correctly. VRFs are a cornerstone of modern cryptography and, among other applications, are at the heart of recently proposed proof-of-stake consensus protocols. In this work we initiate the formal study of aggregate VRFs, i.e., VRFs that allow for the aggregation of proofs/images into a small di- gest, whose size is independent of...
At EUROCRYPT’23, Castryck and Decru, Maino et al., and Robert present efficient attacks against supersingular isogeny Diffie-Hellman key exchange protocol (SIDH). Drawing inspiration from these attacks, Andrea Basso, Luciano Maino, and Giacomo Pope introduce FESTA, an isogeny-based trapdoor function, along with a corresponding IND-CCA secure public key encryption (PKE) protocol at ASIACRYPT’23. FESTA incorporates either a diagonal or circulant matrix into the secret key to mask torsion...
We show that there is a discrepancy between the emulated floating-point multiplications in the submission package of Falcon and the claimed behavior. In particular, we show that floating-point products with absolute values the smallest normal positive floating-point number are incorrectly zeroized. However, we show that the discrepancy doesn’t effect the complex fast Fourier transform by modeling the floating-point addition, subtraction, and multiplication in CryptoLine. We later implement...
Polynomial commitment scheme allows a prover to commit to a polynomial $f \in \mathcal{R}[X]$ of degree $L$, and later prove that the committed function was correctly evaluated at a specified point $x$; in other words $f(x)=u$ for public $x,u \in\mathcal{R}$. Most applications of polynomial commitments, e.g. succinct non-interactive arguments of knowledge (SNARKs), require that (i) both the commitment and evaluation proof are succinct (i.e., polylogarithmic in the degree $L$) - with the...
Interactive theorem provers (ITPs), such as Lean and Coq, can express formal proofs for a large category of theorems, from abstract math to software correctness. Consider Alice who has a Lean proof for some public statement $T$. Alice wants to convince the world that she has such a proof, without revealing the actual proof. Perhaps the proof shows that a secret program is correct or safe, but the proof itself might leak information about the program's source code. A natural way for...
To assess the robustness of CPU-based systems against fault injection attacks, it is necessary to analyze the consequences of the fault propagation resulting from the intricate interaction between the software and the processor. However, current formal methodologies that combine both hardware and software aspects experience scalability issues, primarily due to the use of bounded verification techniques. This work formalizes the notion of $k$-fault resistant partitioning as an inductive...
Over the past decade, cryptocurrencies have garnered attention from academia and industry alike, fostering a diverse blockchain ecosystem and novel applications. The inception of bridges improved interoperability, enabling asset transfers across different blockchains to capitalize on their unique features. Despite their surge in popularity and the emergence of Decentralized Finance (DeFi), trustless bridge protocols remain inefficient, either relaying too much information (e.g.,...
Adaptor signature is a novel cryptographic primitive which ties together the signature and the leakage of a secret value. It has become an important tool for solving the scalability and interoperability problems in the blockchain. Aumayr et al. (Asiacrypt 2021) recently provide the formalization of the adaptor signature and present a provably secure ECDSA-based adaptor signature, which requires zero-knowledge proof in the pre-signing phase to ensure the signer works correctly. However, the...
Given a fixed-size block, cryptographic block functions gen- erate outputs by a sequence of bitwise operations. Block functions are widely used in the design of hash functions and stream ciphers. Their correct implementations hence are crucial to computer security. We pro- pose a method that leverages logic equivalence checking to verify assem- bly implementations of cryptographic block functions. Logic equivalence checking is a well-established technique from hardware verification....
Driven by the open problem raised by Hofheinz and Kiltz (Journal of Cryptology, 2012), we study the formalization of lattice-based programmable hash function (PHF), and give three types of concrete constructions by using several techniques such as a novel combination of cover-free sets and lattice trapdoors. Under the Inhomogeneous Small Integer Solution (ISIS) assumption, we show that any (non-trivial) lattice-based PHF is a collision-resistant hash function, which gives a direct...
Verification of program safety is often reducible to proving the unsatisfiability (i.e., validity) of a formula in Satisfiability Modulo Theories (SMT): Boolean logic combined with theories that formalize arbitrary first-order fragments. Zero-knowledge (ZK) proofs allow SMT formulas to be validated without revealing the underlying formulas or their proofs to other parties, which is a crucial building block for proving the safety of proprietary programs. Recently, Luo et al. (CCS 2022)...
The Internet Key Exchange version 2 (IKEv2) (RFC 7296) is a component of IPsec used to authenticate two parties (the initiator and responder) to each other and to establish a set of security parameters for the communications. The security parameters include secret keys to encrypt and authenticate data as well as the negotiation of a set of cryptographic algorithms. The core documentation uses exclusively Diffie-Hellman exchanges to agree the security information. However, this is not a...
When outsourcing a database to an untrusted remote server, one might want to verify the integrity of contents while accessing it. To solve this, Blum et al. [FOCS `91] propose the notion of memory checking. Memory checking allows a user to run a RAM program on a remote server, with the ability to verify integrity of the storage with small local storage. In this work, we define and initiate the formal study of memory checking for Parallel RAMs (PRAMs). The parallel RAM...
Motivated by applications in anonymous reputation systems and blockchain governance, we initiate the study of predicate aggregate signatures (PAS), which is a new primitive that enables users to sign multiple messages, and these individual signatures can be aggregated by a combiner, preserving the anonymity of the signers. The resulting PAS discloses only a brief description of signers for each message and provides assurance that both the signers and their description satisfy the specified...
Data formats used for cryptographic inputs have historically been the source of many attacks on cryptographic protocols, but their security guarantees remain poorly studied. One reason is that, due to their low-level nature, formats often fall outside of the security model. Another reason is that studying all of the uses of all of the formats within one protocol is too difficult to do by hand, and requires a comprehensive, automated framework. We propose a new framework, “Comparse”, that...
Physical attacks are well-known threats to cryptographic implementations. While countermeasures against passive Side-Channel Analysis (SCA) and active Fault Injection Analysis (FIA) exist individually, protecting against their combination remains a significant challenge. A recent attempt at achieving joint security has been published at CCS 2022 under the name CINI-MINIS. The authors introduce relevant security notions and aim to construct arbitrary-order gadgets that remain trivially...
While cryptographic protocols are often analyzed in isolation, they are typically deployed within a stack of protocols, where each layer relies on the security guarantees provided by the protocol layer below it, and in turn provides its own security functionality to the layer above. Formally analyzing the whole stack in one go is infeasible even for semi-automated verification tools, and impossible for pen-and-paper proofs. The DY$^\star$ protocol verification framework offers a modular and...
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...
We provide a preliminary report of our ongoing work in formally defining and verifying, in a compositional way, the R1CS gadgets generated by Aleo's snarkVM. The approach is applicable to other systems that generate gadgets in a similar manner, and that may use non-R1CS representations.
We generalize the Bernstein-Yang (BY) algorithm for constant-time modular inversion to compute the Kronecker symbol, of which the Jacobi and Legendre symbols are special cases. We start by developing a basic and easy-to-implement divstep version of the algorithm defined in terms of full-precision division steps. We then describe an optimized version due to Hamburg over word-sized inputs, similar to the jumpdivstep version of the BY algorithm, and formally verify its correctness. Along the...
Digital Covid certificates are the first widely deployed end-user cryptographic certificates. For service providers, such as airlines or event ticket vendors, that needed to check that their (global) customers satisfy certain health policies, the verification of such Covid certificates was challenging though - not because of the cryptography involved, but due to the multitude of issuers, different certificate types and the evolving nature of country-specific policies that had to be...
Physical side-channel attacks exploit a device's emanations to compromise the security of cryptographic implementations. Many countermeasures have been proposed against these attacks, especially the widely-used and efficient masking countermeasure. While theoretical models offer formal security proofs, they often rest on unrealistic assumptions, leading current approaches to prove the security of masked implementations to primarily rely on empirical verification. Consequently, the...
The accelerated advances in information communication technologies have made it possible for enterprises to deploy large scale applications in a multi-server architecture (also known as cloud computing environment). In this architecture, a mobile user can remotely obtain desired services over the Internet from multiple servers by initially executing a single registration on a trusted registration server (RS). Due to the hazardous nature of the Internet, to protect user privacy and online...
Subversion-resistant zk-SNARKs allow the provers to verify the Structured Reference String (SRS), via an SRS Verification (SV) algorithm and bypass the need for a Trusted Third Party (TTP). Pairing-based zk-SNARKs with \(updatable\) and \(universal\) SRS are an extension of subversion-resistant ones which additionally allow the verifiers to update the SRS, via an SRS Updating (SU) algorithm, and similarly bypass the need for a TTP. In this paper, we examine the setup of these zk-SNARKs by...
Private payments in blockchain-based cryptocurrencies have been a topic of research, both academic and industrial, ever since the advent of Bitcoin. Stealth address payments were proposed as a solution to improve payment privacy for users and are, in fact, deployed in several major cryptocurrencies today. The mechanism lets users receive payments so that none of these payments are linkable to each other or the recipient. Currently known stealth address mechanisms either (1) are insecure in...
The stream cipher ChaCha is one of the most widely used ciphers in the real world, such as in TLS, SSH and so on. In this paper, we study the security of ChaCha via differential cryptanalysis based on probabilistic neutrality bits (PNBs). We introduce the \textit{syncopation} technique for the PNB-based approximation in the backward direction, which significantly amplifies its correlation by utilizing the property of ARX structure. In virtue of this technique, we present a new and efficient...
Zero-knowledge proof systems are becoming increasingly prevalent and being widely used to secure decentralized financial systems and protect the privacy of users. Given the sensitivity of these applications, zero-knowledge proof systems are a natural target for formal verification methods. We describe methods for checking one such proof system: Halo2. We use abstract interpretation and an SMT solver to check various properties of Halo2 circuits. Using abstract interpretation, we can detect...
This paper introduces arithmetic sketching, an abstraction of a primitive that several previous works use to achieve lightweight, low-communication zero-knowledge verification of secret-shared vectors. An arithmetic sketching scheme for a language $\mathcal{L} \in \mathbb{F}^n$ consists of (1) a randomized linear function compressing a long input x to a short “sketch,” and (2) a small arithmetic circuit that accepts the sketch if and only if $x \in \mathcal{L}$, up to some small error. If...
Non-Interactive Verifiable Secret Sharing (NI-VSS) is a technique for distributing a secret among a group of individuals in a verifiable manner, such that shareholders can verify the validity of their received share and only a specific number of them can access the secret. VSS is a fundamental tool in cryptography and distributed computing. In this paper, we present an extremely efficient NI-VSS scheme using Zero-Knowledge (ZK) proofs on secret shared data. While prior VSS schemes have...
Anonymous or attribute-based credential (ABC) systems are a versatile and important cryptographic tool to achieve strong access control guarantees while simultaneously respecting the privacy of individuals. A major problem in the practical adoption of ABCs is their transferability, i.e., such credentials can easily be duplicated, shared or lent. One way to counter this problem is to tie ABCs to biometric features of the credential holder and to require biometric verification on every use....
Digital and paper-based authentication are the two predominant mechanisms that have been deployed in the real world to authenticate end-users. When verification of a digital credential is performed in person (e.g. the authentication that was often required to access facilities at the peak of the COVID global pandemic), the two mechanisms are often deployed together: the verifier checks government-issued ID to match the picture on the ID to the individual holding it, and then checks the...
The masking countermeasure is often analyzed in the probing model. Proving the probing security of large circuits at high masking orders is achieved by composing gadgets that satisfy security definitions such as non-interference (NI), strong non-interference (SNI) or free SNI. The region probing model is a variant of the probing model, where the probing capabilities of the adversary scale with the number of regions in a masked circuit. This model is of interest as it allows better reductions...
Masking is considered to be an essential defense mechanism against side-channel attacks, but it is challenging to be adopted for hardware cryptographic implementations, especially for high security orders. Recently, Knichel et al. proposed an automated tool called AGEMA that enables the generation of masked implementations in hardware for arbitrary security orders using composable gadgets. This accelerates the construction and practical application of masking schemes. This article proposes a...
Password-based credentials (PBCs), introduced by Zhang et al. (NDSS'20), provide an elegant solution to secure, yet convenient user authentication. Therein the user establishes a strong cryptographic access credential with the server. To avoid the assumption of secure storage on the user side, the user does not store the credential directly, but only a password-protected version of it. The ingenuity of PBCs is that the password-based credential cannot be offline attacked, offering...
We implement the Schnorr protocol in assembler via the Jasmin toolchain, and prove the security (proof-of-knowledge and zero-knowledge properties) and the absence of leakage through timing side-channels of that implementation in EasyCrypt. In order to do so, we provide a semantic characterization of leakage-freeness for probabilistic Jasmin programs (that are not constant-time). We design a library for multiple-precision integer arithmetic in Jasmin -- the "libjbn'' library. Among others,...
Cryptographic software running on embedded devices requires protection against physical side-channel attacks such as power analysis. Masking is a widely deployed countermeasure against these attacksand is directly implemented on algorithmic level. Many works study the security of masked cryptographic software on CPUs, pointing out potential problems on algorithmic/microarchitecture-level, as well as corresponding solutions, and even show masked software can be implemented efficiently and...
A zero-knowledge proof (ZKP) is a powerful cryptographic primitive used in many decentralized or privacy-focused applications. However, the high overhead of ZKPs can restrict their practical applicability. We design a programming language, Ou, aimed at easing the programmer's burden when writing efficient ZKPs, and a compiler framework, Lian, that automates the analysis and distribution of statements to a computing cluster. Lian uses programming language semantics, formal methods, and...
Zero-knowledge (ZK) proof systems have emerged as a promising solution for building security-sensitive applications. However, bugs in ZK applications are extremely difficult to detect and can allow a malicious party to silently exploit the system without leaving any observable trace. This paper presents Coda, a novel statically-typed language for building zero-knowledge applications. Critically, Coda makes it possible to formally specify and statically check properties of a ZK application...
Computationally sound protocol verification tools promise to deliver full-strength cryptographic proofs for security protocols. Unfortunately, current tools lack either modularity or automation. We propose a new approach based on a novel use of information flow and refinement types for sound cryptographic proofs. Our framework, Owl, allows type-based modular descriptions of security protocols, wherein disjoint subprotocols can be programmed and automatically proved secure separately....
ISO 15118 enables charging and billing of Electric Vehicles (EVs) without user interaction by using locally installed cryptographic credentials that must be secure over the long lifetime of vehicles. In the dawn of quantum computers, Post-Quantum Cryptography (PQC) needs to be integrated into the EV charging infrastructure. In this paper, we propose QuantumCharge, a PQC extension for ISO 15118, which includes concepts for migration, crypto-agility, verifiable security, and the use of...
This draft presents work-in-progress concerning hybrid/composite signature schemes. More concretely, we give several tailored combinations of Fiat-Shamir based signature schemes (such as Dilithium) or Falcon with RSA or DSA. We observe that there are a number of signature hybridization goals, few of which are not achieved through parallel signing or concatenation approaches. These include proof composability (that the post-quantum hybrid signature security can easily be linked to the...
This work is motivated by the following question: can an untrusted quantum server convince a classical verifier of the answer to an efficient quantum computation using only polylogarithmic communication? We show how to achieve this in the quantum random oracle model (QROM), after a non-succinct instance-independent setup phase. We introduce and formalize the notion of post-quantum interactive oracle arguments for languages in QMA, a generalization of interactive oracle proofs...
This work presents a novel machine-checked tight security proof for $\mathrm{XMSS}$ — a stateful hash-based signature scheme that is (1) standardized in RFC 8391 and NIST SP 800-208, and (2) employed as a primary building block of $\mathrm{SPHINCS}^{+}$, one of the signature schemes recently selected for standardization as a result of NIST’s post-quantum competition. In 2020, Kudinov, Kiktenko, and Fedoro pointed out a flaw affecting the tight security proofs of $\mathrm{SPHINCS}^{+}$ and...
One approach for scaling blockchains is to create bilateral, offchain channels, known as payment/state channels, that can protect parties against cheating via onchain collateralization. While such channels have been studied extensively, not much attention has been given to programmability, where the parties can agree to dynamically enforce arbitrary conditions over their payments without going onchain. We introduce the notion of a programmable payment channel ($\mathsf{PPC}$) that allows...
This paper presents a correct-by-construction method of designing an FHE model based on the automated program verifier Dafny. We model FHE operations from the ground up, including fundamentals like GCD, coprimality, Montgomery multiplications, and polynomial operations, etc., and higher level optimizations such as Residue Number System (RNS) and Number Theoretic Transform (NTT). The fully formally verified FHE model serves as a reference design for both software stack development and...
We show how to obfuscate pseudo-deterministic quantum circuits in the classical oracle model, assuming the quantum hardness of learning with errors. Given the classical description of a quantum circuit $Q$, our obfuscator outputs a quantum state $\ket{\widetilde{Q}}$ that can be used to evaluate $Q$ repeatedly on arbitrary inputs. Instantiating the classical oracle using any candidate post-quantum indistinguishability obfuscator gives us the first candidate construction of...
We extend and consolidate the security justification for the Dilithium signature scheme. In particular, we identify a subtle but crucial gap that appears in several ROM and QROM security proofs for signature schemes that are based on the Fiat-Shamir with aborts paradigm, including Dilithium. The gap lies in the CMA-to-NMA reduction and was uncovered when trying to formalize a variant of the QROM security proof by Kiltz, Lyubashevsky, and Schaffner (Eurocrypt 2018). The gap was confirmed by...
In this paper we present the first formally verified implementations of Kyber and, to the best of our knowledge, the first such implementations of any post-quantum cryptosystem. We give a (readable) formal specification of Kyber in the EasyCrypt proof assistant, which is syntactically very close to the pseudocode description of the scheme as given in the most recent version of the NIST submission. We present high-assurance open-source implementations of Kyber written in the Jasmin language,...
The field of high-assurance cryptography is quickly maturing, yet a unified foundational framework for end-to-end formal verification of efficient cryptographic implementations is still missing. To address this gap, we use the Coq proof assistant to formally connect three existing tools: (1) the Hacspec emergent cryptographic specification language; (2) the Jasmin language for efficient, high-assurance cryptographic implementations; and (3) the SSProve foundational verification framework for...
Since the post-quantum crypto system CRYSTALS-KYBER has been chosen for standardization by the National Institute for Standards and Technology (US), a formal verification of its correctness and security properties becomes even more relevant. Using the automated theorem prover Isabelle, we are able to formalize the algorithm specifications and parameter sets of Kyber's public key encryption scheme and verify the $\delta$-correctness and indistinguishability under chosen plaintext attack...
Flow is a high-throughput blockchain with a dedicated step for executing the transactions in a block and a subsequent verification step performed by Verification Nodes. To enforce integrity of the blockchain, the protocol requires a component that prevents Verification Nodes from approving execution results without checking. In our preceding work, we have sketched out an approach called Specialized Proof of Confidential Knowledge (SPoCK). Using SPoCK, nodes can provide evidence to a third...
Critical and widely used cryptographic protocols have repeatedly been found to contain flaws in their design and their implementation. A prominent class of such vulnerabilities is logical attacks, e.g. attacks that exploit flawed protocol logic. Automated formal verification methods, based on the Dolev-Yao (DY) attacker, formally define and excel at finding such flaws, but operate only on abstract specification models. Fully automated verification of existing protocol implementations is...
We introduce incoercible digital signature schemes, a variant of a standard digital signature. Incoercible signatures enable signers, when coerced to produce a signature for a message chosen by an attacker, to generate fake signatures that are indistinguishable from real signatures, even if the signer is compelled to reveal their full history (including their secret signing keys and any randomness used to produce keys/signatures) to the attacker. Additionally, we introduce an authenticator...
Most cryptographic protocols model a player’s knowledge of secrets in a simple way. Informally, the player knows a secret in the sense that she can directly furnish it as a (private) input to a protocol, e.g., to digitally sign a message. The growing availability of Trusted Execution Environments (TEEs) and secure multiparty computation, however, undermines this model of knowledge. Such tools can encumber a secret sk and permit a chosen player to access sk conditionally, without actually...
A decisive contribution to the all-embracing protection of cryptographic software, especially on embedded devices, is the protection against SCA attacks. Masking countermeasures can usually be integrated into the software during the design phase. In theory, this should provide reliable protection against such physical attacks. However, the correct application of masking is a non-trivial task that often causes even experts to make mistakes. In addition to human-caused errors,...
This paper describes a formalization of the specification and the algorithm of the cryptographic scheme CRYSTALS-KYBER as well as the verification of its (1 − δ)-correctness proof. During the formalization, a problem in the correctness proof was uncovered. In order to amend this issue, a necessary property on the modulus parameter of the CRYSTALS-KYBER algorithm was introduced. This property is already implicitly fulfilled by the structure of the modulus prime used in the number theoretic...
Developers of computer-aided cryptographic tools are optimistic that formal methods will become a vital part of developing new cryptographic systems. We study the use of such tools to specify and verify the implementation of Classic McEliece, one of the code-based cryptography candidates in the fourth round of the NIST Post-Quantum standardisation Process. From our case study we draw conclusions about the practical applicability of these methods to the development of novel cryptography.
The redundant of multimedia data made an unnecessary waste in encrypted cloud storage, unlike text with completely consistent content, multimedia data allows a certain degree of similarity in deduplication, In this work, we focus on the multimedia data which takes a seriously proportion of storage in scenarios such as data outsourcing to propose secure fuzzy deduplication without the additional servers based on Convergent Encryption(CE), say the Single-server Fuzzy Deduplication (SSFD)....
Secure cryptographic storage is one of the most important issues that both businesses and end-users take into account before moving their data to either centralized clouds or blockchain-based decen- tralized storage marketplace. Recent work [4 ] formalizes the notion of Proof of Storage-Time (PoSt) which enables storage servers to demonstrate non-interactive continuous availability of outsourced data in a publicly verifiable way. The work also proposes a stateful compact PoSt...
Anonymous authentication primitives, e.g., group or ring signatures, allow one to realize privacy-preserving data collection applications, as they strike a balance between authenticity of data being collected and privacy of data providers. At PKC 2021, Diaz and Lehmann defined group signatures with User-Controlled Linkability (UCL) and provided an instantiation based on BBS+ signatures. In a nutshell, a signer of a UCL group signature scheme can link any of her signatures: linking evidence...
The building blocks for secure messaging apps, such as Signal’s X3DH and Double Ratchet (DR) protocols, have received a lot of attention from the research community. They have notably been proved to meet strong security properties even in the case of compromise such as Forward Secrecy (FS) and Post-Compromise Security (PCS). However, there is a lack of formal study of these properties at the application level. Whereas the research works have studied such properties in the context of a single...
EDHOC is a lightweight authenticated key exchange protocol for IoT communication, currently being standardized by the IETF. Its design is a trimmed-down version of similar protocols like TLS 1.3, building on the SIGn-then-MAc (SIGMA) rationale. In its trimming, however, EDHOC notably deviates from the SIGMA design by sending only short, non-unique credential identifiers, and letting recipients perform trial verification to determine the correct communication partner. Done naively, this can...
Public verification of quantum money has been one of the central objects in quantum cryptography ever since Wiesner's pioneering idea of using quantum mechanics to construct banknotes against counterfeiting. So far, we do not know any publicly-verifiable quantum money scheme that is provably secure from standard assumptions. In this work, we provide both negative and positive results for publicly verifiable quantum money. **In the first part, we give a general theorem, showing that a...
We design and implement a simple zero-knowledge argument protocol for $\mathsf{NP}$ whose communication complexity is proportional to the square-root of the verification circuit size. The protocol can be based on any collision-resistant hash function. Alternatively, it can be made non-interactive in the random oracle model, yielding concretely efficient zk-SNARKs that do not require a trusted setup or public-key cryptography. Our protocol is obtained by applying an optimized version of the...
Ring signatures allow a user to sign messages on behalf of an ad hoc set of users - a ring - while hiding her identity. The original motivation for ring signatures was whistleblowing [Rivest et al. ASIACRYPT'01]: a high government employee can anonymously leak sensitive information while certifying that it comes from a reliable source, namely by signing the leak. However, essentially all known ring signature schemes require the members of the ring to publish a structured verification key...
Privacy is a notoriously difficult property to achieve in complicated systems and especially in electronic voting schemes. Moreover, electronic voting schemes is a class of systems that require very high assurance. The literature contains a number of ballot privacy definitions along with security proofs for common systems. Some machine-checked security proofs have also appeared. We define a new ballot privacy notion that captures a larger class of voting schemes. This notion improves on the...
COQCRYPTOLINE is an automatic certified verification tool for cryptographic programs. It is built on OCAML programs extracted from algorithms fully certified in COQ with SS- REFLECT. Similar to other automatic tools, COQCRYPTO- LINE calls external decision procedures during verification. To ensure correctness, all answers from external decision procedures are validated by certified certificate checkers in COQCRYPTOLINE. We evaluate COQCRYPTOLINE on cryp- tographic programs from BITCOIN,...
KEMTLS is a proposal for changing the TLS handshake to authenticate the handshake using long-term key encapsulation mechanism keys instead of signatures, motivated by trade-offs in the characteristics of post-quantum algorithms. Prior proofs of security of KEMTLS and its variant KEMTLS-PDK have been hand-written proofs in the reductionist model under computational assumptions. In this paper, we present computer-verified symbolic analyses of KEMTLS and KEMTLS-PDK using two distinct Tamarin...
The FIDO2 protocol is a globally used standard for passwordless authentication, building on an alliance between major players in the online authentication space. While already widely deployed, the standard is still under active development. Since version 2.1 of its CTAP sub-protocol, FIDO2 can potentially be instantiated with post-quantum secure primitives. We provide the first formal security analysis of FIDO2 with the CTAP 2.1 and WebAuthn 2 sub-protocols. Our security models build on...
Even today, SCA attacks pose a serious threat to the security of cryptographic implementations fabricated with low-power and nano-scale feature technologies. Fortunately, the masking countermeasures offer reliable protection against such attacks based on simple security assumptions. However, the practical application of masking to a cryptographic algorithm is not trivial, and the designer may overlook possible security flaws, especially when masking a complex circuit. Moreover, abstract...
We construct a classically verifiable succinct interactive argument for quantum computation (BQP) with communication complexity and verifier runtime that are poly-logarithmic in the runtime of the BQP computation (and polynomial in the security parameter). Our protocol is secure assuming the post-quantum security of indistinguishability obfuscation (iO) and Learning with Errors (LWE). This is the first succinct argument for quantum computation in the plain model; prior work...
Masking is a popular secret-sharing technique that is used to protect cryptographic implementations against physical attacks like differential power analysis. So far, most research in this direction has focused on finding efficient Boolean masking schemes for well-known symmetric cryptographic algorithms like AES and Keccak. However, especially with the advent of post-quantum cryptography (PQC), arithmetic masking has received increasing attention from the research community. In practice,...
There are numerous settings in which people's preferences are aggregated outside of formal elections, and where privacy and verification are important but the stringent authentication and coercion-resistant properties of government elections do not apply, a prime example being social media platforms. These systems are often iterative and have no trusted authority, in contrast to the centrally organised, single-shot elections on which most of the literature is focused. Moreover, they require...
Symbolic security protocol verifiers have reached a high degree of automation and maturity. Today, experts can model real-world protocols, but this often requires model-specific encodings and deep insight into the strengths and weaknesses of each of those tools. With Sapic+ , we introduce a protocol verification platform that lifts this burden and permits choosing the right tool for the job, at any development stage. We build on the existing compiler from Sapic to Tamarin, and extend it with...
The fair exchange problem has faced for a long time the bottleneck of a required trusted third party. The recent development of blockchains introduces a new type of party to this problem, whose trustworthiness relies on a public ledger and distributed computation. The challenge in this setting is to reconcile the minimalistic and public nature of blockchains with elaborate fair exchange requirements, from functionality to privacy. Zero-knowledge contingent payments (ZKCP) are a class of...
We propose a novel obfuscation technique that can be used to outsource hard satisfiability (SAT) formulas to the cloud. Servers with large computational power are typically used to solve SAT instances that model real-life problems in task scheduling, AI planning, circuit verification and more. However, outsourcing data to the cloud may lead to privacy and information breaches since satisfying assignments may reveal considerable information about the underlying problem modeled by SAT. In...
Cryptographic constant-time (CT) is a popular programming disci- pline used by cryptographic libraries to protect themselves against timing attacks. The CT discipline aims to enforce that program ex- ecution does not leak secrets, where leakage is defined by a formal leakage model. In practice, different leakage models coexist, some- times even within a single library, both to reflect different architec- tures and to accommodate different security-efficiency trade-offs. Constant-timeness is...
A proactive secret sharing scheme (PSS), expressed in the dynamic-membership setting, enables a committee of n holders of secret-shares, dubbed as players, to securely hand-over new shares of the same secret to a new committee. We dub such a sub-protocol as a Refresh. All existing PSS under an honest majority, require the use of a broadcast (BC) in each refresh. BC is costly to implement, and its security relies on timing assumptions on the network. So the privacy of the secret and/or its...
The Noise protocol framework defines a succinct notation and execution framework for a large class of 59+ secure channel protocols, some of which are used in popular applications such as WhatsApp and WireGuard. We present a verified implementation of a Noise protocol compiler that takes any Noise protocol, and produces an optimized C implementation with extensive correctness and security guarantees. To this end, we formalize the complete Noise stack in F*, from the low-level cryptographic...
The protection of cryptographic software implementations against power-analysis attacks is critical for applications in embedded systems. A commonly used algorithmic countermeasure against these attacks is masking, a secret-sharing scheme that splits a sensitive computation into computations on multiple random shares. In practice, the security of masking schemes relies on several assumptions that are often violated by microarchitectural side-effects of CPUs. Many past works address this...
Research on the design of masked cryptographic hardware circuits in the past has mostly focused on reducing area and randomness requirements. However, many embedded devices like smart cards and IoT nodes also need to meet certain performance criteria, which is why the latency of masked hardware circuits also represents an important metric for many practical applications. The root cause of latency in masked hardware circuits is the need for additional register stages that synchronize the...
Physical attacks, including passive Side-Channel Analysis and active Fault Injection Analysis, are considered among the most powerful threats against physical cryptographic implementations. These attacks are well known and research provides many specialized countermeasures to protect cryptographic implementations against them. Still, only a limited number of combined countermeasures, i.e., countermeasures that protect implementations against multiple attacks simultaneously, were proposed in...
Side channel attacks are powerful attacks for retrieving secret data by exploiting physical measurements such as power consumption or electromagnetic emissions. Masking is a popular countermeasure as it can be proven secure against an attacker model. In practice, software masked implementations suffer from a security reduction due to a mismatch between the considered leakage sources in the security proof and the real ones, which depend on the micro-architecture. We present the model of a...
In this work, we consider the formal verification of the public-key encryption scheme of Saber, one of the selected few post-quantum cipher suites currently considered for potential standardization. We formally verify this public-key encryption scheme's IND-CPA security and $\delta$-correctness properties, i.e., the properties required to transform the public-key encryption scheme into an IND-CCA2 secure and $\delta$-correct key encapsulation mechanism, in EasyCrypt. To this end, we...
This work extends the composable secure-emulation of Canetti et al. to dynamic settings. Our work builds on top of dynamic probabilistic I/O automata, a recent framework introduced to model dynamic probabilistic systems. Our extension is an important tool towards the formal verification of protocols combining probabilistic distributed systems and cryptography in dynamic settings (e.g. blockchains, secure distributed computation, cybersecure distributed protocols etc).
Masking is an important countermeasure against side-channel attacks, but its secure implementation is known to be error-prone. The automated verification and generation of masked designs is therefore an important theoretical and practical challenge. In a recent work, Knichel et al. proposed a tool for the automated generation of masked hardware implementations satisfying strong security properties (e.g., glitch-freeness and composability). In this paper, we study the possibility to improve...
Zero-knowledge (ZK) protocols enable one party to prove to others that it knows a fact without revealing any information about the evidence for such knowledge. There exist ZK protocols for all problems in NP, and recent works developed highly efficient protocols for proving knowledge of satisfying assignments to Boolean formulas, circuits and other NP formalisms. This work shows an efficient protocol for the the converse: proving formula *unsatisfiability* in ZK (when the prover posses a...
Payment channel network (PCN), not only improving the transaction throughput of blockchain but also realizing cross-chain payment, is a very promising solution to blockchain scalability problem. Most existing PCN constructions focus on either atomicity or privacy properties. Moreover, they are built on specific scripting features of the underlying blockchain such as HTLC or are tailored to several signature algorithms like ECDSA and Schnorr. In this work, we devise a Generalized Multi-Hop...
Accelerated by the increased interconnection of highly accessible devices, the demand for effective and efficient protection of hardware designs against SCA is ever rising, causing its topical relevance to remain immense in both, academia and industry. Among a wide range of proposed countermeasures against SCA, masking is a highly promising candidate due to its sound foundations and well-understood security requirements. In addition, formal adversary models have been introduced, aiming to...
Chandran et al. (SIAM J. Comput.'14) formally introduced the cryptographic task of position verification, where they also showed that it cannot be achieved by classical protocols. In this work, we initiate the study of position verification protocols with classical verifiers. We identify that proofs of quantumness (and thus computational assumptions) are necessary for such position verification protocols. For the other direction, we adapt the proof of quantumness protocol by Brakerski et al....
Today's data-intensive applications increasingly suffer from significant performance bottlenecks due to the limited memory bandwidth of the classical von Neumann architecture. Near-Data Processing (NDP) has been proposed to perform computation near memory or data storage to reduce data movement for improving performance and energy consumption. However, the untrusted NDP processing units (PUs) bring in new threats to workloads that are private and sensitive, such as private database queries...
The ability to verifiably retrieve transaction or state data stored off-chain is crucial to blockchain scaling techniques such as rollups or sharding. We formalize the problem and design a storage- and communication-efficient protocol using linear erasure-correcting codes and homomorphic vector commitments. Motivated by application requirements for rollups, our solution Semi-AVID-PR departs from earlier Verifiable Information Dispersal schemes in that we do not require comprehensive...
Masking countermeasure is implemented to thwart side-channel attacks. The maturity of high-order masking schemes has reached the level where the concepts are sound and proven. For instance, Rivain and Prouff proposed a full-fledged AES at CHES 2010. Some non-trivial fixes regarding refresh functions were needed though. Now, industry is adopting such solutions, and for the sake of both quality and certification requirements, masked cryptographic code shall be checked for correctness using the...
Deep attestation is a particular case of remote attestation, i.e., verifying the integrity of a platform with a remote verification server. We focus on the remote attestation of hypervisors and their hosted virtual machines (VM), for which two solutions are currently supported by ETSI. The first is single-channel attestation, requiring for each VM an attestation of that VM and the underlying hypervisor through the physical TPM. The second, multi-channel attestation, allows to attest VMs via...
Side-channel attacks are a powerful class of attacks targeting cryptographic devices. Masking is a popular protection technique to thwart such attacks as it can be theoretically proven secure. However, correctly implementing masking schemes is a non-trivial task and error-prone. If several techniques have been proposed to formally verify masked implementations, they all come with limitations regarding expressiveness, scalability or accuracy. In this work, we propose a symbolic approach,...
Branching program (BP) is a DAG-based non-uniform computational model for L/poly class. It has been widely used in formal verification, logic synthesis, and data analysis. As a special BP, a decision tree is a popular machine learning classifier for its effectiveness and simplicity. In this work, we propose a UC-secure efficient 3-party computation platform for outsourced branching program and/or decision tree evaluation. We construct a constant-round protocol and a linear-round protocol. In...
Sender-anonymous end-to-end encrypted messaging allows sending messages to a recipient without revealing the sender’s identity to the messaging platform. Signal recently introduced a sender anonymity feature that includes an abuse mitigation mechanism meant to allow the platform to block malicious senders on behalf of a recipient. We explore the tension between sender anonymity and abuse mitigation. We start by showing limitations of Signal’s deployed mechanism, observing that it results in...
EasyCrypt is a formal verification tool used extensively for formalizing concrete security proofs of cryptographic constructions. However, the EasyCrypt formal logics consider only classical attackers, which means that post-quantum security proofs cannot be formalized and machine-checked with this tool. In this paper we prove that a natural extension of the EasyCrypt core logics permits capturing a wide class of post-quantum cryptography proofs, settling a question raised by (Unruh, POPL...
Belenios is an online voting system that provides a strong notion of election verifiability, where no single party has to be trusted, and security holds as soon as either the voting registrar or the voting server is honest. It was formally proved to be secure, making the assumption that no further ballots are cast on the bulletin board after voters verified their ballots. In practice, however, revoting is allowed and voters can verify their ballots anytime. This gap between formal proofs and...
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 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...
