Group Signatures are fundamental cryptographic primitives that allow users to sign a message on behalf of a predefined set of users, curated by the group manager. The security properties ensure that members of the group can sign anonymously and without fear of being framed. In dynamic group signatures, the group manager has finer-grained control over group updates while ensuring membership privacy (i.e., hiding when users join and leave). The only known scheme that achieves standard security properties and membership privacy has been proposed by Backes et al. CCS 2019. However, they rely on an inefficient revocation mechanism that re-issues credentials to all active members during every group update, and users have to rely on a secure and private channel to join the group. In this paper, we introduce a dynamic group signature that supports verifier local revocation, while achieving strong security properties, including membership privacy for users joining over a public channel. Moreover, when our scheme is paired with structure-preserving signatures over equivalence class it enjoys a smaller signature size compared to Backes et al. Finally, as a stand-alone contribution we extend the primitive Asynchronous Remote Key Generation (Frymann et al. CCS 2020) with trapdoors and introduce new security properties to capture this new functionality, which is fundamental to the design of our revocation mechanism.
In this paper, we propose a novel choke point metric for the elimination of attack paths. Our study is motivated by its applications in the widely used Active Directory (AD) attack graphs. Choke points are typically defined as critical locations where the largest number of attack paths converge. Identifying these choke points is crucial. Enumeration of all attack paths is implied in this definition, but the immensity of paths in AD attack graphs makes the task extremely challenging. Consequently, industry solutions and research often rely on mapping only the shortest paths or prioritizing their elimination as a method for hardening AD attack graphs. We theoretically describe and empirically measure major limitations with the shortest path approach. To address the limitations, we introduce a new choke point metric that quantifies the intersection of connections rather than attack paths, which improves upon shortest path mapping. Additionally, we present human experiments to observe how white-hat hackers use shortest path mapping, provide simple graph examples that visually demonstrate failure cases where shortest path-based methods do not yield optimal results, and conduct experiments with a diverse set of real-world and synthetic AD datasets. From the results, we conclude that uninformed attack path mapping cannot capture the complexity of the attack path composition in a real-world attack, and reliance on shortest path mapping leads to significant volatility in security-hardening outcomes. In contrast, the connection-based choke point metric we propose offers greater optimality and utility in mitigating the attack surface.
Message Authentication Codes (MACs) represent a fundamental symmetric key primitive, serving to ensure the authenticity and integrity of transmitted data. As a building block in authenticated encryption and in numerous deployed standards, including TLS, IPsec, and SSH, MACs play a central role in practice. Due to their importance for practice, MACs have been subject to extensive research, leading to prominent schemes such as HMAC, CBCMAC, or LightMAC. Despite the existence of various MACs, there is still considerable interest in creating schemes that are more efficient, potentially parallelizable, or have specific non-cryptographic attributes, such as being patent-free. In this context, we introduce an automated method for analyzing and synthesizing MAC schemes. In order to achieve this goal, we have constructed a framework that restricts the class of MACs in such a way that it is sufficiently expressive to cover known constructions, yet also admits automated reasoning about the security guarantees of both known and new schemes. Our automated analysis has identified a novel category of MACs, termed “hybrid” MACs. These MACs operate by processing multiple blocks concurrently, with each block managed by a different, specified MAC scheme. A key finding is that in certain scenarios, the hybrid MAC marginally outperforms the simultaneous operation of the individual MACs. This improvement is attributed to the hybrid approach exploiting the strengths and compensating for the weaknesses of each distinct MAC scheme involved. Our implementation confirms that we have successfully identified new schemes that have comparable performance with state-of-the-art schemes and in some settings seem to be slightly more efficient.
State-separating proofs are a powerful tool to structure cryptographic arguments, so that they are amenable for mechanization, as has been shown through implementations, such as SSProve. However, the treatment of separation for heaps has never been satisfactorily addressed. In this work, we present the first comprehensive treatment of nominal state separation in state-separating proofs using nominal sets. We provide a Rocq library, called Nominal-SSProve, that builds on nominal state separation supporting mechanized proofs that appear more concise and arguably more elegant.
Explainability and transparency of computations, as well as compliance with data-privacy requirements, presuppose an understanding of whether some input plays a non-trivial role in computing an output. However, difficulty in distinguishing between correlation and actual usage in computation, along with possible correlations between inputs, makes determination of such accountability challenging. A flow definition is presented that can make this distinction. The definition enables the construction of accountability evidence to establish how an input is computed based on an output, in terms of the intermediate variables used. Intermediate variables can also serve as mediation points that fully block information flow from an input to an output. A connection between accountability and mediation is established by showing the role of mediation points for constructing accountability evidence.
Voter privacy and end-to-end (E2E) verifiability are critical features of electronic voting (e-voting) systems to safeguard elections. To achieve these properties commonly a perfect bulletin board (BB) is assumed that provides consistent, reliable, and tamper-proof storage and transmission of voting data. However, in practice, BBs operate in asynchronous and unreliable networks, and hence, are susceptible to vulnerabilities such as equivocation attacks and dropped votes, which can compromise both verifiability and privacy. Although prior research has weakened the perfect BB assumption, it still depends on trusting certain BB components. In this work, we present and initiate a formal exploration of designing e-voting systems based on fully untrusted BBs. For this purpose, we leverage the notion of accountability and in particular use accountable BBs. Accountability ensures that if a security breach occurs, then cryptographic evidence can identify malicious parties. Fully untrusted BBs running in asynchronous networks bring new challenges. Among others, we identify several types of attacks that a malicious but accountable BB might be able to perform and propose a new E2E verifiability notion for this setting. Based on this notion and as a proof of concept, we construct the first e-voting system that is provably E2E verifiable and provides vote privacy even when the underlying BB is fully malicious. This establishes an alternative to traditional e-voting architectures that rely on (threshold) trusted BB servers.
In this paper we present Declassification Core Calculus (DeCC), a graded modal type theory for relaxed semantic declassification, a declassification criterion inspired from Delimited Release and Relaxed Noninterference. We build upon Dependency Core Calculus (DCC) that already has a graded monad for classification of information. DeCC inherits DCC's graded monad, but adds a new modality for the purpose of declassification. We build a logical relation model describing both the unary and relational semantics of the types including the two graded modalities, and use this model to prove the soundness of DeCC. We describe how our new modality interacts with DCC's graded monad via distributive laws, and also describe the conditions under which our new modality forms a comonad. This work has been mechanised in the HOL4 theorem prover.
The security of Fully Homomorphic Encryption (FHE) has received a lot of attention in recent years with new security notions emerging to better understand the practical attacks that may threaten the real-world deployments of passively secure FHE schemes. One such new notions is CPAD a slight extension of CPA security modelling a passive adversary who is granted access to a decryption oracle accepting only well-formed ciphertexts. While successful CPAD attacks have initially been performed on approximate FHE schemes such as CKKS, recent works have also demonstrated practical CPAD attacks on all mainstream non-approximate FHE, such as BFV, BGV or TFHE. Despite their clear computational practicality, these latter attacks however focus on the abstract security game defining CPAD security. In this paper, we show how to concretely build on these to mount successful FHE key recovery attacks in the Federated Learning (FL) setting, an application scenario of choice for FHE techniques. In FL, participating entities or workers encrypt successive model updates based on their local training data, enabling a central server to aggregate them in order to homomorphically update a global model. As this paper demonstrates, this environment provides a playground for an attacker to launch key recovery attacks against the FHE underlying the secure aggregation mechanism. As such, our findings reveal substantial stealthy key-recovery threats from both the server and a single worker, with very limited impact on the FL training progression or final model quality.
A regular expression (regex) is said to be vulnerable to the regex denial of service (ReDoS) attack if the worst-case running time of a matching algorithm on the regex is super-linear in the length of the input string. Due to the wide-spread usage of regexes, ReDoS is well recognized to be a serious security threat. Meanwhile, backreference is an extension to regexes that allows preceding substrings to be used later. The extension is practically popular, supported by many regex engines including those in the standard libraries of Java, Python, JavaScript, and more, and is also known to possess interesting theoretical properties such as the language class of regexes extended with it being outside of that of context-free languages but included in that of indexed languages. This paper is a formal study of ReDoS for regexes with and without backreferences. We make the following contributions: (1) we give a sufficient condition for ReDoS invulnerability in terms of the degree of ambiguity of the non-deterministic automaton corresponding to the given regex, using the memory automata model of Schmid for the case with backreferences, and (2) we show a transformation method based on state elimination that converts a deterministic memory (or ordinary) automaton to an equivalent ReDoS-invulnerable regex with (or without) backreferences. A corollary of (2) is that, in the case without backreferences, every regex can be converted to an equivalent ReDoS-invulnerable form. Finally, we show that, in stark contrast to the case without backreferences, (3) assuming a certain well-believed conjecture in parameterized complexity theory, there exists no algorithm for converting every regex with backreferences to an equivalent ReDoS-invulnerable form. We note that the positive results (1) and (2) apply to the practically popular but inefficient backtracking matching algorithm, whereas the negative result (3) applies to any matching algorithm.
Zero-Knowledge Proofs (ZKPs) are cryptographic building blocks of many privacy-preserving security protocols. An important research focus in this area is the development of post-quantum ZKPs. These are ZKPs whose security is reduced to computational hardness assumptions that are assumed to be intractable even by scalable quantum computers. In this paper, we study the post-quantum ZKPs of Jain, Krenn, Pietrzak, and Tentes (Asiacrypt 2012). These are the only ZKPs for proving arbitrary binary statements whose security reduces to the Learning Parity with Noise (LPN) problem-a very conservative post-quantum hardness assumption. We make the following contributions to further develop the potential and understanding of these ZKPs. First, we optimize the efficiency of the verifier by several orders of magnitude, making this part as computationally light as that of the prover. Second, we show that the only open source implementation of these ZKPs does not implement them correctly, allowing a malicious prover to convince the verifier of false statements. Third, we formally verify for the first time the security of these (optimized) ZKPs in EasyCrypt. Fourth, we show how these ZKPs can be used to construct the first code-based ZKP of shuffle and verifiable e- voting protocol.
A multi-designated verifier signature (MDVS) is a digital signature that empowers a signer to designate specific verifiers capable of verifying signatures. Notably, designated verifiers are allowed to not only verify signatures but also simulate "fake" signatures indistinguishable from real ones produced by the original signer. Since this property is useful for realizing off-the-record (i.e., deniable) communication in group settings, MDVS is attracting attention in secure messaging. Recently, Damgard et al. (TCC'20) and Chakraborty et al. (EUROCRYPT'23) have introduced new MDVS schemes, allowing a subset of designated verifiers to simulate signatures in contrast to the conventional one, which requires all designated verifiers for signature simulation. They also define a stronger notion of security for them. This work delves into this new MDVS and offers a comprehensive formalization. We identify all possible security levels of MDVS schemes in subset simulations and prove that some of them are not feasible. Furthermore, we demonstrate that MDVS schemes meeting the security notion defined by Chakraborty et al. imply IND-CCA secure public-key encryption schemes. Beyond formalization, we present new constructions of MDVS schemes in subset simulation. Notably, we introduce a new construction of strongly secure MDVS schemes based on ring signatures and public-key encryption, accompanied by a generic conversion for achieving consistency through non-interactive zero-knowledge arguments. Finally, we evaluate the efficiency of our MDVS schemes in classical and post-quantum settings, showing their practicality.
Cryptographic protocols commonly use (random) nonces to guarantee security properties. Although it is known for a long time that nonces should benefit from clear security properties, modern standards regularly miss this fundamental requirement. The lack of clear recommendations leads to error-prone cryptographic implementations, especially vulnerabilities due to nonce reuse and nonce leakage. This paper introduces a method based on TAMARIN to identify with a systematic approach the nonce-related properties an implementation should guarantee to ensure the security of a cryptographic protocol. As a corollary, the method also determines the security impact of a nonce misuse. Our method also applies to other types of random values used in protocols, namely ephemeral keys, masks, and nonces used in randomized primitives. This approach is then extended to take into account the well-known weaknesses of some randomized primitives when nonces are reused. The paper finally applies the method to real-life cryptographic protocols, discovering so new vulnerabilities related to nonce misuses in Dragonfly, WPA3, and Bluetooth.
Cyber-physical systems are increasingly deployed in safety-critical applications, making their robustness under adversarial conditions a critical concern. Among the diverse range of threats, timed attacks, i.e., attacks triggered at particular timing, pose a unique challenge due to their ability to disrupt system behaviors in subtle and complex ways. In this paper, we propose a formal framework for quantitative analysis of the robustness of system's safety against timed attacks on cyber-physical systems modeled via the formalism of hybrid programs and differential dynamic logic. We introduce a series of timing related properties to characterize the robustness of safety against timed attacks, and develop a system of reasoning techniques, with a focus on the timing of dynamics, to establish these properties. We showcase the reasoning techniques with a case study on a water tank system with non-trivial dynamics.
Information-flow control systems often enforce progress-insensitive noninterference, as it is simple to understand and enforce. Unfortunately, real programs need to declassify results and endorse inputs, which noninterference disallows, while preventing attackers from controlling leakage, including through progress channels, which progress-insensitivity ignores. This work combines ideas for progress-sensitive security with secure downgrading (declassification and endorsement) to identify a notion of securely downgrading progress information. We use hyperproperties to distill the separation between progress-sensitive and progress-insensitive noninterference and combine it with nonmalleable information flow, an existing (progress-insensitive) definition of secure downgrading, to define nonmalleable progress leakage (NMPL). We present the first information-flow type system to allow some progress leakage while enforcing NMPL, and we show how to infer the location of secure progress downgrades. All theorems are verified in Rocq.
As data-driven technologies advance swiftly, maintaining strong privacy measures becomes progressively difficult. Conventional (epsilon, delta)-differential privacy, while prevalent, exhibits limited adaptability for many applications. To mitigate these constraints, we present alpha differential privacy (ADP), an innovative privacy framework grounded in alpha divergence, which provides a more flexible assessment of privacy consumption. This study delineates the theoretical underpinnings of ADP and contrasts its performance with competing privacy frameworks across many scenarios. Empirical assessments demonstrate that ADP offers enhanced privacy guarantees in small to moderate iteration contexts, particularly where severe privacy requirements are necessary. The suggested method markedly improves privacy-preserving methods, providing a flexible solution for contemporary data analysis issues in a data-centric environment.
Aggregate signatures are digital signatures that compress multiple signatures from different parties into a single signature, thereby reducing storage and bandwidth requirements. BLS aggregate signatures are a popular kind of aggregate signature, deployed by Ethereum, Dfinity, and Cloudflare amongst others, currently undergoing standardization at the IETF. However, BLS aggregate signatures are difficult to use correctly, with nuanced requirements that must be carefully handled by protocol developers. In this work, we design the first models of aggregate signatures that enable formal verification tools, such as Tamarin and ProVerif, to be applied to protocols using these signatures. We introduce general models that are based on the cryptographic security definition of generic aggregate signatures, allowing the attacker to exploit protocols where the security requirements are not satisfied. We also introduce a second family of models formalizing BLS aggregate signatures in particular. We demonstrate our approach's practical relevance by modelling and analyzing in Tamarin a device attestation protocol called SANA. Despite SANA's claimed correctness proof, with Tamarin we uncover undocumented assumptions that, when omitted, lead to attacks.
Software-Defined Networking (SDN) has transformed network architectures by decoupling the control and data-planes, enabling fine-grained control over packet processing and forwarding. P4, a language designed for programming data-plane devices, allows developers to define custom packet processing behaviors directly on programmable network devices. This provides greater control over packet forwarding, inspection, and modification. However, the increased flexibility provided by P4 also brings significant security challenges, particularly in managing sensitive data and preventing information leakage within the data-plane. This paper presents a novel security type system for analyzing information flow in P4 programs that combines security types with interval analysis. The proposed type system allows the specification of security policies in terms of input and output packet bit fields rather than program variables. We formalize this type system and prove it sound, guaranteeing that well-typed programs satisfy noninterference. Our prototype implementation, Tap4s, is evaluated on several use cases, demonstrating its effectiveness in detecting security violations and information leakages.
The implementation of security protocols often combines different languages. This practice, however, poses a challenge to traditional verification techniques, which typically assume a single-language environment and, therefore, are insufficient to handle challenges presented by the interplay of different languages. To address this issue, we establish principles for combining multiple programming languages operating on different atomic types using a symbolic execution semantics. This facilitates the (parallel) composition of labeled transition systems, improving the analysis of complex systems by streamlining communication between diverse programming languages. By treating the Dolev-Yao (DY) model as a symbolic abstraction, our approach eliminates the need for translation between different base types, such as bitstrings and DY terms. Our technique provides a foundation for securing interactions in multi-language environments, enhancing program verification and system analysis in complex, interconnected systems.
The rise of 5G and IoT has shifted secure communication from centralized and homogeneous to a landscape of heterogeneous mobile devices constantly travelling between myriad networks. In such environments, it is desirable for devices to securely extend their connection from one network to another, often referred to as a handover. In this work we introduce the first cryptographic formalisation of secure handover schemes. We leverage our formalisation to propose path privacy, a novel security property for handovers that has hitherto remained unexplored. We further develop a syntax for secure handovers, and identify security properties appropriate for secure handover schemes. Finally, we introduce a generic handover scheme that captures all the strong notions of security we have identified, combining our novel path privacy concept with other security properties characteristic to existing handover schemes, demonstrating the robustness and versatility of our framework.
Strand spaces are a formal framework for symbolic protocol verification that allows for pen-and-paper proofs of security. While extremely insightful, pen-and-paper proofs are error-prone, and it is hard to gain confidence on their correctness. To overcome this problem, we developed StrandsRocq, a full mechanization of the strand spaces in Coq (soon to be renamed Rocq). The mechanization was designed to be faithful to the original pen-and-paper development, and it was engineered to be modular and extensible. StrandsRocq incorporates new original proof techniques, a novel notion of maximal penetrator that enables protocol compositionality, and a set of Coq tactics tailored to the domain, facilitating proof automation and reuse, and simplifying the work of protocol analysts. To demonstrate the versatility of our approach, we modelled and analyzed a family of authentication protocols, drawing inspiration from ISO/IEC 9798-2 two-pass authentication, the classical Needham-Schroeder-Lowe protocol, as well as a recently-proposed static analysis for a key management API. The analyses in StrandsRocq confirmed the high degree of proof reuse, and enabled us to distill the minimal requirements for protocol security. Through mechanization, we identified and addressed several issues in the original proofs and we were able to significantly improve the precision of the static analysis for the key management API. Moreover, we were able to leverage the novel notion of maximal penetrator to provide a compositional proof of security for two simple authentication protocols.
