IACR News
Here you can see all recent updates to the IACR webpage. These updates are also available:
11 September 2023
Valerie Fetzer, Michael Klooß, Jörn Müller-Quade, Markus Raiber, Andy Rupp
ePrint Report
User privacy is becoming increasingly important in our digital society. Yet, many applications face legal requirements or regulations that prohibit unconditional anonymity guarantees, e.g., in electronic payments where surveillance is mandated to investigate suspected crimes.
As a result, many systems have no effective privacy protections at all, or have backdoors, e.g., stored at the operator side of the system, that can be used by authorities to disclose a user’s private information (e.g., lawful interception). The problem with such backdoors is that they also enable silent mass surveillance within the system. To prevent such misuse, various approaches have been suggested which limit possible abuse or ensure it can be detected. Many works consider auditability of surveillance actions but do not enforce that traces are left when backdoors are retrieved. A notable exception which offers retrospective and silent surveillance is the recent work on misuse-resistant surveillance by Green et al. (EUROCRYPT’21). However, their approach relies on extractable witness encryption, which is a very strong primitive with no known efficient and secure implementations.
In this work, we develop a building block for auditable surveillance. In our protocol, backdoors or escrow secrets of users are protected in multiple ways: (1) Backdoors are short-term and user-specific; (2) they are shared between trustworthy parties to avoid a single point of failure; and (3) backdoor access is given conditionally. Moreover (4) there are audit trails and public statistics for every (granted) backdoor request; and (5) surveillance remains silent, i.e., users do not know they are surveilled. Concretely, we present an abstract UC-functionality which can be used to augment applications with auditable surveillance capabilities. Our realization makes use of threshold encryption to protect user secrets, and is concretely built in a blockchain context with committee-based YOSO MPC. As a consequence, the committee can verify that the conditions for backdoor access are given, e.g., that law enforcement is in possession of a valid surveillance warrant (via a zero-knowledge proof). Moreover, access leaves an audit trail on the ledger, which allows an auditor to retrospectively examine surveillance decisions.
As a toy example, we present an Auditably Sender-Traceable Encryption scheme, a PKE scheme where the sender can be deanonymized by law enforcement. We observe and solve problems posed by retrospective surveillance via a special non-interactive non-committing encryption scheme which allows zero-knowledge proofs over message, sender identity and (escrow) secrets.
As a result, many systems have no effective privacy protections at all, or have backdoors, e.g., stored at the operator side of the system, that can be used by authorities to disclose a user’s private information (e.g., lawful interception). The problem with such backdoors is that they also enable silent mass surveillance within the system. To prevent such misuse, various approaches have been suggested which limit possible abuse or ensure it can be detected. Many works consider auditability of surveillance actions but do not enforce that traces are left when backdoors are retrieved. A notable exception which offers retrospective and silent surveillance is the recent work on misuse-resistant surveillance by Green et al. (EUROCRYPT’21). However, their approach relies on extractable witness encryption, which is a very strong primitive with no known efficient and secure implementations.
In this work, we develop a building block for auditable surveillance. In our protocol, backdoors or escrow secrets of users are protected in multiple ways: (1) Backdoors are short-term and user-specific; (2) they are shared between trustworthy parties to avoid a single point of failure; and (3) backdoor access is given conditionally. Moreover (4) there are audit trails and public statistics for every (granted) backdoor request; and (5) surveillance remains silent, i.e., users do not know they are surveilled. Concretely, we present an abstract UC-functionality which can be used to augment applications with auditable surveillance capabilities. Our realization makes use of threshold encryption to protect user secrets, and is concretely built in a blockchain context with committee-based YOSO MPC. As a consequence, the committee can verify that the conditions for backdoor access are given, e.g., that law enforcement is in possession of a valid surveillance warrant (via a zero-knowledge proof). Moreover, access leaves an audit trail on the ledger, which allows an auditor to retrospectively examine surveillance decisions.
As a toy example, we present an Auditably Sender-Traceable Encryption scheme, a PKE scheme where the sender can be deanonymized by law enforcement. We observe and solve problems posed by retrospective surveillance via a special non-interactive non-committing encryption scheme which allows zero-knowledge proofs over message, sender identity and (escrow) secrets.
Bidhannagar, India, 21 December - 23 December 2023
Event Calendar
Event date: 21 December to 23 December 2023
Submission deadline: 15 September 2023
Notification: 31 October 2023
Submission deadline: 15 September 2023
Notification: 31 October 2023
Halifax, Canada, 4 September - 7 September 2024
CHES
Event date: 4 September to 7 September 2024
University of Leuven (KU Leuven)
Job Posting
The research involves developing SW and HW security solutions and acceleration of core cryptographic primitives deployed at the Edge. The successful candidate will be part of a Horizon Network of Excellence for distributed, trustworthy, efficient and scalable AI at the Edge.
Responsibilities: Security and privacy threat modeling.
Security evaluation and assessment.
Design and implement optimized privacy-preserving computation protocols for low-power general purpose processors.
Write research papers and project deliverables, and present findings at intessrnational conferences and workshops.
Specific skills required
To be considered for this position, you should have a PhD degree in computer science or mathematics or cryptography, with a strong publication track record in top venues. In addition, good communication and programming skills are required.
Responsibilities:
Specific skills required
To be considered for this position, you should have a PhD degree in computer science or mathematics or cryptography, with a strong publication track record in top venues. In addition, good communication and programming skills are required.
Closing date for applications:
Contact: jobs-cosic@esat.kuleuven.be
More information: https://www.esat.kuleuven.be/cosic/vacancies/
University of Leuven (KU Leuven)
Job Posting
The research involves developing SW and HW security solutions and acceleration of core cryptographic primitives deployed at the Edge. The successful candidate will be part of a Horizon Network of Excellence for distributed, trustworthy, efficient and scalable AI at the Edge.
Responsibilities: Design and develop secure mechanisms for authentication, aothorization, and access control for the distributed network.
Design and develop lightweight security mechanisms for Federated Learning, and SW/HW acceleration of relevant cryptographic primitives.
Write research papers and present findings at intessrnational conferences and workshops.
Specific skills required To be considered for this position, you should have a strong background in computer science or mathematics, with a specialization in cryptography or related fields. Ideally, you will hold a master's degree in a relevant discipline and have excellent analytical and problem-solving skills. Good programming skills, e.g., in C/C++/Python/Rust, will be merited.
Responsibilities:
Specific skills required To be considered for this position, you should have a strong background in computer science or mathematics, with a specialization in cryptography or related fields. Ideally, you will hold a master's degree in a relevant discipline and have excellent analytical and problem-solving skills. Good programming skills, e.g., in C/C++/Python/Rust, will be merited.
Closing date for applications:
Contact: jobs-cosic@esat.kuleuven.be
More information: https://www.esat.kuleuven.be/cosic/vacancies/
08 September 2023
Willemstad, Netherlands, 4 March - 8 March 2024
Event Calendar
Event date: 4 March to 8 March 2024
Submission deadline: 18 September 2023
Notification: 25 November 2023
Submission deadline: 18 September 2023
Notification: 25 November 2023
David Balbás, Dario Fiore, Maria Isabel González Vasco, Damien Robissout, Claudio Soriente
ePrint Report
Cryptographic proof systems provide integrity, fairness, and privacy in applications that outsource data processing tasks. However, general-purpose proof systems do not scale well to large inputs. At the same time, ad-hoc solutions for concrete applications - e.g., machine learning or image processing - are more efficient but lack modularity, hence they are hard to extend or to compose with other tools of a data-processing pipeline.
In this paper, we combine the performance of tailored solutions with the versatility of general-purpose proof systems. We do so by introducing a modular framework for verifiable computation of sequential operations. The main tool of our framework is a new information-theoretic primitive called Verifiable Evaluation Scheme on Fingerprinted Data (VE) that captures the properties of diverse sumcheck-based interactive proofs, including the well-established GKR protocol. Thus, we show how to compose VEs for specific functions to obtain verifiability of a data-processing pipeline.
We propose a novel VE for convolution operations that can handle multiple input-output channels and batching, and we use it in our framework to build proofs for (convolutional) neural networks and image processing. We realize a prototype implementation of our proof systems, and show that we achieve up to $5 \times$ faster proving time and $10 \times$ shorter proofs compared to the state-of-the-art, in addition to asymptotic improvements.
In this paper, we combine the performance of tailored solutions with the versatility of general-purpose proof systems. We do so by introducing a modular framework for verifiable computation of sequential operations. The main tool of our framework is a new information-theoretic primitive called Verifiable Evaluation Scheme on Fingerprinted Data (VE) that captures the properties of diverse sumcheck-based interactive proofs, including the well-established GKR protocol. Thus, we show how to compose VEs for specific functions to obtain verifiability of a data-processing pipeline.
We propose a novel VE for convolution operations that can handle multiple input-output channels and batching, and we use it in our framework to build proofs for (convolutional) neural networks and image processing. We realize a prototype implementation of our proof systems, and show that we achieve up to $5 \times$ faster proving time and $10 \times$ shorter proofs compared to the state-of-the-art, in addition to asymptotic improvements.
Jakob Feldtkeller, Tim Güneysu, Thorben Moos, Jan Richter-Brockmann, Sayandeep Saha, Pascal Sasdrich, François-Xavier Standaert
ePrint Report
Physical attacks are well-known threats to cryptographic implementations. While countermeasures against passive Side-Channel Analysis (SCA) and active Fault Injection Analysis (FIA) exist individually, protecting against their combination remains a significant challenge. A recent attempt at achieving joint security has been published at CCS 2022 under the name CINI-MINIS. The authors introduce relevant security notions and aim to construct arbitrary-order gadgets that remain trivially composable in the presence of a combined adversary. Yet, we show that all CINI-MINIS gadgets at any order are susceptible to a devastating attack with only a single fault and probe due to a lack of error correction modules in the compression. We explain the details of the attack, pinpoint the underlying problem in the constructions, propose an additional design principle, and provide new (fixed) provably secure and composable gadgets for arbitrary order. Luckily, the changes in the compression stage help us to save correction modules and registers elsewhere, making the resulting Combined Private Circuits (CPC) more secure and more efficient than the original ones. We also explain why the discovered flaws have been missed by the associated formal verification tool VERICA (TCHES 2022) and propose fixes to remove its blind spot. Finally, we explore alternative avenues to repair the compression stage without additional corrections based on non-completeness, i.e., constructing a compression that never recombines any secret. Yet, while this approach could have merit for low-order gadgets, it is, for now, hard to generalize and scales poorly to higher orders. We conclude that our refurbished arbitrary order CINI gadgets provide a solid foundation for further research.
Sıla ÖZEREN, Oğuz YAYLA
ePrint Report
In the context of post-quantum secure algorithms like CRYSTALS-Kyber, the importance of protecting sensitive polynomial coefficients from side-channel attacks is increasingly recognized. Our research introduces two alternative masking methods to enhance the security of the compression function in Kyber through masking. Prior to this, the topic had been addressed by only one other research study. The "Double and Check" method integrates arithmetic sharing and symmetry adjustments, introducing a layer of obfuscation by determining coefficient values based on modular overflows. In contrast, the Look-Up-Table (LUT) integration method employs arithmetic-to-Boolean conversions, augmented by a pre-computed table for efficient value verifications. Furthermore, by leveraging the alternative prime 7681, we propose a novel masked compression function. This prime, 7681, is also notable as the smallest prime suitable for fast NTT multiplication. While both algorithms prioritize data protection and streamlined processing, they also underscore the inherent challenges of balancing computational speed with the potential vulnerabilities to side-channel attacks.
Aniket Kate, Easwar Vivek Mangipudi, Siva Mardana, Pratyay Mukherjee
ePrint Report
Web3 applications based on blockchains regularly need access to randomness that is unbiased, unpredictable, and publicly verifiable. For Web3 gaming applications, this becomes a crucial selling point to attract more users by providing credibility to the "random reward" distribution feature. A verifiable random function (VRF) protocol satisfies these requirements naturally, and there is a tremendous rise in the use of VRF services. As most blockchains cannot maintain the secret keys required for VRFs, Web3 applications interact with external VRF services via a smart contract where a VRF output is exchanged for a fee. While this smart contract-based plain-text exchange offers the much-needed public verifiability immediately, it severely limits the way the requester can employ the VRF service: the requests cannot be made in advance, and the output cannot be reused. This introduces significant latency and monetary overhead.
This work overcomes this crucial limitation of the VRF service by introducing a novel privacy primitive Output Private VRF ( Pri-VRF) and thereby adds significantly more flexibility to the Web3-based VRF services. We call our framework FlexiRand. While maintaining the pseudo-randomness and public verifiability properties of VRFs, FlexiRand ensures that the requester alone can observe the VRF output. The smart contract and anybody else can only observe a blinded-yet-verifiable version of the output. We formally define Pri-VRF, put forward a practically efficient design, and provide provable security analysis in the universal composability (UC) framework (in the random oracle model) using a variant of one-more Diffie-Hellman assumption over bilinear groups.
As the VRF service, with its ownership of the secret key, be- comes a single point of failure, it is realized as a distributed VRF with the key secret-shared across distinct nodes in our framework. We develop our distributed Pri-VRF construction by combining approaches from Distributed VRF and Distributed Oblivious PRF literature. We provide provable security analysis (in UC), implement it and compare its performance with existing distributed VRF schemes. Our distributed Pri-VRF only introduces a minimal computation and communication overhead for the VRF service, the requester, and the contract.
This work overcomes this crucial limitation of the VRF service by introducing a novel privacy primitive Output Private VRF ( Pri-VRF) and thereby adds significantly more flexibility to the Web3-based VRF services. We call our framework FlexiRand. While maintaining the pseudo-randomness and public verifiability properties of VRFs, FlexiRand ensures that the requester alone can observe the VRF output. The smart contract and anybody else can only observe a blinded-yet-verifiable version of the output. We formally define Pri-VRF, put forward a practically efficient design, and provide provable security analysis in the universal composability (UC) framework (in the random oracle model) using a variant of one-more Diffie-Hellman assumption over bilinear groups.
As the VRF service, with its ownership of the secret key, be- comes a single point of failure, it is realized as a distributed VRF with the key secret-shared across distinct nodes in our framework. We develop our distributed Pri-VRF construction by combining approaches from Distributed VRF and Distributed Oblivious PRF literature. We provide provable security analysis (in UC), implement it and compare its performance with existing distributed VRF schemes. Our distributed Pri-VRF only introduces a minimal computation and communication overhead for the VRF service, the requester, and the contract.
Kushal Babel, Mojan Javaheripi, Yan Ji, Mahimna Kelkar, Farinaz Koushanfar, Ari Juels
ePrint Report
We introduce Lanturn: a general purpose adaptive learning-based framework for measuring the cryptoeconomic security of composed decentralized-finance (DeFi) smart contracts. Lanturn discovers strategies comprising of concrete transactions for extracting economic value from smart contracts interacting with a particular transaction environment. We formulate the strategy discovery as a black-box optimization problem and leverage a novel adaptive learning-based algorithm to address it.
Lanturn features three key properties. First, it needs no contract-specific heuristics or reasoning, due to our black-box formulation of cryptoeconomic security. Second, it utilizes a simulation framework that operates natively on blockchain state and smart contract machine code, such that transactions returned by Lanturn’s learning-based optimization engine can be executed on-chain without modification. Finally, Lanturn is scalable in that it can explore strategies comprising a large number of transactions that can be reordered or subject to insertion of new transactions.
We evaluate Lanturn on the historical data of the biggest and most active DeFi Applications: Sushiswap, UniswapV2, UniswapV3, and AaveV2. Our results show that Lanturn not only rediscovers existing, well-known strategies for extracting value from smart contracts, but also discovers new strategies that are previously undocumented. Lanturn also consistently discovers higher value than evidenced in the wild, surpassing a natural baseline computed using value extracted by bots and other strategic agents.
Carlo Brunetta, Hans Heum, Martijn Stam
ePrint Report
When modelling how public key encryption can enable secure communication, we should acknowledge that secret information, such as private keys or the randomness used for encryption, could become compromised. Intuitively, one would expect unrelated communication to remain secure, yet formalizing this intuition has proven challenging. Several security notions have appeared that aim to capture said scenario, ranging from the multi-user setting with corruptions, via selective opening attacks (SOA), to non-committing encryption (NCE). Remarkably, how the different approaches compare has not yet been systematically explored.
We provide a novel framework that maps each approach to an underlying philosophy of confidentiality: indistinguishability versus simulatability based, each with an a priori versus an a posteriori variant, leading to four distinct philosophies. In the absence of corruptions, these notions are largely equivalent; yet, in the presence of corruptions, they fall into a hierarchy of relative strengths, from IND-CPA and IND-CCA at the bottom, via indistinguishability SOA and simulatability SOA, to NCE at the top.
We provide a concrete treatment for the four notions, discuss subtleties in their definitions and asymptotic interpretations and identify limitations of each. Furthermore, we re-cast the main implications of the hierarchy in a concrete security framework, summarize and contextualize other known relations, identify open problems, and close a few gaps.
We end on a survey of constructions known to achieve the various notions. We identify and name a generic random-oracle construction that has appeared in various guises to prove security in seemingly different contexts. It hails back to Bellare and Rogaway's seminal work on random oracles (CCS'93) and, as previously shown, suffices to meet one of the strongest notions of our hierarchy (single-user NCE with bi-openings).
We provide a novel framework that maps each approach to an underlying philosophy of confidentiality: indistinguishability versus simulatability based, each with an a priori versus an a posteriori variant, leading to four distinct philosophies. In the absence of corruptions, these notions are largely equivalent; yet, in the presence of corruptions, they fall into a hierarchy of relative strengths, from IND-CPA and IND-CCA at the bottom, via indistinguishability SOA and simulatability SOA, to NCE at the top.
We provide a concrete treatment for the four notions, discuss subtleties in their definitions and asymptotic interpretations and identify limitations of each. Furthermore, we re-cast the main implications of the hierarchy in a concrete security framework, summarize and contextualize other known relations, identify open problems, and close a few gaps.
We end on a survey of constructions known to achieve the various notions. We identify and name a generic random-oracle construction that has appeared in various guises to prove security in seemingly different contexts. It hails back to Bellare and Rogaway's seminal work on random oracles (CCS'93) and, as previously shown, suffices to meet one of the strongest notions of our hierarchy (single-user NCE with bi-openings).
Nirvan Tyagi, Arasu Arun, Cody Freitag, Riad Wahby, Joseph Bonneau, David Mazières
ePrint Report
We introduce the first practical protocols for fully decentralized
sealed-bid auctions using timed commitments. Timed commitments
ensure that the auction is finalized fairly even if all participants drop
out after posting bids or if $n-1$ bidders collude to try to learn the
$n^{th}$ bidder’s bid value. Our protocols rely on a novel non-malleable
timed commitment scheme which efficiently supports range proofs
to establish that bidders have sufficient funds to cover a hidden
bid value. This allows us to penalize users who abandon bids for
exactly the bid value, while supporting simultaneous bidding in
multiple auctions with a shared collateral pool. Our protocols are
concretely efficient and we have implemented them in an Ethereum-
compatible smart contract which automatically enforces payment
and delivery of an auctioned digital asset.
Thomas Espitau, Thi Thu Quyen Nguyen, Chao Sun, Mehdi Tibouchi, Alexandre Wallet
ePrint Report
In this paper, we introduce a novel trapdoor generation technique for
Prest's hybrid sampler over NTRU lattices. Prest's sampler is used in
particular in the recently proposed Mitaka signature scheme
(Eurocrypt 2022), a variant of the Falcon signature scheme, one of the
candidates selected by NIST for standardization. Mitaka was introduced
to address Falcon's main drawback, namely the fact that the lattice
Gaussian sampler used in its signature generation is highly complex,
difficult to implement correctly, to parallelize or protect against
side-channels, and to instantiate over rings of dimension not a power of
two to reach intermediate security levels. Prest's sampler is
considerably simpler and solves these various issues, but when applying
the same trapdoor generation approach as Falcon, the resulting
signatures have far lower security in equal dimension. The Mitaka
paper showed how certain randomness-recycling techniques could be used to
mitigate this security loss, but the resulting scheme is still
substantially less secure by Falcon (by around 20 to 50 bits of
CoreSVP security depending on the parameters), and has much slower key
generation.
Our new trapdoor generation techniques solves all of those issues satisfactorily: it gives rise to a much simpler and faster key generation algorithm than Mitaka's (achieving similar speeds to Falcon), and is able to comfortably generate trapdoors reaching the same NIST security levels as Falcon as well. It can also be easily adapted to rings of intermediate dimensions, in order to support the same versatility as Mitaka in terms of parameter selection. All in all, this new technique combines all the advantages of both Falcon and Mitaka (and more) with none of the drawbacks.
Our new trapdoor generation techniques solves all of those issues satisfactorily: it gives rise to a much simpler and faster key generation algorithm than Mitaka's (achieving similar speeds to Falcon), and is able to comfortably generate trapdoors reaching the same NIST security levels as Falcon as well. It can also be easily adapted to rings of intermediate dimensions, in order to support the same versatility as Mitaka in terms of parameter selection. All in all, this new technique combines all the advantages of both Falcon and Mitaka (and more) with none of the drawbacks.
Jiaxin Pan, Runzhi Zeng
ePrint Report
We propose a generic construction of password-based authenticated key exchange (PAKE) from key encapsulation mechanisms (KEM). Assuming that the KEM is oneway secure against plaintext-checkable attacks (OW-PCA), we prove that our PAKE protocol is \textit{tightly secure} in the Bellare-Pointcheval-Rogaway model (EUROCRYPT 2000). Our tight security proofs require ideal ciphers and random oracles. The OW-PCA security is relatively weak and can be implemented tightly with the Diffie-Hellman assumption, which generalizes the work of Liu et al. (PKC 2023), and ``almost'' tightly with lattice-based assumptions, which tightens the security loss of the work of Beguinet et al. (ACNS 2023) and allows more efficient practical implementation with Kyber. Beyond these, it opens an opportunity of constructing tight PAKE based on various assumptions.
Shashi Kant Pandey
ePrint Report
The use of random seeds to a deterministic random bit generator to generate uniform random sampling has been applied multiple times in post-quantum algorithms. The finalists Dilithium and Kyber use SHAKE and AES to generate the random sequence at multiple stages of the algorithm. Here we characterize one of the sampleing techniques available in Dilithium for a random sequence of length 256 with the help of the neutrosophic Boolean function. The idea of the neutrosophic Boolean function came from the theory of neutrosophy and it is useful to study any ternary distributions. We present the non-existence of neutrobalanced bent functions specifically with respect to the sampling named SampleInBall in Dilithium.
Gabrielle Beck, Harry Eldridge, Matthew Green, Nadia Heninger, Abhishek Jain
ePrint Report
Location tracking accessories (or ``tracking tags'') such as those sold by Apple, Samsung, and Tile, allow owners to track the location of their property and devices via offline tracking networks. The tracking protocols have been designed to ensure some level of user privacy against surveillance by the vendor. Such privacy mechanisms, however, seem to be at odds with the phenomenon of tracker-based stalking, where attackers use these very tags to monitor a target's movements. Numerous such criminal incidents have been reported, and in response, manufacturers have chosen to weaken privacy guarantees in order to allow users to detect malicious stalker tags.
In this work we show how to achieve an improved trade-off between user privacy and stalker detection within the constraints of existing tracking protocols. We implement our new protocol using families of list-decodable error-correcting codes, and give efficient algorithms for stalker detection under realistic conditions.
In this work we show how to achieve an improved trade-off between user privacy and stalker detection within the constraints of existing tracking protocols. We implement our new protocol using families of list-decodable error-correcting codes, and give efficient algorithms for stalker detection under realistic conditions.
Ishtiyaque Ahmad, Divyakant Agrawal, Amr El Abbadi, Trinabh Gupta
ePrint Report
Consider a cloud server that owns a key-value store and provides a private query service to its clients. Preserving client privacy in this setting is difficult because the key-value store is public, and a client cannot encrypt or modify it. Therefore, privacy in this context implies hiding the access pattern of a client. Pantheon is a system that cryptographically allows a client to retrieve the value corresponding to a key from a public key-value store without allowing the server or any adversary to know any information about the key or value accessed. Pantheon devises a single-round retrieval protocol which reduces server-side latency by refining its cryptographic machinery and massively parallelizing the query execution workload. Using these novel techniques, Pantheon achieves a $93\times$ improvement for server-side latency over a state-of-the-art solution.
Mengce Zheng
ePrint Report
We point out critical deficiencies in lattice-based cryptanalysis of common prime RSA presented in ``Remarks on the cryptanalysis of common prime RSA for IoT constrained low power devices'' [Information Sciences, 538 (2020) 54--68]. To rectify these flaws, we carefully scrutinize the relevant parameters involved in the analysis during solving a specific trivariate integer polynomial equation. Additionally, we offer a synthesized attack illustration of small private key attacks on common prime RSA.
Karthikeyan Bhargavan, Abhishek Bichhawat, Pedram Hosseyni, Ralf Kuesters, Klaas Pruiksma, Guido Schmitz, Clara Waldmann, Tim Würtele
ePrint Report
While cryptographic protocols are often analyzed in isolation, they are typically deployed within a stack of protocols, where each layer relies on the security guarantees provided by the protocol layer below it, and in turn provides its own security functionality to the layer above. Formally analyzing the whole stack in one go is infeasible even for semi-automated verification tools, and impossible for pen-and-paper proofs. The DY$^\star$ protocol verification framework offers a modular and scalable technique that can reason about large protocols, specified as a set of F$^\star$ modules. However, it does not support the compositional verification of layered protocols since it treats the global security invariants monolithically. In this paper, we extend DY$^\star$ with a new methodology that allows analysts to modularly analyze each layer in a way that compose to provide security for a protocol stack. Importantly, our technique allows a layer to be replaced by another implementation, without affecting the proofs of other layers. We demonstrate this methodology on two case studies. We also present a verified library of generic authenticated and confidential communication patterns that can be used in future protocol analyses and is of independent interest.