ABSTRACT. We develop a type system for secure information flow where new security levels can be created and inserted into the security lattice \emph{dynamically}, i.e., even in the middle of an execution of a system. Our system is formalized by extending Kobayashi's type-based secure information flow analysis for Milner's pi-calculus, which is one of the most expressive models (or ``languages'') supporting both sequential and concurrent computations, with concise syntax, reduction-based semantics, and bisimulation equivalence as a robust formalization of secrecy as non-interference. The development required careful treatment of extensions of lattices themselves as well as deliberate generalization from the simple 2-element lattice (consisting of only High and Low) in the original system.

ABSTRACT. We define a security-typed lambda-calculus with declassification, and develop an environmental bisimulation proof technique for secure information flow in this setting. Unlike traditional security typing that enforces full noninterference, our bisimulation allows proving conditional, intentionally weakened noninterference properties while correctly ``leaking'' (or publishing) part of the high-security information. Despite the long history of this research area and previous work on declassification, this is, to our knowledge, the first result of such a direct approach to the problem of proving noninterference in a higher-order language with declassification. Our technical development is based on novel treatment of \texttt{if}-branches whose conditions are of high secrecy.

ABSTRACT. Attestation means providing evidence that a remote target system is worthy of trust for some sensitive interaction. Although attestation is already used in network access control, security management, and trusted execution environments, it mainly concerns only a few system components. A clever adversary might manipulate these shallow attestations to mislead the relying party. Reliable attestations require layering. We construct attestations whose layers report evidence about successive components of the target system. Reliability also requires structuring the target system so only a limited set of components matters. We show how to structure an example system for reliable attestations despite a well-defined, relatively strong adversary. It is based on widely available hardware, such as Trusted Platform Modules, and software, such as Linux with SELinux. We isolate our principles in a few maxims that guide system development. We provide a cogent analysis of our mechanisms against our adversary model, as well as an empirical appraisal of the resulting system. The performance burden of our attestation is negligible, circa~1.3%. After our first example, we vary our application level, and then also its underlying hardware anchor to use confidential computing with AMD's SEV-SNP. The same maxims help us achieve trustworthy attestations. Keywords. Layered Attestation; Run-Time Attestation; Hardware-based attestation; Copland; Cross-Domain Solutions

ABSTRACT. We verify the `extendedGCD` implementation in Go's standard library (`crypto/internal/fips140/bigmod`), which plays a crucial role in the generation of RSA key pairs. Even though the Go implementation is supposedly a direct port from BoringSSL's implementation, we uncovered two deviations that each break the algorithm's invariants: (1) the Go implementation deviates in the way coefficients are updated, and (2) it permits a larger input domain. We address both deviations; the first by fixing the Go implementation, which results in an on average 24% speedup, and the second deviation by porting an existing proof for BoringSSL and extending it to cover the larger input domain. We prove correctness and termination of the fixed Go implementation using Gobra, a deductive program verifier for Go. Where necessary, we used Lean to prove key lemmata on non-linear arithmetic, which we import into Gobra. Our verification effort reveals three key insights: subtle bugs can slip into even well-reviewed code with surprising ease; formal verification is a powerful tool for uncovering them; and AI agents can facilitate the verification process by iteratively refining invariants and lemmata based on Gobra's error messages.

ABSTRACT. The FS-FS hybrid signature scheme by Bindel and Hale (2023) combines two Fiat-Shamir components through a single shared challenge. Its EUF-CMA security is stated as a theorem in that work-in-progress, but no proof is provided. We report an EasyCrypt mechanisation of the FS-FS security argument in the Random Oracle Model (ROM), defined over abstract Fiat-Shamir components and instantiated with Schnorr, with ongoing work toward broader instantiations and the QROM. The formalisation yields two distinct insights. First, the second-preimage resistance assumption appearing in the original theorem statement is subsumed by the standard ROM guessing bound. Second, establishing the reduction in EasyCrypt requires two additional proof obligations: a logging invariant for the guessing branch and a tracker invariant for the collision-resistance reduction. Together, these obligations reveal proof-structural complexity introduced by the shared challenge that is absent from single-component Fiat-Shamir signatures.

ABSTRACT. The EasyCrypt proof assistant has been used to successfully formalize security proofs for a wide variety of cryptographic primitives. However, attempts at formalizing objects with interactivity, such as protocols, have fared much worse. In this paper, we investigate (some of) the reasons for this difficulty by formalizing a simple interactive key agreement protocol. From a first complete but exploratory proof, to a failed attempt at a structured proof, and to what we believe is an ``essential'' proof, we identify which proof features contribute most to the complexity of formalization in pRHL. In particular, we argue that difficulties in formalizing the security of interactive protocols in the computational model arise from the fact that such proofs rely on both state and temporal invariants---the former to support cryptographic reasoning, and the latter to support reasoning about the protocol's structure. We believe that this observation can help build new reasoning tools that can bridge the gap that currently exists between primitive-focused tools and protocol-focused tools.

