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.
