(Page 2 of) 265 results sorted by ID
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...
Clockwork Finance: Automated Analysis of Economic Security in Smart Contracts
Kushal Babel, Philip Daian, Mahimna Kelkar, Ari Juels
Applications
We introduce the Clockwork Finance Framework (CFF), a general purpose, formal verification framework for mechanized reasoning about the economic security properties of composed decentralized-finance (DeFi) smart contracts.
CFF features three key properties. It is contract complete, meaning that it can model any smart contract platform and all its contracts—Turing complete or otherwise. It does so with asymptotically constant model overhead. It is also attack-exhaustive by construction,...
Secure and Efficient Software Masking on Superscalar Pipelined Processors
Barbara Gigerl, Robert Primas, Stefan Mangard
Applications
Physical side-channel attacks like power analysis pose a serious threat to cryptographic devices in real-world applications. Consequently, devices implement algorithmic countermeasures like masking.
In the past, works on the design and verification of masked software implementations have mostly focused on simple microprocessors that find usage on smart cards. However, many other applications such as in the automotive industry require side-channel protected cryptographic computations on much...
A Formal Security Analysis of the W3C Web Payment APIs: Attacks and Verification
Quoc Huy Do, Pedram Hosseyni, Ralf Kuesters, Guido Schmitz, Nils Wenzler, Tim Wuertele
Cryptographic protocols
Payment is an essential part of e-commerce. Merchants usually rely on third-parties, so-called payment processors, who take care of transferring the payment from the customer to the merchant. How a payment processor interacts with the customer and the merchant varies a lot. Each payment processor typically invents its own protocol that has to be integrated into the merchant’s application and provides the user with a new, potentially unknown and confusing user experience.
Pushed by major...
FIVER -- Robust Verification of Countermeasures against Fault Injections
Jan Richter-Brockmann, Aein Rezaei Shahmirzadi, Pascal Sasdrich, Amir Moradi, Tim Güneysu
Fault Injection Analysis is seen as a powerful attack against implementations of cryptographic algorithms. Over the last two decades, researchers proposed a plethora of countermeasures to secure such implementations. However, the design process and implementation are still error-prone, complex, and manual tasks which require long-standing experience in hardware design and physical security. Moreover, the validation of the claimed security is often only done by empirical testing in a very...
Mithril: Stake-based Threshold Multisignatures
Pyrros Chaidos, Aggelos Kiayias
Cryptographic protocols
Stake-based multiparty cryptographic primitives operate in a setting where participants are associated with their stake, security is argued against an adversary that is bounded by the total stake it possesses —as opposed to number of parties— and we are interested in scalability, i.e., the complexity of critical operations depends only logarithmically in the number of participants (who are assumed to be numerous).
In this work we put forth a new stake-based primitive, stake-based...
Progressive And Efficient Verification For Digital Signatures
Cecilia Boschini, Dario Fiore, Elena Pagnin
Public-key cryptography
Digital signatures are widely deployed to authenticate the source of incoming information, or to certify data integrity. Common signature verification procedures return a decision (accept/reject) only at the very end of the execution. If interrupted prematurely, however, the verification process cannot infer any meaningful information about the validity of the given signature. We notice that this limitation is due to the algorithm design solely, and it is not inherent to signature...
Probabilistic Dynamic Input Output Automata (Extended Version)
Pierre Civit, Maria Potop-Butucaru
Foundations
We present probabilistic dynamic I/O automata, a framework to model dynamic probabilistic systems. Our work extends dynamic I/O Automata formalism of Attie & Lynch to probabilistic setting. The original dynamic I/O Automata formalism included operators for parallel composition, action hiding, action renaming, automaton creation, and behavioral sub-typing by means of trace inclusion. They can model mobility by using signature modification. They are also hierarchical: a dynamically changing...
High-assurance field inversion for curve-based cryptography
Benjamin Salling Hvass, Diego F. Aranha, Bas Spitters
Implementation
The security of modern cryptography depends on multiple factors, from sound hardness assumptions to correct implementations that resist side-channel cryptanalysis. Curve-based cryptography is not different in this regard, and substantial progress in the last few decades has been achieved in both selecting parameters and devising secure implementation strategies. In this context, the security of implementations of field inversion is sometimes overlooked in the research literature, because
...
A Coq proof of the correctness of X25519 in TweetNaCl
Peter Schwabe, Benoît Viguier, Timmy Weerwag, Freek Wiedijk
Public-key cryptography
We formally prove that the C implementation of the X25519 key-exchange protocol in the TweetNaCl library is correct. We prove both that it correctly implements the protocol from Bernstein's 2006 paper, as standardized in RFC 7748, as well as the absence of undefined behavior like arithmetic overflows and array out-of-bounds errors. We also formally prove, based on the work of Bartzia and Strub, that X25519 is mathematically correct, i.e., that it correctly computes scalar multiplication on...
Efficient Verification of Optimized Code: Correct High-speed X25519
Marc Schoolderman, Jonathan Moerman, Sjaak Smetsers, Marko van Eekelen
Implementation
Code that is highly optimized poses a problem for program-level verification: programmers can employ various clever tricks that are non-trivial to reason about. For cryptography on low-power devices, it is nonetheless crucial that implementations be functionally correct, secure, and efficient. These are usually crafted in hand-optimized machine code that eschew conventional control flow as much as possible.
We have formally verified such code: a library which implements elliptic curve...
Leakage Resilient Value Comparison With Application to Message Authentication
Christoph Dobraunig, Bart Mennink
Side-channel attacks are a threat to secrets stored on a device, especially if an adversary has physical access to the device. As an effect of this, countermeasures against such attacks for cryptographic algorithms are a well-researched topic. In this work, we deviate from the study of cryptographic algorithms and instead focus on the side-channel protection of a much more basic operation, the comparison of a known attacker-controlled value with a secret one. Comparisons sensitive to...
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq
Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Carmine Abate, Nikolaj Sidorenco, Catalin Hritcu, Kenji Maillard, Bas Spitters
Foundations
State-separating proofs (SSP) is a recent methodology for structuring game-based cryptographic proofs in a modular way, by using algebraic laws to exploit the modular structure of composed protocols. While promising, this methodology was previously not fully formalized and came with little tool support. We address this by introducing SSProve, the first general verification framework for machine-checked state-separating proofs. SSProve combines high-level modular proofs about composed...
Veksel: Simple, Efficient, Anonymous Payments with Large Anonymity Sets from Well-Studied Assumptions
Matteo Campanelli, Mathias Hall-Andersen
Cryptographic protocols
We propose Veksel, a simple generic paradigm for constructing efficient non-interactive coin mixes. The central component in our work is a concretely efficient proof $\pi_{one-many}$ that a homomorphic commitment $c^*$ is a rerandomization of a commitment $c \in \{c_1, \ldots, c_\ell \}$ without revealing $c$. We formalize anonymous account-based cryptocurrency as a universal composability functionality and show how to efficiently instantiate the functionality using $\pi_{one-many}$ in a...
On the Relationships between Different Methods for Degree Evaluation (Full Version)
Siwei Chen, Zejun Xiang, Xiangyong Zeng, Shasha Zhang
Secret-key cryptography
In this paper, we compare several non-tight degree evaluation methods i.e., Boura and Canteaut's formula, Carlet's formula as well as Liu's numeric mapping and division property proposed by Todo, and hope to find the best one from these methods for practical applications. Specifically, for the substitution-permutation-network (SPN) ciphers, we first deeply explore the relationships between division property of an Sbox and its algebraic properties (e.g., the algebraic degree of its inverse)....
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability
Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub
Foundations
EasyCrypt is a proof assistant used for verifying computational
security proofs of cryptographic constructions. It has been applied to
several prominent examples, including the SHA3 standard and a
critical component of AWS Key Management Services.
In this paper we enhance the EasyCrypt proof assistant to reason
about computational complexity of adversaries. The key technical
tool is a Hoare logic for reasoning about computational complexity
(execution time and oracle calls) of adversarial...
IPDL: A Simple Framework for Formally Verifying Distributed Cryptographic Protocols
Greg Morrisett, Elaine Shi, Kristina Sojakova, Xiong Fan, Joshua Gancher
Although there have been many successes in verifying proofs of non-interactive cryptographic primitives such as encryption and signatures, formal verification of interactive cryptographic protocols is still a nascent area. While in principle, it seems possible to extend general frameworks such as Easycrypt to encode proofs for more complex, interactive protocols, a big challenge is whether the human effort would be scalable enough for proof mechanization to eventually acquire mainstream...
Single-Message Credential-Hiding Login
Kevin Lewi, Payman Mohassel, Arnab Roy
The typical login protocol for authenticating a user to a web service involves the client sending a password over a TLS-secured channel to the service, occasionally deployed with the password being prehashed. This widely-deployed paradigm, while simple in nature, is prone to both inadvertent logging and eavesdropping attacks, and has repeatedly led to the exposure of passwords in plaintext.
Partly to address this problem, symmetric and asymmetric PAKE protocols were developed to ensure that...
Analysing the HPKE Standard
Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp, Doreen Riepel
Public-key cryptography
The Hybrid Public Key Encryption (HPKE) scheme is an emerging standard currently under consideration by the Crypto Forum Research Group (CFRG) of the IETF as a candidate for formal approval. Of the four modes of HPKE, we analyse the authenticated mode HPKE_Auth in its single-shot encryption form as it contains what is, arguably, the most novel part of HPKE and has applications to other upcoming standards such as MLS.
HPKE_Auth’s intended application domain is captured by a new primitive...
Machine-checking the universal verifiability of ElectionGuard
Thomas Haines, Rajeev Gore, Jack Stodart
Implementation
ElectionGuard is an open source set of software components and specifications from Microsoft designed to allow the modification of a number of different e-voting protocols and products to produce public evidence (transcripts) which anyone can verify. The software uses ElGamal, homomorphic tallying and sigma protocols to enable public scrutiny without adversely affecting privacy. Some components have been formally verified (machine-checked) to be free of certain software bugs but there was no...
Vetted Encryption
Martha Norberg Hovd, Martijn Stam
Public-key cryptography
We introduce Vetted Encryption (VE), a novel cryptographic primitive, which addresses the following scenario: a receiver controls, or vets, who can send them encrypted messages. We model this as a filter publicly checking ciphertext validity, where the overhead does not grow with the number of senders. The filter receives one public key for verification, and every user receives one personal encryption key.
We present three versions: Anonymous, Identifiable, and Opaque VE (AVE, IVE and OVE),...
Post-Quantum Adaptor Signature for Privacy-Preserving Off-Chain Payments
Erkan Tairi, Pedro Moreno-Sanchez, Matteo Maffei
Applications
Adaptor signatures (AS) are an extension of digital signatures that enable the encoding of a cryptographic hard problem (e.g., discrete logarithm) within the signature itself. An AS scheme ensures that (i) the signature can be created only by the user knowing the solution to the cryptographic problem; (ii) the signature reveals the solution itself; (iii) the signature can be verified with the standard verification algorithm. These properties have made AS a salient building block for many...
Coco: Co-Design and Co-Verification of Masked Software Implementations on CPUs
Barbara Gigerl, Vedad Hadzic, Robert Primas, Stefan Mangard, Roderick Bloem
Implementation
The protection of cryptographic implementations against power analysis attacks is of critical importance for many applications in embedded systems. The typical approach of protecting against these attacks is to implement algorithmic countermeasures, like masking. However, implementing these countermeasures in a secure and correct manner is challenging. Masking schemes require the independent processing of secret shares, which is a property that is often violated by CPU microarchitectures in...
Taming the many EdDSAs
Konstantinos Chalkias, François Garillot, Valeria Nikolaenko
Public-key cryptography
This paper analyses security of concrete instantiations of EdDSA by identifying exploitable inconsistencies between standardization recommendations and Ed25519 implementations. We mainly focus on current ambiguity regarding signature verification equations, binding and malleability guarantees, and incompatibilities between randomized batch and single verification. We give a formulation of Ed25519 signature scheme that achieves the highest level of security, explaining how each step of the...
Election Verifiability Revisited: Automated Security Proofs and Attacks on Helios and Belenios
Sevdenur Baloglu, Sergiu Bursuc, Sjouke Mauw, Jun Pang
Foundations
Election verifiability aims to ensure that the outcome produced by electronic voting systems correctly reflects the intentions of eligible voters, even in the presence of an adversary that may corrupt various parts of the voting infrastructure. Protecting such systems from manipulation is challenging because of their distributed nature involving voters, election authorities, voting servers and voting platforms. An adversary corrupting any of these can make changes that, individually, would...
Post-Quantum Verification of Fujisaki-Okamoto
Dominique Unruh
Public-key cryptography
We present a computer-verified formalization of the post-quantum
security proof of the Fujisaki-Okamoto transform (as analyzed by
Hövelmanns, Kiltz, Schäge, and Unruh, PKC 2020). The formalization is
done in quantum relational Hoare logic and checked in the qrhl-tool
(Unruh, POPL 2019).
Proof of Storage-Time: Efficiently Checking Continuous Data Availability
Giuseppe Ateniese, Long Chen, Mohammad Etemad, Qiang Tang
Applications
A high-quality outsourced storage service is crucial for many existing applications. For example, hospitals and data centers need to guarantee the availability of their systems to perform routine daily activities. Such a system should protect users against downtime and ensure data availability over time. Continuous data availability is a critical property to measure the quality of an outsourced storage service, which implies that outsourced data is continuously available to the server...
Random Probing Security: Verification, Composition, Expansion and New Constructions
Sonia Belaïd, Jean-Sébastien Coron, Emmanuel Prouff, Matthieu Rivain, Abdul Rahman Taleb
Foundations
The masking countermeasure is among the most powerful countermeasures to counteract side-channel attacks. Leakage models have been exhibited to theoretically reason on the security of such masked implementations. So far, the most widely used leakage model is the probing model defined by Ishai, Sahai, and Wagner at (CRYPTO 2003). While it is advantageously convenient for security proofs, it does not capture an adversary exploiting full leakage traces as, e.g., in horizontal attacks. Those...
SAKE+: Strengthened Symmetric-Key Authenticated Key Exchange with Perfect Forward Secrecy for IoT
Seyed Farhad Aghili, Amirhossein Adavoudi Jolfaei, Aysajan Abidin
Cryptographic protocols
Lightweight authenticated key exchange (AKE) protocols based on symmetric-key cryptography are important in securing the Internet of Things (IoT). However, achieving perfect forward secrecy (PFS) is not trivial for AKE based on symmetric-key cryptography, as opposed to AKE based on public-key cryptography. The most recent proposals that provide PFS are SAKE and SAKE-AM. In this paper, we first take a closer look at these protocols and observe that they have some limitations, specially when...
SILVER - Statistical Independence and Leakage Verification
David Knichel, Pascal Sasdrich, Amir Moradi
Implementation
Implementing cryptographic functions securely in the presence of physical adversaries is still a challenge although a lion's share of research in the physical security domain has been put in development of countermeasures. Among several protection schemes, masking has absorbed the most attention of research in both academic and industrial communities, due to its theoretical foundation allowing to provide proofs or model the achieved security level. In return, masking schemes are difficult to...
Masking in Fine-Grained Leakage Models: Construction, Implementation and Verification
Gilles Barthe, Marc Gourjon, Benjamin Gregoire, Maximilian Orlt, Clara Paglialonga, Lars Porth
We propose a new approach for building efficient, provably secure, and practically hardened implementations of masked algorithms. Our approach is based on a Domain Specific Language in which users can write efficient assembly implementations and fine-grained leakage models. The latter are then used as a basis for formal verification, allowing for the first time formal guarantees for a broad range of device-specific leakage effects not addressed by prior work.
The practical benefits of our...
HACL×N: Verified Generic SIMD Crypto (for all your favorite platforms)
Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, Santiago Zanella-Béguelin
Implementation
We present a new methodology for building formally verified cryptographic libraries that are optimized for multiple architectures. In particular, we show how to write and verify generic crypto code in the F* programming language that exploits single-instruction multiple data (SIMD) parallelism. We show how this code can be compiled to platforms that supports vector instructions, including ARM Neon and Intel AVX, AVX2, and AVX512. We apply our methodology to obtain verified vectorized...
Aggregatable Subvector Commitments for Stateless Cryptocurrencies
Alin Tomescu, Ittai Abraham, Vitalik Buterin, Justin Drake, Dankrad Feist, Dmitry Khovratovich
Public-key cryptography
An aggregatable subvector commitment (aSVC) scheme is a vector commitment (VC) scheme that can aggregate multiple proofs into a single, small subvector proof. In this paper, we formalize aSVCs and give a construction from constant-sized polynomial commitments. Our construction is unique in that it has linear-sized public parameters, it can compute all constant-sized proofs in quasilinear time, it updates proofs in constant time and it can aggregate multiple proofs into a constant-sized...
Tornado: Automatic Generation of Probing-Secure Masked Bitsliced Implementations
Sonia Belaïd, Pierre-Evariste Dagand, Darius Mercadier, Matthieu Rivain, Raphaël Wintersdorff
Implementation
Cryptographic implementations deployed in real world devices often aim at (provable) security against the powerful class of side-channel attacks while keeping reasonable performances. Last year at Asiacrypt, a new formal verification tool named tightPROVE was put forward to exactly determine whether a masked implementation is secure in the well-deployed probing security model for any given security order t. Also recently, a compiler named Usuba was proposed to automatically generate...
An Analysis of Hybrid Public Key Encryption
Benjamin Lipp
Cryptographic protocols
Hybrid Public Key Encryption (HPKE) is a cryptographic primitive being standardized by the Crypto Forum Research Group (CFRG) within the Internet Research Task Force (IRTF). HPKE schemes combine asymmetric and symmetric cryptographic primitives for efficient authenticated encryption of arbitrary-sized plaintexts under a given recipient public key. This document presents a mechanized cryptographic analysis done with CryptoVerif, of all four HPKE modes, instantiated with a prime-order-group...
A Verifiable and Practical Lattice-Based Decryption Mix Net with External Auditing
Xavier Boyen, Thomas Haines, Johannes Mueller
Applications
Mix nets are often used to provide privacy in modern security protocols, through shuffling. Some of the most important applications, such as secure electronic voting, require mix nets that are verifiable. In the literature, numerous techniques have been proposed to make mix nets verifiable. Some of them have also been employed for securing real political elections.
With the looming possibility of quantum computers and their threat to cryptosystems based on classical hardness assumptions,...
Relaxed freshness in component authentication
Frank Schuhmacher
Foundations
We suggests a relaxed freshness paradigm for challenge-response authentication for each field of application where challenger and responder are tightly coupled and authentication takes place in a friendly environment. Replay attacks are not feasible under this premise, and freshness can be relaxed to relative freshness: no refresh is required as long as all previously tested responders were authentic. One field of application is anti-counterfeiting of electronic device components. The main...
Supersingular Isogeny-Based Designated Verifier Blind Signature
Rajeev Anand Sahu, Agnese Gini, Ankan Pal
Public-key cryptography
Recently, Srinath and Chandrasekaran have proposed an undeniable blind signature scheme (UBSS) from supersingular isogeny to provide signer’s control in a quantum-resistant blind signature. However, certain weaknesses of undeniable signature have already been observed and have been overcome by formalizing the designated verifier signature (DVS). In this paper, we explore the possibility of generic construction of a DVS from hard homogeneous spaces. Further, following this...
IPDL: A Probabilistic Dataflow Logic for Cryptography
Xiong Fan, Joshua Gancher, Greg Morrisett, Elaine Shi, Kristina Sojakova
Cryptographic protocols
While there have been many successes in verifying cryptographic security proofs of noninter- active primitives such as encryption and signatures, less attention has been paid to interactive cryptographic protocols. Interactive protocols introduce the additional verification challenge of concurrency, which is notoriously hard to reason about in a cryptographically sound manner.
When proving the (approximate) observational equivalance of protocols, as is required by simulation based security...
SoK: Computer-Aided Cryptography
Manuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, Bryan Parno
Implementation
Computer-aided cryptography is an active area of research that develops and
applies formal, machine-checkable approaches to the design, analysis, and
implementation of cryptography. We present a cross-cutting systematization of
the computer-aided cryptography literature, focusing on three main areas:
(i) design-level security (both symbolic security and computational
security), (ii) functional correctness and efficiency, and (iii)
implementation-level security (with a focus on digital...
Are These Pairing Elements Correct? Automated Verification and Applications
Susan Hohenberger, Satyanarayana Vusirikala
Applications
Using a set of pairing product equations (PPEs) to verify the correctness of an untrusted set of pairing elements with respect to another set of trusted elements has numerous cryptographic applications. These include the design of basic and structure-preserving signature schemes, building oblivious transfer schemes from “blind” IBE, finding new verifiable random functions and keeping the IBE/ABE authority “accountable” to the user.
A natural question to ask is: are all trusted-untrusted...
BlockMaze: An Efficient Privacy-Preserving Account-Model Blockchain Based on zk-SNARKs
Zhangshuang Guan, Zhiguo Wan, Yang Yang, Yan Zhou, Butian Huang
Applications
The disruptive blockchain technology is expected to have broad applications in many areas due to its advantages of transparency, fault tolerance, and decentralization, but the open nature of blockchain also introduces severe privacy issues. Since anyone can deduce private information about relevant accounts, different privacy-preserving techniques have been proposed for cryptocurrencies under the UTXO model, e.g., Zerocash and Monero. However, it is more challenging to protect privacy for...
Release of Unverified Plaintext: Tight Unified Model and Application to ANYDAE
Donghoon Chang, Nilanjan Datta, Avijit Dutta, Bart Mennink, Mridul Nandi, Somitra Sanadhya, Ferdinand Sibleyras
Secret-key cryptography
Authenticated encryption schemes are usually expected to offer confidentiality and authenticity. In case of release of unverified plaintext (RUP), an adversary gets separated access to the decryption and verification functionality, and has more power in breaking the scheme. Andreeva et al. (ASIACRYPT 2014) formalized RUP security using plaintext awareness, informally meaning that the decryption functionality gives no extra power in breaking confidentiality, and INT-RUP security, covering...
Anonyma: Anonymous Invitation-Only Registration in Malicious Adversarial Model
Sanaz Taheri Boshrooyeh, Alptekin Küpçü, Öznur Özkasap
Applications
In invitation-based systems, a new user can register upon having a threshold number of invitations issued by the existing members. The newcomer hands his invitations to the system administrator who verifies whether the invitations are issued by legitimate members. This causes the administrator to be aware of who is invited by whom. However, the inviter-invitee relationship is privacy-sensitive information and can lead to inference attacks where the invitee's profile (e.g., political view or...
Stronger Security and Constructions of Multi-Designated Verifier Signatures
Ivan Damgård, Helene Haagh, Rebekah Mercer, Anca Nițulescu, Claudio Orlandi, Sophia Yakoubov
Cryptographic protocols
Off-the-Record (OTR) messaging is a two-party message authentication protocol that also provides plausible deniability: there is no record that can later convince a third party what messages were actually sent. To extend OTR to group messaging we need to consider issues that are not present in the 2-party case. In group OTR (as in two-party OTR), the sender should be able to authenticate (or sign) his messages so that group members can verify who sent a message (that is, signatures should be...
Proof-of-Burn
Kostis Karantias, Aggelos Kiayias, Dionysis Zindros
Cryptographic protocols
Proof-of-burn has been used as a mechanism to destroy cryptocurrency in a verifiable manner. Despite its well known use, the mechanism has not been previously formally studied as a primitive. In this paper, we put forth the first cryptographic definition of what a proof-of-burn protocol is. It consists of two functions: First, a function which generates a cryptocurrency address. When a user sends money to this address, the money is irrevocably destroyed. Second, a verification function...
A Conditional Privacy Preserving Authentication and Multi Party Group Key Establishment Scheme for Real-Time Application in VANETs
Swapnil Paliwal, Anvita Chandrakar
Cryptographic protocols
Vehicular Ad-hoc Networks (VANETs) are a cardinal part of intelligent transportation system (ITS) which render various services in terms of traffic and transport management. The VANET is used to manage growing traffic and manage data about traffic conditions, weather, road conditions, speed of the vehicle, etc. Even though, VANETs are self-sufficient and effective networks but they still suffer from various security and privacy issues. VANETs need to ensure that an adversary should not be...
Card-based Cryptography Meets Formal Verification
Alexander Koch, Michael Schrempp, Michael Kirsten
Cryptographic protocols
Card-based cryptography provides simple and practicable protocols for performing secure multi-party computation (MPC) with just a deck of cards. For the sake of simplicity, this is often done using cards with only two symbols, e.g., clubs and hearts. Within this paper, we target the setting where all cards carry distinct symbols, catering for use-cases with commonly available standard decks and a weaker indistinguishability assumption. As of yet, the literature provides for only three...
Verifpal: Cryptographic Protocol Analysis for the Real World
Nadim Kobeissi, Georgio Nicolas, Mukesh Tiwari
Cryptographic protocols
Verifpal is a new automated modeling framework and verifier for cryptographic protocols, optimized with heuristics for common-case protocol specifications, that aims to work better for real-world practitioners, students and engineers without sacrificing comprehensive formal verification features. In order to achieve this, Verifpal introduces a new, intuitive language for modeling protocols that is easier to write and understand than the languages employed by existing tools. Its formal...
2019/970
Last updated: 2019-09-02
Puncturable Signatures and Applications in Proof-of-Stake Blockchain Protocol
Xinyu Li, Jing Xu, Xiong Fan, Yuchen Wang, Zhenfeng Zhang
Applications
Proof-of-stake (PoS) blockchain protocols are emerging as one of the most promising alternative to the energy-consuming proof-of-work protocols. However, one particularly critical threat in the PoS setting is the well-known long-range attacks caused by secret key leakage (LRSL attack). Specifically, an adversary can attempt to corrupt the secret keys corresponding to accounts possessing substantial stake at some past moment such that double-spend or erase past transactions, violating the...
Formal Verification of a Constant-Time Preserving C Compiler
Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu
Implementation
Timing side-channels are arguably one of the main sources of
vulnerabilities in cryptographic implementations. One effective
mitigation against timing side-channels is to write programs that do
not perform secret-dependent branches and memory accesses. This
mitigation, known as ''cryptographic constant-time'', is
adopted by several popular cryptographic libraries.
This paper focuses on compilation of cryptographic constant-time
programs, and more specifically on the following question: is...
Your Money or Your Life---Modeling and Analyzing the Security of Electronic Payment in the UC Framework
Dirk Achenbach, Roland Gröll, Timon Hackenjos, Alexander Koch, Bernhard Löwe, Jeremias Mechler, Jörn Müller-Quade, Jochen Rill
Cryptographic protocols
EMV, also known as Chip and PIN, is the world-wide standard for card-based electronic payment. Its security wavers: over the past years, researchers have demonstrated various practical attacks, ranging from using stolen cards by disabling PIN verification to cloning cards by pre-computing transaction data. Most of these attacks rely on violating certain unjustified and not explicitly stated core assumptions upon which EMV is built, namely that the input device (e.g. the ATM) is trusted and...
Arcula: A Secure Hierarchical Deterministic Wallet for Multi-asset Blockchains
Adriano Di Luzio, Danilo Francati, Giuseppe Ateniese
Applications
This work presents Arcula, a new design for hierarchical deterministic wallets that brings identity-based addresses to the blockchain. Arcula is built on top of provably secure cryptographic primitives. It generates all its cryptographic secrets from a user-provided seed and enables the derivation of new public keys based on the identities of users, without requiring any secret information. Unlike other wallets, it achieves all these properties while being secure against privilege...
Can Verifiable Delay Functions be Based on Random Oracles?
Mohammad Mahmoody, Caleb Smith, David J. Wu
Foundations
Boneh, Bonneau, Bünz, and Fisch (CRYPTO 2018) recently introduced the notion of a verifiable delay function (VDF). VDFs are functions that take a long sequential time $T$ to compute, but whose outputs $y = \mathsf{Eval}(x)$ can be efficiently verified (possibly given a proof $\pi$) in time $t \ll T$ (e.g., $t=\mathrm{poly}(\lambda, \log T)$ where $\lambda$ is the security parameter). The first security requirement on a VDF, called uniqueness, is that no polynomial-time algorithm can find a...
EasyUC: Using EasyCrypt to Mechanize Proofs of Universally Composable Security
Ran Canetti, Alley Stoughton, Mayank Varia
Cryptographic protocols
We present a methodology for using the EasyCrypt proof assistant (originally designed for mechanizing the generation of proofs of game-based security of cryptographic schemes and protocols) to mechanize proofs of security of cryptographic protocols within the universally composable (UC) security framework. This allows, for the first time, the mechanization and formal verification of the entire sequence of steps needed for proving simulation-based security in a modular way:
* Specifying a...
Verification of Authenticated Firmware Load
Sujit Kumar Muduli, Pramod Subramanyan, Sayak Ray
Foundations
An important primitive in ensuring security of modern systems-on-chip designs are protocols for authenticated firmware load. These loaders read a firmware binary image from an untrusted input device, authenticate the image using cryptography and load the image into memory for execution if authentication succeeds. While these protocols are an essential part of the hardware root of trust in almost all modern computing devices, verification techniques for reasoning about end-to-end security of...
Formally Verified Cryptographic Web Applications in WebAssembly
Jonathan Protzenko, Benjamin Beurdouche, Denis Merigoux, Karthikeyan Bhargavan
Implementation
After suffering decades of high-profile attacks, the need for formal verification of security-critical software has never been clearer. Verification-oriented programming languages like F* are now being used to build high-assurance cryptographic libraries and implementations of standard protocols like TLS. In this paper, we seek to apply these verification techniques to modern Web applications, like WhatsApp, that embed sophisticated custom cryptographic components. The problem is that these...
Prime, Order Please! Revisiting Small Subgroup and Invalid Curve Attacks on Protocols using Diffie-Hellman
Cas Cremers, Dennis Jackson
Cryptographic protocols
Diffie-Hellman groups are a widely used component in cryptographic protocols in which a shared secret is needed. These protocols are typically proven to be secure under the assumption they are implemented with prime order Diffie Hellman groups. However, in practice, many implementations either choose to use non-prime order groups for reasons of efficiency, or can be manipulated into operating in non-prime order groups. This leaves a gap between the proofs of protocol security, which assume...
Refinement and Verification of CBC Casper
Ryuya Nakamura, Takayuki Jimba, Dominik Harz
Cryptographic protocols
Decentralised ledgers are a prime application case for consensus protocols. Changing sets of validators have to agree on a set of transactions in an asynchronous network and in the presence of Byzantine behaviour. Major research efforts focus on creating consensus protocols under such conditions, with proof-of-stake (PoS) representing a promising candidate. PoS aims to reduce the waste of energy inherent to proof-of-work (PoW) consensus protocols. However, a significant challenge is to get...
KeyForge: Mitigating Email Breaches with Forward-Forgeable Signatures
Michael Specter, Sunoo Park, Matthew Green
Cryptographic protocols
Email breaches are commonplace, and they expose a wealth of personal, business, and political data whose release may have devastating consequences. Such damage is compounded by email’s strong attributability: today, any attacker who gains access to your email can easily prove to others that the stolen messages are authentic, a property arising from a necessary anti-spam/anti-spoofing protocol called DKIM. This greatly increases attackers’ capacity to do harm by selling the stolen information...
Lelantus: A New Design for Anonymous and Confidential Cryptocurrencies
Aram Jivanyan
Cryptographic protocols
For cryptocurrency payments to be truly private, transactions have to have two
properties: confidentiality, i.e., hiding the transferred amounts, and anonymity, i.e. hiding the
identities of the sender and/or receiver in a transaction.
In this paper, we propose Lelantus, a new decentralized anonymous payment (DAP) protocol
that ensures confidential and anonymous blockchain transactions with small transaction sizes,
short verification times, and without requiring a trusted setup. It...
A Formal Approach to Secure Speculation
Kevin Cheang, Cameron Rasmussen, Sanjit Seshia, Pramod Subramanyan
Implementation
Transient execution attacks like Spectre, Meltdown and Foreshadow have shown that combinations of microarchitectural side-channels can be synergistically exploited to create side-channel leaks that are greater than the sum of their parts. While both hardware and software mitigations have been proposed against these attacks, provable security has remained elusive. This paper introduces a formal methodology for enabling secure speculative execution on modern processors. We propose a new class...
2018/1243
Last updated: 2020-08-19
BoxDB: Realistic Adversary Model for Distance Bounding
Ioana Boureanu, David Gerault, Pascal Lafourcade
Cryptographic protocols
Recently, the worldwide-used EMVCo standard for electronic payments included the “EMV RRP (Europay Mastercard Visa Relay-Resistant Protocol)” protocol. This uses distance bounding to counteract relay attacks in contactless payments. Last year, EMV RRP was widely analysed by symbolic verification methods, with several distance-bounding attacks and fixes proposed. Yet, one version of EMV RRP was found secure by all such formal analyses. Contrary to this, we exhibit an attack on this version of...
Proof-of-Work Sidechains
Aggelos Kiayias, Dionysis Zindros
Cryptographic protocols
During the last decade, the blockchain space has exploded with a plethora of new cryptocurrencies, covering a wide array of different features, performance and security characteristics. Nevertheless, each of these coins functions in a stand-alone manner, independently. Sidechains have been envisioned as a mechanism to allow blockchains to communicate with one another and, among other applications, allow the transfer of value from one chain to another, but so far there have been no...
Sharing Independence & Relabeling: Efficient Formal Verification of Higher-Order Masking
Roderick Bloem, Rinat Iusupov, Martin Krenn, Stefan Mangard
Implementation
The efficient verification of the security of masked hardware implementations is an important issue that hinders the development and deployment of randomness-efficient masking techniques. At EUROCRYPT 2018, Bloem et al. [6] introduced the first practical formal tool to prove the side-channel resilience of masked circuits in the probing model with glitches. Most recently Barthe et al.[2] introduced a more efficient formal tool that builds upon the findings of Bloem et al. for modeling the...
Key-Insulated and Privacy-Preserving Signature Scheme with Publicly Derived Public Key
Zhen Liu, Guomin Yang, Duncan S. Wong, Khoa Nguyen, Huaxiong Wang
Since the introduction of Bitcoin in 2008, cryptocurrency has been undergoing a quick and explosive development. At the same time, privacy protection, one of the key merits of cryptocurrency, has attracted much attention by the community.
A deterministic wallet algorithm and a stealth address algorithm have been widely adopted in the community, due to their virtues on functionality and privacy-protection, which come from a key derivation mechanism that an arbitrary number of derived keys can...
On the Security of the PKCS#1 v1.5 Signature Scheme
Tibor Jager, Saqib A. Kakvi, Alexander May
Foundations
The RSA PKCS#1 v1.5 signature algorithm is the most widely used digital signature scheme in practice. Its two main strengths are its extreme simplicity, which makes it very easy to implement, and that verification of signatures is significantly faster than for DSA or ECDSA. Despite the huge practical importance of RSA PKCS#1 v1.5 signatures, providing formal evidence for their security based on plausible cryptographic hardness assumptions has turned out to be very difficult. Therefore the...
Noise Explorer: Fully Automated Modeling and Verification for Arbitrary Noise Protocols
Nadim Kobeissi, Georgio Nicolas, Karthikeyan Bhargavan
Cryptographic protocols
The Noise Protocol Framework, introduced recently, allows for the design and construction of secure channel protocols by describing them through a simple, restricted language from which complex key derivation and local state transitions are automatically inferred. Noise "Handshake Patterns" can support mutual authentication, forward secrecy, zero round-trip encryption, identity hiding and other advanced features. Since the framework's release, Noise-based protocols have been adopted by...
Formal Analysis of Vote Privacy using Computationally Complete Symbolic Attacker
Gergei Bana, Rohit Chadha, Ajay Kumar Eeralla
Cryptographic protocols
We analyze the FOO electronic voting protocol in the provable secu- rity model using the technique of Computationally Complete Symbolic Attacker (CCSA). The protocol uses commitments, blind signatures and anonymous chan- nels to achieve vote privacy. Unlike the Dolev-Yao analyses of the protocol, we assume neither perfect cryptography nor existence of perfectly anonymous chan- nels. Our analysis reveals new attacks on vote privacy, including an attack that arises due to the inadequacy of the...
Verifiable Delay Functions
Dan Boneh, Joseph Bonneau, Benedikt Bünz, Ben Fisch
Cryptographic protocols
We study the problem of building a verifiable delay function (VDF). A VDF requires a specified number of sequential steps to evaluate, yet produces a unique output that can be efficiently and publicly verified. VDFs have many applications in decentralized systems, including public randomness beacons, leader election in consensus protocols, and proofs of replication. We formalize the requirements for VDFs and present new candidate constructions that are the first to achieve an exponential gap...
On the Security Properties of e-Voting Bulletin Boards
Aggelos Kiayias, Annabell Kuldmaa, Helger Lipmaa, Janno Siim, Thomas Zacharias
In state-of-the-art e-voting systems, a bulletin board (BB) is a critical component for preserving election integrity and availability. Although it is common in the literature to assume that a BB is a centralized entity that is trusted, in the recent works of Culnane and Schneider [CSF 2014] and Chondros et al. [ICDCS 2016], the importance of removing BB as a single point of failure has been extensively discussed.
Motivated by these works, we introduce a framework for the formal security...
Computer-aided proofs for multiparty computation with active security
Helene Haagh, Aleksandr Karbyshev, Sabine Oechsner, Bas Spitters, Pierre-Yves Strub
Cryptographic protocols
Secure multi-party computation (MPC) is a general cryptographic technique that allows distrusting parties to compute a function of their individual inputs, while only revealing the output of the function. It has found applications in areas such as auctioning, email filtering, and secure teleconference. Given their importance, it is crucial that the protocols are specified and implemented correctly. In the programming language community, it has become good practice to use computer proof...
Betrayal, Distrust, and Rationality: Smart Counter-Collusion Contracts for Verifiable Cloud Computing
Changyu Dong, Yilei Wang, Amjad Aldweesh, Patrick McCorry, Aad van Moorsel
Cloud computing has become an irreversible trend. Together comes the pressing need for verifiability, to assure the client the correctness of computation outsourced to the cloud. Existing verifiable computation techniques all have a high overhead, thus if being deployed in the clouds, would render cloud computing more expensive than the on-premises counterpart. To achieve verifiability at a reasonable cost, we leverage game theory and propose a smart contract based solution. In a nutshell, a...
Towards Tight Security of Cascaded LRW2
Bart Mennink
Secret-key cryptography
The Cascaded LRW2 tweakable block cipher was introduced by Landecker et al. at CRYPTO 2012, and proven secure up to $2^{2n/3}$ queries. There has not been any attack on the construction faster than the generic attack in $2^n$ queries. In this work we initiate the quest towards a tight bound. We first present a distinguishing attack in $2n^{1/2}2^{3n/4}$ queries against a generalized version of the scheme. The attack is supported with an experimental verification and a formal success...
Ledger Design Language: Towards Formal Reasoning and Implementation for Public Ledgers
Nadim Kobeissi, Natalia Kulatova
Implementation
Cryptocurrencies have popularized public ledgers, known colloquially as "blockchains". While the Bitcoin blockchain is relatively simple to reason about as, effectively, a hash chain, more complex public ledgers are largely designed without any formalization of desired cryptographic properties such as authentication or integrity. These designs are then implemented without assurances against real-world bugs leading to little assurance with regards to practical, real-world security.
Ledger...
Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, Bernardo Portela
We give a language-based security treatment of domain-specific
languages and compilers for secure multi-party computation, a
cryptographic paradigm that enables collaborative computation over
encrypted data. Computations are specified in a core imperative
language, as if they were intended to be executed by a trusted-third
party, and formally verified against an information-flow policy
modelling (an upper bound to) their leakage. This allows non-experts
to assess the impact of...
Secure Cloud Storage Scheme Based On Hybrid Cryptosystem
Atanu Basu, Indranil Sengupta
This paper presents a secure cloud storage scheme based on hybrid cryptosystem, which consists of Elliptic Curve Cryptography (ECC),
Advanced Encryption Standard (AES), and one-way hash function. Here, the data owner exports large volume of encrypted data to a cloud
storage provider. The exported encrypted data is over-encrypted by the cloud storage provider, and the data is sent to the requesting user. An existing hybrid cryptosystem based dynamic key management scheme with hierarchical...
Capsule: A Protocol for Secure Collaborative Document Editing
Nadim Kobeissi
Cryptographic protocols
Today's global society strongly relies on collaborative document editing, which plays an increasingly large role in sensitive workflows. While other collaborative venues, such as secure messaging, have seen secure protocols being standardized and widely implemented, the same cannot be said for collaborative document editing. Popular tools such as Google Docs, Microsoft Office365 and Etherpad are used to collaboratively write reports and other documents which are frequently sensitive and...
SoK: unraveling Bitcoin smart contracts
Nicola Atzei, Massimo Bartoletti, Tiziana Cimoli, Stefano Lande, Roberto Zunino
Cryptographic protocols
Albeit the primary usage of Bitcoin is to exchange currency, its blockchain and consensus mechanism can also be exploited to securely execute some forms of smart contracts. These are agreements among mutually distrusting parties, which can be automatically enforced without resorting to a trusted intermediary. Over the last few years a variety of smart contracts for Bitcoin have been proposed, both by the academic community and by that of developers. However, the heterogeneity in their...
Two-Factor Password-Authenticated Key Exchange with End-to-End Password Security
Stanislaw Jarecki, Mohammed Jubur, Hugo Krawczyk, Maliheh Shirvanian, Nitesh Saxena
Cryptographic protocols
We present a secure two-factor authentication (TFA) scheme based on the possession by the user of a password and a crypto-capable device. Security is ``end-to-end" in the sense that the attacker can attack all parts of the system, including all communication links and any subset of parties (servers, devices, client terminals), can learn users' passwords, and perform active and passive attacks, online and offline. In all cases the scheme provides the highest attainable security bounds given...
Verification of FPGA-augmented trusted computing mechanisms based on Applied Pi Calculus
Alessandro Cilardo, Andrea Primativo
Implementation
Trusted computing technologies may play a key role for cloud security as they enable users to relax the trustworthiness assumptions about the provider that operates the physical cloud infrastructure. This work focuses on the possibility of embodying Field-Programmable Gate Array (FPGA) devices in cloud-based infrastructures, where they can benefit compute-intensive workloads like data compression, machine learning, data encoding, etc. The focus is on the implications for cloud applications...
Provably secure compilation of side-channel countermeasures
Gilles Barthe, Benjamin Grégoire, Vincent Laporte
Implementation
Software-based countermeasures provide effective mitigation against side-channel attacks, often with minimal efficiency and deployment overheads. Their effectiveness is often amenable to rigorous analysis: specifically, several popular countermeasures can be formalized as information flow policies, and correct implementation of the countermeasures can be verified with state-of-the-art analysis and verification techniques. However, in absence of further justification, the guarantees only hold...
VerMI: Verification Tool for Masked Implementations
Victor Arribas, Svetla Nikova, Vincent Rijmen
Implementation
Masking is a widely used countermeasure against Side-Channel
Attacks (SCA), but the implementation of these countermeasures is challenging. Experimental security evaluation requires special equipment, a considerable amount of time and extensive technical knowledge. So, to automate and to speed up this process, a formal verification can be performed to asses the security of a design. Multiple theoretical approaches and verification tools have been proposed in the literature. The majority of...
Generic Low-Latency Masking in Hardware
Hannes Gross, Rinat Iusupov, Roderick Bloem
Implementation
In this work, we introduce a generalized concept for low-latency masking that is applicable to any implementation and protection order, and (in its most extreme form) does not require on-the-fly randomness. The main idea of our approach is to avoid collisions of shared variables in nonlinear circuit parts and to skip the share compression. We show the feasibility of our approach on a full implementation of a one-round unrolled Ascon variant and on an AES S-box case study. Additionally, we...
Formal Verification of Masked Hardware Implementations in the Presence of Glitches
Roderick Bloem, Hannes Gross, Rinat Iusupov, Bettina Könighofer, Stefan Mangard, Johannes Winter
Implementation
Masking provides a high level of resistance against side-channel analysis. However, in practice there are many possible pitfalls when masking schemes are applied, and implementation flaws are easily overlooked. Over the recent years, the formal verification of masked software implementations has made substantial progress. In contrast to software implementations, hardware implementations are inherently susceptible to glitches. Therefore, the same methods tailored for software implementations...
Formal Verification of Side-channel Countermeasures via Elementary Circuit Transformations
Jean-Sebastien Coron
Implementation
We describe a technique to formally verify the security of masked implementations against side-channel attacks, based on elementary circuit transforms. We describe two complementary approaches: a generic approach for the formal verification of any circuit, but for small attack orders only, and a specialized approach for the verification of specific circuits, but at any order. We also show how to generate security proofs automatically, for simple circuits. We describe the implementation of...
On the Untapped Potential of Encoding Predicates by Arithmetic Circuits and Their Applications
Shuichi Katsumata
Public-key cryptography
Predicates are used in cryptography as a fundamental tool to control the disclosure of secrets. However, how to embed a particular predicate into a cryptographic primitive is usually not given much attention. In this work, we formalize the idea of encoding predicates as arithmetic circuits and observe that choosing the right encoding of a predicate may lead to an improvement in many aspects such as the efficiency of a scheme or the required hardness assumption. In particular, we develop two...
Consensus from Signatures of Work
Juan A. Garay, Aggelos Kiayias, Giorgos Panagiotakos
Cryptographic protocols
Assuming the existence of a public-key infrastructure (PKI), digital signatures are a fundamental building block in the design of
secure consensus protocols
with optimal resilience.
More recently, with the advent of blockchain
protocols like Bitcoin, consensus has been considered in the ``permissionless''
setting where no authentication or even point-to-point communication is available.
Yet, despite some positive preliminary
results, there has been no attempt to formalize a
building block...
A Formal Foundation for Secure Remote Execution of Enclaves
Pramod Subramanyan, Rohit Sinha, Ilia Lebedev, Srinivas Devadas, Sanjit Seshia
Applications
Recent proposals for trusted hardware platforms, such as Intel SGX and the MIT Sanctum processor, offer compelling security features but lack formal guarantees. We introduce a verification methodology based on a trusted abstract platform (TAP) that formally models idealized enclaves and a parameterized adversary. We present machine-checked proofs showing that the TAP satisfies the three key security properties needed for secure remote execution: integrity, confidentiality and secure...
Snarky Signatures: \\ Minimal Signatures of Knowledge from Simulation-Extractable SNARKs
Jens Groth, Mary Maller
We construct a pairing-based simulation-extractable succinct non-interactive argument of knowledge (SE-SNARK) that consists of only 3 group elements and has highly efficient verification. By formally linking SE-SNARKs to signatures of knowledge, we then obtain a succinct signature of knowledge consisting of only 3 group elements.
SE-SNARKs enable a prover to give a proof that they know a witness to an instance in a manner which is: (1) \textit{succinct} - proofs are short and verifier...
HACL*: A Verified Modern Cryptographic Library
Jean Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche
Implementation
HACL* is a verified portable C cryptographic library that implements modern cryptographic primitives such as the ChaCha20 and Salsa20 encryption algorithms, Poly1305 and HMAC message authentication, SHA-256 and SHA-512 hash functions, the Curve25519 elliptic curve, and Ed25519 signatures.
HACL* is written in the F* programming language and then compiled to readable C code. The F* source code for each crypto- graphic primitive is verified for memory safety, mitigations against timing...
Message-Recovery MACs and Verification-Unskippable AE
Shoichi Hirose, Yu Sasaki, Kan Yasuda
Secret-key cryptography
This paper explores a new type of MACs called message-recovery MACs (MRMACs). MRMACs have an additional input $R$ that gets recovered upon verification.
Receivers must execute verification in order to recover $R$, making the verification process unskippable. Such a feature helps avoid mis-implementing verification algorithms.
The syntax and security notions of MRMACs are rigorously formulated. In particular, we formalize the notion of unskippability and present a construction of an...
Passphone: Outsourcing Phone-based Web Authentication while Protecting User Privacy
Martin Potthast, Christian Forler, Eik List, Stefan Lucks
Cryptographic protocols
This work introduces PassPhone, a new smartphone-based authentication scheme that outsources user verification to a trusted third party without sacrificing privacy: neither can the trusted third party learn the relation between users and service providers, nor can service providers learn those of their users to others. When employed as a second factor in conjunction with, for instance, passwords as a first factor, our scheme maximizes the deployability of two-factor authentication for...
Sharper Ring-LWE Signatures
Paulo S. L. M. Barreto, Patrick Longa, Michael Naehrig, Jefferson E. Ricardini, Gustavo Zanon
Public-key cryptography
We present Tesla# (pronounced "Tesla Sharp"), a digital signature scheme based on the RLWE assumption that continues a recent line of proposals of lattice-based digital signature schemes originating in work by Lyubashevsky as well as by Bai and Galbraith. It improves upon all of its predecessors in that it attains much faster key pair generation, signing, and verification, outperforming most (conventional or lattice-based) signature schemes on modern processors.
We propose a selection of...
Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model
Gilles Barthe, François Dupressoir, Sebastian Faust, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub
In this paper, we provide a necessary clarification of the good security properties that can be obtained from parallel implementations of masking schemes. For this purpose, we first argue that (i) the probing model is not straightforward to interpret, since it more naturally captures the intuitions of serial implementations, and (ii) the noisy leakage model is not always convenient, e.g. when combined with formal methods for the verification of cryptographic implementations. Therefore we...
Survey of Approaches and Techniques for Security Verification of Computer Systems
Ferhat Erata, Shuwen Deng, Faisal Zaghloul, Wenjie Xiong, Onur Demir, Jakub Szefer
Implementation
This paper surveys the landscape of security verification approaches and techniques for computer systems at various levels: from a software-application level all the way to the physical hardware level. Different existing projects are compared, based on the tools used and security aspects being examined. Since many systems require both hardware and software components to work together to provide the system's promised security protections, it is not sufficient to verify just the software...
When Are Three Voters Enough for Privacy Properties?
Myrto Arapinis, Véronique Cortier, Steve Kremer
Cryptographic protocols
Protocols for secure electronic voting are of increasing societal importance. Proving rigorously their security is more challenging than many other protocols, which aim at authentication or key exchange. One of the reasons is that they need to be secure for an arbitrary number of malicious voters. In this paper we identify a class of voting protocols for which only a small number of agents needs to be considered: if there is an attack on vote privacy then there is also an attack that...
Antikernel: A Decentralized Secure Hardware-Software Operating System Architecture
Andrew D. Zonenberg, Bulent Yener
The ``kernel" model has been part of operating system architecture for decades, but upon closer inspection it clearly violates the principle of least required privilege. The kernel is a single entity which provides many services (memory management, interfacing to drivers, context switching, IPC) which have no real relation to each other, and has the ability to observe or tamper with all state of the system. This work presents Antikernel, a novel operating system architecture consisting of...
Programmable Hash Functions from Lattices: Short Signatures and IBEs with Small Key Sizes
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 two types of 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 collision-resistant, which gives a direct application of this new primitive. We...
-
« Previous
-
1
- 2
- 3
-
Next »
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...
We introduce the Clockwork Finance Framework (CFF), a general purpose, formal verification framework for mechanized reasoning about the economic security properties of composed decentralized-finance (DeFi) smart contracts. CFF features three key properties. It is contract complete, meaning that it can model any smart contract platform and all its contracts—Turing complete or otherwise. It does so with asymptotically constant model overhead. It is also attack-exhaustive by construction,...
Physical side-channel attacks like power analysis pose a serious threat to cryptographic devices in real-world applications. Consequently, devices implement algorithmic countermeasures like masking. In the past, works on the design and verification of masked software implementations have mostly focused on simple microprocessors that find usage on smart cards. However, many other applications such as in the automotive industry require side-channel protected cryptographic computations on much...
Payment is an essential part of e-commerce. Merchants usually rely on third-parties, so-called payment processors, who take care of transferring the payment from the customer to the merchant. How a payment processor interacts with the customer and the merchant varies a lot. Each payment processor typically invents its own protocol that has to be integrated into the merchant’s application and provides the user with a new, potentially unknown and confusing user experience. Pushed by major...
Fault Injection Analysis is seen as a powerful attack against implementations of cryptographic algorithms. Over the last two decades, researchers proposed a plethora of countermeasures to secure such implementations. However, the design process and implementation are still error-prone, complex, and manual tasks which require long-standing experience in hardware design and physical security. Moreover, the validation of the claimed security is often only done by empirical testing in a very...
Stake-based multiparty cryptographic primitives operate in a setting where participants are associated with their stake, security is argued against an adversary that is bounded by the total stake it possesses —as opposed to number of parties— and we are interested in scalability, i.e., the complexity of critical operations depends only logarithmically in the number of participants (who are assumed to be numerous). In this work we put forth a new stake-based primitive, stake-based...
Digital signatures are widely deployed to authenticate the source of incoming information, or to certify data integrity. Common signature verification procedures return a decision (accept/reject) only at the very end of the execution. If interrupted prematurely, however, the verification process cannot infer any meaningful information about the validity of the given signature. We notice that this limitation is due to the algorithm design solely, and it is not inherent to signature...
We present probabilistic dynamic I/O automata, a framework to model dynamic probabilistic systems. Our work extends dynamic I/O Automata formalism of Attie & Lynch to probabilistic setting. The original dynamic I/O Automata formalism included operators for parallel composition, action hiding, action renaming, automaton creation, and behavioral sub-typing by means of trace inclusion. They can model mobility by using signature modification. They are also hierarchical: a dynamically changing...
The security of modern cryptography depends on multiple factors, from sound hardness assumptions to correct implementations that resist side-channel cryptanalysis. Curve-based cryptography is not different in this regard, and substantial progress in the last few decades has been achieved in both selecting parameters and devising secure implementation strategies. In this context, the security of implementations of field inversion is sometimes overlooked in the research literature, because ...
We formally prove that the C implementation of the X25519 key-exchange protocol in the TweetNaCl library is correct. We prove both that it correctly implements the protocol from Bernstein's 2006 paper, as standardized in RFC 7748, as well as the absence of undefined behavior like arithmetic overflows and array out-of-bounds errors. We also formally prove, based on the work of Bartzia and Strub, that X25519 is mathematically correct, i.e., that it correctly computes scalar multiplication on...
Code that is highly optimized poses a problem for program-level verification: programmers can employ various clever tricks that are non-trivial to reason about. For cryptography on low-power devices, it is nonetheless crucial that implementations be functionally correct, secure, and efficient. These are usually crafted in hand-optimized machine code that eschew conventional control flow as much as possible. We have formally verified such code: a library which implements elliptic curve...
Side-channel attacks are a threat to secrets stored on a device, especially if an adversary has physical access to the device. As an effect of this, countermeasures against such attacks for cryptographic algorithms are a well-researched topic. In this work, we deviate from the study of cryptographic algorithms and instead focus on the side-channel protection of a much more basic operation, the comparison of a known attacker-controlled value with a secret one. Comparisons sensitive to...
State-separating proofs (SSP) is a recent methodology for structuring game-based cryptographic proofs in a modular way, by using algebraic laws to exploit the modular structure of composed protocols. While promising, this methodology was previously not fully formalized and came with little tool support. We address this by introducing SSProve, the first general verification framework for machine-checked state-separating proofs. SSProve combines high-level modular proofs about composed...
We propose Veksel, a simple generic paradigm for constructing efficient non-interactive coin mixes. The central component in our work is a concretely efficient proof $\pi_{one-many}$ that a homomorphic commitment $c^*$ is a rerandomization of a commitment $c \in \{c_1, \ldots, c_\ell \}$ without revealing $c$. We formalize anonymous account-based cryptocurrency as a universal composability functionality and show how to efficiently instantiate the functionality using $\pi_{one-many}$ in a...
In this paper, we compare several non-tight degree evaluation methods i.e., Boura and Canteaut's formula, Carlet's formula as well as Liu's numeric mapping and division property proposed by Todo, and hope to find the best one from these methods for practical applications. Specifically, for the substitution-permutation-network (SPN) ciphers, we first deeply explore the relationships between division property of an Sbox and its algebraic properties (e.g., the algebraic degree of its inverse)....
EasyCrypt is a proof assistant used for verifying computational security proofs of cryptographic constructions. It has been applied to several prominent examples, including the SHA3 standard and a critical component of AWS Key Management Services. In this paper we enhance the EasyCrypt proof assistant to reason about computational complexity of adversaries. The key technical tool is a Hoare logic for reasoning about computational complexity (execution time and oracle calls) of adversarial...
Although there have been many successes in verifying proofs of non-interactive cryptographic primitives such as encryption and signatures, formal verification of interactive cryptographic protocols is still a nascent area. While in principle, it seems possible to extend general frameworks such as Easycrypt to encode proofs for more complex, interactive protocols, a big challenge is whether the human effort would be scalable enough for proof mechanization to eventually acquire mainstream...
The typical login protocol for authenticating a user to a web service involves the client sending a password over a TLS-secured channel to the service, occasionally deployed with the password being prehashed. This widely-deployed paradigm, while simple in nature, is prone to both inadvertent logging and eavesdropping attacks, and has repeatedly led to the exposure of passwords in plaintext. Partly to address this problem, symmetric and asymmetric PAKE protocols were developed to ensure that...
The Hybrid Public Key Encryption (HPKE) scheme is an emerging standard currently under consideration by the Crypto Forum Research Group (CFRG) of the IETF as a candidate for formal approval. Of the four modes of HPKE, we analyse the authenticated mode HPKE_Auth in its single-shot encryption form as it contains what is, arguably, the most novel part of HPKE and has applications to other upcoming standards such as MLS. HPKE_Auth’s intended application domain is captured by a new primitive...
ElectionGuard is an open source set of software components and specifications from Microsoft designed to allow the modification of a number of different e-voting protocols and products to produce public evidence (transcripts) which anyone can verify. The software uses ElGamal, homomorphic tallying and sigma protocols to enable public scrutiny without adversely affecting privacy. Some components have been formally verified (machine-checked) to be free of certain software bugs but there was no...
We introduce Vetted Encryption (VE), a novel cryptographic primitive, which addresses the following scenario: a receiver controls, or vets, who can send them encrypted messages. We model this as a filter publicly checking ciphertext validity, where the overhead does not grow with the number of senders. The filter receives one public key for verification, and every user receives one personal encryption key. We present three versions: Anonymous, Identifiable, and Opaque VE (AVE, IVE and OVE),...
Adaptor signatures (AS) are an extension of digital signatures that enable the encoding of a cryptographic hard problem (e.g., discrete logarithm) within the signature itself. An AS scheme ensures that (i) the signature can be created only by the user knowing the solution to the cryptographic problem; (ii) the signature reveals the solution itself; (iii) the signature can be verified with the standard verification algorithm. These properties have made AS a salient building block for many...
The protection of cryptographic implementations against power analysis attacks is of critical importance for many applications in embedded systems. The typical approach of protecting against these attacks is to implement algorithmic countermeasures, like masking. However, implementing these countermeasures in a secure and correct manner is challenging. Masking schemes require the independent processing of secret shares, which is a property that is often violated by CPU microarchitectures in...
This paper analyses security of concrete instantiations of EdDSA by identifying exploitable inconsistencies between standardization recommendations and Ed25519 implementations. We mainly focus on current ambiguity regarding signature verification equations, binding and malleability guarantees, and incompatibilities between randomized batch and single verification. We give a formulation of Ed25519 signature scheme that achieves the highest level of security, explaining how each step of the...
Election verifiability aims to ensure that the outcome produced by electronic voting systems correctly reflects the intentions of eligible voters, even in the presence of an adversary that may corrupt various parts of the voting infrastructure. Protecting such systems from manipulation is challenging because of their distributed nature involving voters, election authorities, voting servers and voting platforms. An adversary corrupting any of these can make changes that, individually, would...
We present a computer-verified formalization of the post-quantum security proof of the Fujisaki-Okamoto transform (as analyzed by Hövelmanns, Kiltz, Schäge, and Unruh, PKC 2020). The formalization is done in quantum relational Hoare logic and checked in the qrhl-tool (Unruh, POPL 2019).
A high-quality outsourced storage service is crucial for many existing applications. For example, hospitals and data centers need to guarantee the availability of their systems to perform routine daily activities. Such a system should protect users against downtime and ensure data availability over time. Continuous data availability is a critical property to measure the quality of an outsourced storage service, which implies that outsourced data is continuously available to the server...
The masking countermeasure is among the most powerful countermeasures to counteract side-channel attacks. Leakage models have been exhibited to theoretically reason on the security of such masked implementations. So far, the most widely used leakage model is the probing model defined by Ishai, Sahai, and Wagner at (CRYPTO 2003). While it is advantageously convenient for security proofs, it does not capture an adversary exploiting full leakage traces as, e.g., in horizontal attacks. Those...
Lightweight authenticated key exchange (AKE) protocols based on symmetric-key cryptography are important in securing the Internet of Things (IoT). However, achieving perfect forward secrecy (PFS) is not trivial for AKE based on symmetric-key cryptography, as opposed to AKE based on public-key cryptography. The most recent proposals that provide PFS are SAKE and SAKE-AM. In this paper, we first take a closer look at these protocols and observe that they have some limitations, specially when...
Implementing cryptographic functions securely in the presence of physical adversaries is still a challenge although a lion's share of research in the physical security domain has been put in development of countermeasures. Among several protection schemes, masking has absorbed the most attention of research in both academic and industrial communities, due to its theoretical foundation allowing to provide proofs or model the achieved security level. In return, masking schemes are difficult to...
We propose a new approach for building efficient, provably secure, and practically hardened implementations of masked algorithms. Our approach is based on a Domain Specific Language in which users can write efficient assembly implementations and fine-grained leakage models. The latter are then used as a basis for formal verification, allowing for the first time formal guarantees for a broad range of device-specific leakage effects not addressed by prior work. The practical benefits of our...
We present a new methodology for building formally verified cryptographic libraries that are optimized for multiple architectures. In particular, we show how to write and verify generic crypto code in the F* programming language that exploits single-instruction multiple data (SIMD) parallelism. We show how this code can be compiled to platforms that supports vector instructions, including ARM Neon and Intel AVX, AVX2, and AVX512. We apply our methodology to obtain verified vectorized...
An aggregatable subvector commitment (aSVC) scheme is a vector commitment (VC) scheme that can aggregate multiple proofs into a single, small subvector proof. In this paper, we formalize aSVCs and give a construction from constant-sized polynomial commitments. Our construction is unique in that it has linear-sized public parameters, it can compute all constant-sized proofs in quasilinear time, it updates proofs in constant time and it can aggregate multiple proofs into a constant-sized...
Cryptographic implementations deployed in real world devices often aim at (provable) security against the powerful class of side-channel attacks while keeping reasonable performances. Last year at Asiacrypt, a new formal verification tool named tightPROVE was put forward to exactly determine whether a masked implementation is secure in the well-deployed probing security model for any given security order t. Also recently, a compiler named Usuba was proposed to automatically generate...
Hybrid Public Key Encryption (HPKE) is a cryptographic primitive being standardized by the Crypto Forum Research Group (CFRG) within the Internet Research Task Force (IRTF). HPKE schemes combine asymmetric and symmetric cryptographic primitives for efficient authenticated encryption of arbitrary-sized plaintexts under a given recipient public key. This document presents a mechanized cryptographic analysis done with CryptoVerif, of all four HPKE modes, instantiated with a prime-order-group...
Mix nets are often used to provide privacy in modern security protocols, through shuffling. Some of the most important applications, such as secure electronic voting, require mix nets that are verifiable. In the literature, numerous techniques have been proposed to make mix nets verifiable. Some of them have also been employed for securing real political elections. With the looming possibility of quantum computers and their threat to cryptosystems based on classical hardness assumptions,...
We suggests a relaxed freshness paradigm for challenge-response authentication for each field of application where challenger and responder are tightly coupled and authentication takes place in a friendly environment. Replay attacks are not feasible under this premise, and freshness can be relaxed to relative freshness: no refresh is required as long as all previously tested responders were authentic. One field of application is anti-counterfeiting of electronic device components. The main...
Recently, Srinath and Chandrasekaran have proposed an undeniable blind signature scheme (UBSS) from supersingular isogeny to provide signer’s control in a quantum-resistant blind signature. However, certain weaknesses of undeniable signature have already been observed and have been overcome by formalizing the designated verifier signature (DVS). In this paper, we explore the possibility of generic construction of a DVS from hard homogeneous spaces. Further, following this...
While there have been many successes in verifying cryptographic security proofs of noninter- active primitives such as encryption and signatures, less attention has been paid to interactive cryptographic protocols. Interactive protocols introduce the additional verification challenge of concurrency, which is notoriously hard to reason about in a cryptographically sound manner. When proving the (approximate) observational equivalance of protocols, as is required by simulation based security...
Computer-aided cryptography is an active area of research that develops and applies formal, machine-checkable approaches to the design, analysis, and implementation of cryptography. We present a cross-cutting systematization of the computer-aided cryptography literature, focusing on three main areas: (i) design-level security (both symbolic security and computational security), (ii) functional correctness and efficiency, and (iii) implementation-level security (with a focus on digital...
Using a set of pairing product equations (PPEs) to verify the correctness of an untrusted set of pairing elements with respect to another set of trusted elements has numerous cryptographic applications. These include the design of basic and structure-preserving signature schemes, building oblivious transfer schemes from “blind” IBE, finding new verifiable random functions and keeping the IBE/ABE authority “accountable” to the user. A natural question to ask is: are all trusted-untrusted...
The disruptive blockchain technology is expected to have broad applications in many areas due to its advantages of transparency, fault tolerance, and decentralization, but the open nature of blockchain also introduces severe privacy issues. Since anyone can deduce private information about relevant accounts, different privacy-preserving techniques have been proposed for cryptocurrencies under the UTXO model, e.g., Zerocash and Monero. However, it is more challenging to protect privacy for...
Authenticated encryption schemes are usually expected to offer confidentiality and authenticity. In case of release of unverified plaintext (RUP), an adversary gets separated access to the decryption and verification functionality, and has more power in breaking the scheme. Andreeva et al. (ASIACRYPT 2014) formalized RUP security using plaintext awareness, informally meaning that the decryption functionality gives no extra power in breaking confidentiality, and INT-RUP security, covering...
In invitation-based systems, a new user can register upon having a threshold number of invitations issued by the existing members. The newcomer hands his invitations to the system administrator who verifies whether the invitations are issued by legitimate members. This causes the administrator to be aware of who is invited by whom. However, the inviter-invitee relationship is privacy-sensitive information and can lead to inference attacks where the invitee's profile (e.g., political view or...
Off-the-Record (OTR) messaging is a two-party message authentication protocol that also provides plausible deniability: there is no record that can later convince a third party what messages were actually sent. To extend OTR to group messaging we need to consider issues that are not present in the 2-party case. In group OTR (as in two-party OTR), the sender should be able to authenticate (or sign) his messages so that group members can verify who sent a message (that is, signatures should be...
Proof-of-burn has been used as a mechanism to destroy cryptocurrency in a verifiable manner. Despite its well known use, the mechanism has not been previously formally studied as a primitive. In this paper, we put forth the first cryptographic definition of what a proof-of-burn protocol is. It consists of two functions: First, a function which generates a cryptocurrency address. When a user sends money to this address, the money is irrevocably destroyed. Second, a verification function...
Vehicular Ad-hoc Networks (VANETs) are a cardinal part of intelligent transportation system (ITS) which render various services in terms of traffic and transport management. The VANET is used to manage growing traffic and manage data about traffic conditions, weather, road conditions, speed of the vehicle, etc. Even though, VANETs are self-sufficient and effective networks but they still suffer from various security and privacy issues. VANETs need to ensure that an adversary should not be...
Card-based cryptography provides simple and practicable protocols for performing secure multi-party computation (MPC) with just a deck of cards. For the sake of simplicity, this is often done using cards with only two symbols, e.g., clubs and hearts. Within this paper, we target the setting where all cards carry distinct symbols, catering for use-cases with commonly available standard decks and a weaker indistinguishability assumption. As of yet, the literature provides for only three...
Verifpal is a new automated modeling framework and verifier for cryptographic protocols, optimized with heuristics for common-case protocol specifications, that aims to work better for real-world practitioners, students and engineers without sacrificing comprehensive formal verification features. In order to achieve this, Verifpal introduces a new, intuitive language for modeling protocols that is easier to write and understand than the languages employed by existing tools. Its formal...
Proof-of-stake (PoS) blockchain protocols are emerging as one of the most promising alternative to the energy-consuming proof-of-work protocols. However, one particularly critical threat in the PoS setting is the well-known long-range attacks caused by secret key leakage (LRSL attack). Specifically, an adversary can attempt to corrupt the secret keys corresponding to accounts possessing substantial stake at some past moment such that double-spend or erase past transactions, violating the...
Timing side-channels are arguably one of the main sources of vulnerabilities in cryptographic implementations. One effective mitigation against timing side-channels is to write programs that do not perform secret-dependent branches and memory accesses. This mitigation, known as ''cryptographic constant-time'', is adopted by several popular cryptographic libraries. This paper focuses on compilation of cryptographic constant-time programs, and more specifically on the following question: is...
EMV, also known as Chip and PIN, is the world-wide standard for card-based electronic payment. Its security wavers: over the past years, researchers have demonstrated various practical attacks, ranging from using stolen cards by disabling PIN verification to cloning cards by pre-computing transaction data. Most of these attacks rely on violating certain unjustified and not explicitly stated core assumptions upon which EMV is built, namely that the input device (e.g. the ATM) is trusted and...
This work presents Arcula, a new design for hierarchical deterministic wallets that brings identity-based addresses to the blockchain. Arcula is built on top of provably secure cryptographic primitives. It generates all its cryptographic secrets from a user-provided seed and enables the derivation of new public keys based on the identities of users, without requiring any secret information. Unlike other wallets, it achieves all these properties while being secure against privilege...
Boneh, Bonneau, Bünz, and Fisch (CRYPTO 2018) recently introduced the notion of a verifiable delay function (VDF). VDFs are functions that take a long sequential time $T$ to compute, but whose outputs $y = \mathsf{Eval}(x)$ can be efficiently verified (possibly given a proof $\pi$) in time $t \ll T$ (e.g., $t=\mathrm{poly}(\lambda, \log T)$ where $\lambda$ is the security parameter). The first security requirement on a VDF, called uniqueness, is that no polynomial-time algorithm can find a...
We present a methodology for using the EasyCrypt proof assistant (originally designed for mechanizing the generation of proofs of game-based security of cryptographic schemes and protocols) to mechanize proofs of security of cryptographic protocols within the universally composable (UC) security framework. This allows, for the first time, the mechanization and formal verification of the entire sequence of steps needed for proving simulation-based security in a modular way: * Specifying a...
An important primitive in ensuring security of modern systems-on-chip designs are protocols for authenticated firmware load. These loaders read a firmware binary image from an untrusted input device, authenticate the image using cryptography and load the image into memory for execution if authentication succeeds. While these protocols are an essential part of the hardware root of trust in almost all modern computing devices, verification techniques for reasoning about end-to-end security of...
After suffering decades of high-profile attacks, the need for formal verification of security-critical software has never been clearer. Verification-oriented programming languages like F* are now being used to build high-assurance cryptographic libraries and implementations of standard protocols like TLS. In this paper, we seek to apply these verification techniques to modern Web applications, like WhatsApp, that embed sophisticated custom cryptographic components. The problem is that these...
Diffie-Hellman groups are a widely used component in cryptographic protocols in which a shared secret is needed. These protocols are typically proven to be secure under the assumption they are implemented with prime order Diffie Hellman groups. However, in practice, many implementations either choose to use non-prime order groups for reasons of efficiency, or can be manipulated into operating in non-prime order groups. This leaves a gap between the proofs of protocol security, which assume...
Decentralised ledgers are a prime application case for consensus protocols. Changing sets of validators have to agree on a set of transactions in an asynchronous network and in the presence of Byzantine behaviour. Major research efforts focus on creating consensus protocols under such conditions, with proof-of-stake (PoS) representing a promising candidate. PoS aims to reduce the waste of energy inherent to proof-of-work (PoW) consensus protocols. However, a significant challenge is to get...
Email breaches are commonplace, and they expose a wealth of personal, business, and political data whose release may have devastating consequences. Such damage is compounded by email’s strong attributability: today, any attacker who gains access to your email can easily prove to others that the stolen messages are authentic, a property arising from a necessary anti-spam/anti-spoofing protocol called DKIM. This greatly increases attackers’ capacity to do harm by selling the stolen information...
For cryptocurrency payments to be truly private, transactions have to have two properties: confidentiality, i.e., hiding the transferred amounts, and anonymity, i.e. hiding the identities of the sender and/or receiver in a transaction. In this paper, we propose Lelantus, a new decentralized anonymous payment (DAP) protocol that ensures confidential and anonymous blockchain transactions with small transaction sizes, short verification times, and without requiring a trusted setup. It...
Transient execution attacks like Spectre, Meltdown and Foreshadow have shown that combinations of microarchitectural side-channels can be synergistically exploited to create side-channel leaks that are greater than the sum of their parts. While both hardware and software mitigations have been proposed against these attacks, provable security has remained elusive. This paper introduces a formal methodology for enabling secure speculative execution on modern processors. We propose a new class...
Recently, the worldwide-used EMVCo standard for electronic payments included the “EMV RRP (Europay Mastercard Visa Relay-Resistant Protocol)” protocol. This uses distance bounding to counteract relay attacks in contactless payments. Last year, EMV RRP was widely analysed by symbolic verification methods, with several distance-bounding attacks and fixes proposed. Yet, one version of EMV RRP was found secure by all such formal analyses. Contrary to this, we exhibit an attack on this version of...
During the last decade, the blockchain space has exploded with a plethora of new cryptocurrencies, covering a wide array of different features, performance and security characteristics. Nevertheless, each of these coins functions in a stand-alone manner, independently. Sidechains have been envisioned as a mechanism to allow blockchains to communicate with one another and, among other applications, allow the transfer of value from one chain to another, but so far there have been no...
The efficient verification of the security of masked hardware implementations is an important issue that hinders the development and deployment of randomness-efficient masking techniques. At EUROCRYPT 2018, Bloem et al. [6] introduced the first practical formal tool to prove the side-channel resilience of masked circuits in the probing model with glitches. Most recently Barthe et al.[2] introduced a more efficient formal tool that builds upon the findings of Bloem et al. for modeling the...
Since the introduction of Bitcoin in 2008, cryptocurrency has been undergoing a quick and explosive development. At the same time, privacy protection, one of the key merits of cryptocurrency, has attracted much attention by the community. A deterministic wallet algorithm and a stealth address algorithm have been widely adopted in the community, due to their virtues on functionality and privacy-protection, which come from a key derivation mechanism that an arbitrary number of derived keys can...
The RSA PKCS#1 v1.5 signature algorithm is the most widely used digital signature scheme in practice. Its two main strengths are its extreme simplicity, which makes it very easy to implement, and that verification of signatures is significantly faster than for DSA or ECDSA. Despite the huge practical importance of RSA PKCS#1 v1.5 signatures, providing formal evidence for their security based on plausible cryptographic hardness assumptions has turned out to be very difficult. Therefore the...
The Noise Protocol Framework, introduced recently, allows for the design and construction of secure channel protocols by describing them through a simple, restricted language from which complex key derivation and local state transitions are automatically inferred. Noise "Handshake Patterns" can support mutual authentication, forward secrecy, zero round-trip encryption, identity hiding and other advanced features. Since the framework's release, Noise-based protocols have been adopted by...
We analyze the FOO electronic voting protocol in the provable secu- rity model using the technique of Computationally Complete Symbolic Attacker (CCSA). The protocol uses commitments, blind signatures and anonymous chan- nels to achieve vote privacy. Unlike the Dolev-Yao analyses of the protocol, we assume neither perfect cryptography nor existence of perfectly anonymous chan- nels. Our analysis reveals new attacks on vote privacy, including an attack that arises due to the inadequacy of the...
We study the problem of building a verifiable delay function (VDF). A VDF requires a specified number of sequential steps to evaluate, yet produces a unique output that can be efficiently and publicly verified. VDFs have many applications in decentralized systems, including public randomness beacons, leader election in consensus protocols, and proofs of replication. We formalize the requirements for VDFs and present new candidate constructions that are the first to achieve an exponential gap...
In state-of-the-art e-voting systems, a bulletin board (BB) is a critical component for preserving election integrity and availability. Although it is common in the literature to assume that a BB is a centralized entity that is trusted, in the recent works of Culnane and Schneider [CSF 2014] and Chondros et al. [ICDCS 2016], the importance of removing BB as a single point of failure has been extensively discussed. Motivated by these works, we introduce a framework for the formal security...
Secure multi-party computation (MPC) is a general cryptographic technique that allows distrusting parties to compute a function of their individual inputs, while only revealing the output of the function. It has found applications in areas such as auctioning, email filtering, and secure teleconference. Given their importance, it is crucial that the protocols are specified and implemented correctly. In the programming language community, it has become good practice to use computer proof...
Cloud computing has become an irreversible trend. Together comes the pressing need for verifiability, to assure the client the correctness of computation outsourced to the cloud. Existing verifiable computation techniques all have a high overhead, thus if being deployed in the clouds, would render cloud computing more expensive than the on-premises counterpart. To achieve verifiability at a reasonable cost, we leverage game theory and propose a smart contract based solution. In a nutshell, a...
The Cascaded LRW2 tweakable block cipher was introduced by Landecker et al. at CRYPTO 2012, and proven secure up to $2^{2n/3}$ queries. There has not been any attack on the construction faster than the generic attack in $2^n$ queries. In this work we initiate the quest towards a tight bound. We first present a distinguishing attack in $2n^{1/2}2^{3n/4}$ queries against a generalized version of the scheme. The attack is supported with an experimental verification and a formal success...
Cryptocurrencies have popularized public ledgers, known colloquially as "blockchains". While the Bitcoin blockchain is relatively simple to reason about as, effectively, a hash chain, more complex public ledgers are largely designed without any formalization of desired cryptographic properties such as authentication or integrity. These designs are then implemented without assurances against real-world bugs leading to little assurance with regards to practical, real-world security. Ledger...
We give a language-based security treatment of domain-specific languages and compilers for secure multi-party computation, a cryptographic paradigm that enables collaborative computation over encrypted data. Computations are specified in a core imperative language, as if they were intended to be executed by a trusted-third party, and formally verified against an information-flow policy modelling (an upper bound to) their leakage. This allows non-experts to assess the impact of...
This paper presents a secure cloud storage scheme based on hybrid cryptosystem, which consists of Elliptic Curve Cryptography (ECC), Advanced Encryption Standard (AES), and one-way hash function. Here, the data owner exports large volume of encrypted data to a cloud storage provider. The exported encrypted data is over-encrypted by the cloud storage provider, and the data is sent to the requesting user. An existing hybrid cryptosystem based dynamic key management scheme with hierarchical...
Today's global society strongly relies on collaborative document editing, which plays an increasingly large role in sensitive workflows. While other collaborative venues, such as secure messaging, have seen secure protocols being standardized and widely implemented, the same cannot be said for collaborative document editing. Popular tools such as Google Docs, Microsoft Office365 and Etherpad are used to collaboratively write reports and other documents which are frequently sensitive and...
Albeit the primary usage of Bitcoin is to exchange currency, its blockchain and consensus mechanism can also be exploited to securely execute some forms of smart contracts. These are agreements among mutually distrusting parties, which can be automatically enforced without resorting to a trusted intermediary. Over the last few years a variety of smart contracts for Bitcoin have been proposed, both by the academic community and by that of developers. However, the heterogeneity in their...
We present a secure two-factor authentication (TFA) scheme based on the possession by the user of a password and a crypto-capable device. Security is ``end-to-end" in the sense that the attacker can attack all parts of the system, including all communication links and any subset of parties (servers, devices, client terminals), can learn users' passwords, and perform active and passive attacks, online and offline. In all cases the scheme provides the highest attainable security bounds given...
Trusted computing technologies may play a key role for cloud security as they enable users to relax the trustworthiness assumptions about the provider that operates the physical cloud infrastructure. This work focuses on the possibility of embodying Field-Programmable Gate Array (FPGA) devices in cloud-based infrastructures, where they can benefit compute-intensive workloads like data compression, machine learning, data encoding, etc. The focus is on the implications for cloud applications...
Software-based countermeasures provide effective mitigation against side-channel attacks, often with minimal efficiency and deployment overheads. Their effectiveness is often amenable to rigorous analysis: specifically, several popular countermeasures can be formalized as information flow policies, and correct implementation of the countermeasures can be verified with state-of-the-art analysis and verification techniques. However, in absence of further justification, the guarantees only hold...
Masking is a widely used countermeasure against Side-Channel Attacks (SCA), but the implementation of these countermeasures is challenging. Experimental security evaluation requires special equipment, a considerable amount of time and extensive technical knowledge. So, to automate and to speed up this process, a formal verification can be performed to asses the security of a design. Multiple theoretical approaches and verification tools have been proposed in the literature. The majority of...
In this work, we introduce a generalized concept for low-latency masking that is applicable to any implementation and protection order, and (in its most extreme form) does not require on-the-fly randomness. The main idea of our approach is to avoid collisions of shared variables in nonlinear circuit parts and to skip the share compression. We show the feasibility of our approach on a full implementation of a one-round unrolled Ascon variant and on an AES S-box case study. Additionally, we...
Masking provides a high level of resistance against side-channel analysis. However, in practice there are many possible pitfalls when masking schemes are applied, and implementation flaws are easily overlooked. Over the recent years, the formal verification of masked software implementations has made substantial progress. In contrast to software implementations, hardware implementations are inherently susceptible to glitches. Therefore, the same methods tailored for software implementations...
We describe a technique to formally verify the security of masked implementations against side-channel attacks, based on elementary circuit transforms. We describe two complementary approaches: a generic approach for the formal verification of any circuit, but for small attack orders only, and a specialized approach for the verification of specific circuits, but at any order. We also show how to generate security proofs automatically, for simple circuits. We describe the implementation of...
Predicates are used in cryptography as a fundamental tool to control the disclosure of secrets. However, how to embed a particular predicate into a cryptographic primitive is usually not given much attention. In this work, we formalize the idea of encoding predicates as arithmetic circuits and observe that choosing the right encoding of a predicate may lead to an improvement in many aspects such as the efficiency of a scheme or the required hardness assumption. In particular, we develop two...
Assuming the existence of a public-key infrastructure (PKI), digital signatures are a fundamental building block in the design of secure consensus protocols with optimal resilience. More recently, with the advent of blockchain protocols like Bitcoin, consensus has been considered in the ``permissionless'' setting where no authentication or even point-to-point communication is available. Yet, despite some positive preliminary results, there has been no attempt to formalize a building block...
Recent proposals for trusted hardware platforms, such as Intel SGX and the MIT Sanctum processor, offer compelling security features but lack formal guarantees. We introduce a verification methodology based on a trusted abstract platform (TAP) that formally models idealized enclaves and a parameterized adversary. We present machine-checked proofs showing that the TAP satisfies the three key security properties needed for secure remote execution: integrity, confidentiality and secure...
We construct a pairing-based simulation-extractable succinct non-interactive argument of knowledge (SE-SNARK) that consists of only 3 group elements and has highly efficient verification. By formally linking SE-SNARKs to signatures of knowledge, we then obtain a succinct signature of knowledge consisting of only 3 group elements. SE-SNARKs enable a prover to give a proof that they know a witness to an instance in a manner which is: (1) \textit{succinct} - proofs are short and verifier...
HACL* is a verified portable C cryptographic library that implements modern cryptographic primitives such as the ChaCha20 and Salsa20 encryption algorithms, Poly1305 and HMAC message authentication, SHA-256 and SHA-512 hash functions, the Curve25519 elliptic curve, and Ed25519 signatures. HACL* is written in the F* programming language and then compiled to readable C code. The F* source code for each crypto- graphic primitive is verified for memory safety, mitigations against timing...
This paper explores a new type of MACs called message-recovery MACs (MRMACs). MRMACs have an additional input $R$ that gets recovered upon verification. Receivers must execute verification in order to recover $R$, making the verification process unskippable. Such a feature helps avoid mis-implementing verification algorithms. The syntax and security notions of MRMACs are rigorously formulated. In particular, we formalize the notion of unskippability and present a construction of an...
This work introduces PassPhone, a new smartphone-based authentication scheme that outsources user verification to a trusted third party without sacrificing privacy: neither can the trusted third party learn the relation between users and service providers, nor can service providers learn those of their users to others. When employed as a second factor in conjunction with, for instance, passwords as a first factor, our scheme maximizes the deployability of two-factor authentication for...
We present Tesla# (pronounced "Tesla Sharp"), a digital signature scheme based on the RLWE assumption that continues a recent line of proposals of lattice-based digital signature schemes originating in work by Lyubashevsky as well as by Bai and Galbraith. It improves upon all of its predecessors in that it attains much faster key pair generation, signing, and verification, outperforming most (conventional or lattice-based) signature schemes on modern processors. We propose a selection of...
In this paper, we provide a necessary clarification of the good security properties that can be obtained from parallel implementations of masking schemes. For this purpose, we first argue that (i) the probing model is not straightforward to interpret, since it more naturally captures the intuitions of serial implementations, and (ii) the noisy leakage model is not always convenient, e.g. when combined with formal methods for the verification of cryptographic implementations. Therefore we...
This paper surveys the landscape of security verification approaches and techniques for computer systems at various levels: from a software-application level all the way to the physical hardware level. Different existing projects are compared, based on the tools used and security aspects being examined. Since many systems require both hardware and software components to work together to provide the system's promised security protections, it is not sufficient to verify just the software...
Protocols for secure electronic voting are of increasing societal importance. Proving rigorously their security is more challenging than many other protocols, which aim at authentication or key exchange. One of the reasons is that they need to be secure for an arbitrary number of malicious voters. In this paper we identify a class of voting protocols for which only a small number of agents needs to be considered: if there is an attack on vote privacy then there is also an attack that...
The ``kernel" model has been part of operating system architecture for decades, but upon closer inspection it clearly violates the principle of least required privilege. The kernel is a single entity which provides many services (memory management, interfacing to drivers, context switching, IPC) which have no real relation to each other, and has the ability to observe or tamper with all state of the system. This work presents Antikernel, a novel operating system architecture consisting of...
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 two types of 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 collision-resistant, which gives a direct application of this new primitive. We...
- « Previous
- 1
- 2
- 3
- Next »