ABSTRACT. Implementations of cryptographic primitives need to be both unquestionably secure and highly performant. The second requirement often leads library writers to craft hand-optimized assembly code, which significantly complicates the use of formal methods to satisfy the first requirement. We propose that decompilation techniques can be used to lift cryptographic code written in assembly to Jasmin, a language designed for high-assurance cryptography, and machine-checked for conformance against verified reference implementations, potentially offering comparable guarantees; and evaluate the viability of our approach with case studies drawn from mainstream cryptographic libraries.

ABSTRACT. Frontrunning is a smart contract vulnerability that stems from the non-synchronous nature of blockchain transaction processing. Traditional approaches to detecting frontrunning in smart contracts rely on the notion of Transaction Order Dependence (TOD). A smart contract is considered to have TOD if the result of two contract calls may vary with their execution order. However, TOD does not serve as an accurate predictor for frontrunning vulnerabilities, as it disregards that honest users may purposefully limit contract calls to situations where reordering cannot be harmful. Following this observation, we develop the first frontrunning analysis tool that combines program analysis of a smart contract with protocol analysis for modeling honest user strategies.

ABSTRACT. Blockchain-based distributed consensus enables mutually mistrusting users to jointly realize decentralized services. Cryptocurrencies like Bitcoin or Ethereum use this technology to implement decentralized payment systems and computing platforms. These systems, however, suffer from scalability drawbacks: the underlying consensus mechanism inherently limits their throughput, causing long transaction processing times and transaction costs when scaling them up to large user numbers. A promising approach to mitigate these scalability issues are so-called off-chain protocols. In off-chain protocols, users exchange cryptographic information, which enables them to securely batch multiple transactions, such that their effect can be enforced with a small number of on-chain transactions that are processed by the consensus. Prominently, payment channels use such a mechanism to enable fast and cheap bilateral payments between users. While bringing practical benefits, off-chain protocols are hard to design securely: E.g., payment channel users only enjoy security guarantees if they meet channel-specific deadlines, and constantly monitor the blockchain to detect and punish misbehaviour of the channel counterparty. Small design flaws (e.g., a miscalculated deadline) can immediately result in the loss of user funds. Despite these complexities, so far, there exist no frameworks that help protocol designers in the secure design and verification of those protocols. To help this, we make the following contributions: (1) We present Renegade, an intermediate language for designing blockchain protocols - cryptographic protocols that involve blockchain interactions; (2) We present a compilation from Renegade protocols into blockchain protocols for Bitcoin. The compilation is general enough to be extended to many other cryptocurrencies as compilation targets; (3) We provide a computational soundness proof, showing that all behaviour of compiled protocols in a computational model of cryptography is captured by the symbolic Renegade protocol semantics; (4) We implement the Renegade semantics in the proof assistant Rocq, and conduct a case study, demonstrating Renegade’s utility in reasoning about state-of-the art payment channel protocols. The work presented in this paper is in progress.

ABSTRACT. The advent of quantum computers has initiated both research and standardization efforts toward the development of cryptographic primitives and communication protocols that remain secure against attackers equipped with quantum computers. Computer-aided verification has proven valuable in this context, as it helps identify flaws early and strengthens confidence in cryptographic systems. However, existing verification tools are typically designed for a specific attacker model (most often polynomial-time Turing machines in line with classical cryptographic assumptions) and therefore require adaptation to accurately capture the quantum setting. In this work, we present a novel post-quantum extension of Squirrel, a proof assistant that provides computational guarantees for cryptographic primitives and protocols. Our extension is fully embedded in the higher-order logic underlying Squirrel, allowing logical terms to directly represent quantum values. This design choice makes the extension generic, preserves compatibility with the latest features of Squirrel, and supports its long-term integration into the tool. We implement our approach within Squirrel and validate it through several case studies. In particular, we obtain post-quantum security guarantees for multiple KEM combiners, as well as for two hybrid key-exchange protocols.

ABSTRACT. Security proofs for cryptographic protocols are notably complex and error-prone, in particular in the computational model. Computer-aided cryptography aims at increasing the confidence in these proofs, by mechanising them and formally verifying them with automated tools. One such tool is the Squirrel proof assistant. In this paper, we use it to prove the Post-Compromise Security (PCS) of an asymmetric ratchet mechanism used to generate shared keys, such as the one featured in the Signal protocol. While Squirrel is convenient to study stateful protocols such as the ratchet, the analysis his is made particularly challenging by the fact that the usual notion of secrecy for Squirrel, i.e. real-or-random secrecy, is not well-suited to that protocol. We instead define predicates and a proof system for non-deducibility, a weaker notion of secrecy, which we found to be the notion needed to study the asymmetric ratchet. We establish the soundness of the proof system, implement it within the Squirrel prover, and use it to write a proof of PCS for the asymmetric ratchet, which is the first mechanised such proof.