ABSTRACT. Single Sign-On (SSO) protocols allow an identity provider to authenticate users and report the outcome by issuing identity attestations. Recent attacks show that breaching the identity provider infrastructure enables adversaries to issue arbitrary identity attestations and impersonate users. Survivable SSO protocols limit the risks of similar intrusions, but they have only been defined for password-based authentication, inheriting their limitations against powerful attacks such as credential phishing. While phishing-resistant passwordless authentication protocols have been standardized, they are not designed to guarantee intrusion tolerance. We initiate the research for Survivable Passwordless SSO (SPS) and propose a modular approach which includes the novel definition of Survivable Passwordless Challenge-response (SPC) protocols for authentication as a sub-routine of SSO. We give the first frameworks and game-based security definitions both for SPC and SPS which capture both novel attack classes, such as session injection attacks in a decentralized setting, and existing but not yet formalized attack classes, such as detection of cloned authenticators. The design of the models includes novel strategies to capture proactive security in survivable protocols within security definitions and to compose authentication and SSO through a modular approach. Our strategies and models may also be applied with minor modifications to non-survivable protocols, possibly providing a novel approach to assess the security of existing SSO protocols.

ABSTRACT. This paper presents a formal framework for enhancing privacy in decentralized identity (DID) systems, resolving the inherent conflict between blockchain verifiability and the principle of minimal data disclosure. At its core, we introduce a provably secure cryptographic protocol that leverages attribute commitments on-chain and zero-knowledge proofs for off-chain validation. This approach allows users to demonstrably prove the validity of predicates about their attributes without revealing the underlying sensitive values. We formally define the security and privacy requirements for such a system—including consistency, attribute-based indistinguishability, and predicate-based indistinguishability—within a semi-honest adversarial model. We then construct a concrete scheme that realizes these properties under standard cryptographic assumptions. The proposed architecture is designed for full backward compatibility with W3C DID standards, ensuring practical deployability. Security analysis provides rigorous, provable guarantees, while performance evaluation confirms the efficiency of the core cryptographic operations, supporting its use in resource-constrained environments. This work establishes a foundational and analyzable basis for building decentralized identity systems where both accountability and user privacy are essential.

ABSTRACT. Existing Capture-the-Flag (CTF) platforms trust a single organizer, offer limited auditability, and are vulnerable to infrastructure-level manipulation. We propose zk–MPSFV, a zk-SNARK-based, multi-phase sub-flag verification scheme that replaces centralized scoring with an on-chain, zero-knowledge, publicly verifiable scoreboard. Challenges are decomposed into sub-challenges arranged as a directed acyclic graph (DAG): a team unlocks the next step only after proving completion of all parent nodes. Sub-flags and decryption keys are jointly generated by n organizers and released via an off-chain (t, n) Shamir–BLS threshold signature produced through multi-party computation (MPC), preventing any single organizer from leaking or altering keys. Teams submit zk-PLONK proofs that the contract verifies, timestamps, and records immutably. Under standard assumptions (collision-resistant hashing, SNARK soundness/zero-knowledge, IND-CCA2 ECIES, and at least t honest organizers), we prove that zk–MPSFV achieves the stated security goals, including DAG-gated progress, anti-replay, and threshold-robust organizer security, while out-of-band flag sharing remains out of scope. On a three-organizer testbed with 30 simulated teams, setup costs 0.45 ms per sub-flag, proof generation averages 5.34 s on an 8-core system, and on-chain verification costs ≈ 170k L2 gas on zkSync Era with a median fee of 1.33×10−6 ETH (about $0.0046 at $3,435/ETH). Stress replays sustain ≈ 7 proof transactions/s up to 5000 proofs; extrapolating to 50,000 proofs (1000 teams× 50 submissions) yields ≈ 0.0665 ETH (about $200–$228) and ≈ 2 hours of settlement time. Overall, zk–MPSFV is practical for small- to mid-scale, audit-ready progression CTFs.

ABSTRACT. Attack trees (ATs) are popular graphical models for reasoning about the security of complex systems, allowing for the quantification of risk through so-called AT metrics. A large variety of different such AT metrics have been proposed, and despite their wide-spread practical use, no systematic treatment of attack tree metrics so far is fully satisfactory. Existing approaches either fail to include important metrics, or they are too general to provide a useful systematic way for defining concrete AT metrics, giving only an abstract characterisation of their behaviour. We solve this problem by developing a compositional theory of ATs and their functorial semantics based on gs-monoidal categories. Viewing attack trees as string diagrams, we show that components of ATs form a channel category, a particular type of gs-monoidal category. AT metrics then correspond to functors of channel categories. This characterisation is both general enough to include all common AT metrics, and concrete enough to define AT metrics by their logical structure.

ABSTRACT. Active cyber defense offers a promising approach to addressing the longstanding asymmetry between rapidly evolving cyber threats and static defense systems. However, active cyber defense requires fast responses and proactive reconfigurations that must be verified and tailored to observed attacker be- haviour. Formal methods rely on rigorous mathematical and logical frameworks for verifying system specifications under well- defined assumptions. In particular, multi-agent system (MAS) verification, which examines formal properties of open systems, is well-suited for cybersecurity where attacker–defender inter- actions are central. This paper bridges the gap between system security modelling and MAS verification, providing active defense orchestration with formal guarantees. Our contributions are (i) a general methodology for controlling active cyber defenses with formally verified specifications based on the attack–defense movement model (ADM), a new model of attacker and defender actions, (ii) an application of this methodology for adaptive honeypot control, which relies on a MAS logic contribution to express strategic properties such as attacker attribution, and (iii) VeriPot, a tool which implements the honeypot adaptation strategy extraction from the ADM.

ABSTRACT. Attack Trees (ATs) are widely used to model and analyze security risks. Quantitative AT analysis can furthermore express risk with multiple metrics such as required attacker cost, time, and skill. This gives a detailed security assessment of the system as a whole, but does not come with a notion of which attacks are most critical. Understanding such criticality can significantly contribute to risk prioritization. To fill these gaps in AT, we propose Importance Measures (IMs) for ATs that quantify how important a single attack step is to the overall success or likelihood of the attack. We analyze cost- and probability-based attack models that reflect common operational scenarios among researchers, such as persistent adversaries against systems with limited detection capabilities and single-attempt attacks in high-security environments. Our framework supports arbitrary monotone metrics and provides a framework allowing the study of many metrics. We apply our proposed framework to a real-world case study taken from the MITRE ATT&CK knowledge source. Our results show how importance measures can identify high-leverage attack steps that substantially reduce attacker effort or increase success probability, and how defenders can use our approach to prioritize mitigations under limited resources.