ABSTRACT. Diffie-Hellman groups are commonly used in cryptographic protocols. While most state-of-the-art, symbolic protocol verifiers support them to some degree, they do not support all mathematical operations possible in these groups. In particular, they lack support for exponent addition, as these tools reason about terms using unification, which is undecidable in the theory describing all Diffie-Hellman operators. In this paper we approximate such a theory and propose a semi-decision procedure to determine whether a protocol, which may use all operations in such groups, satisfies user-defined properties. We implement this approach by extending the Tamarin prover to support the full Diffie-Hellman theory, including group element multiplication and hence addition of exponents. This is the first time a state-of-the-art tool can model and reason about such protocols. We illustrate our approach’s effectiveness with different case studies: ElGamal encryption and MQV. Using Tamarin, we prove security properties of ElGamal, and we rediscover known attacks on MQV.

ABSTRACT. In symbolic models, equational theories are used to model the algebraic primitives of cryptographic primitives. Automated verification tools however only handle limited classes of equational theories to avoid performance and termination issues. In particular associative and commutative (AC) symbols have often been problematic, although they are common, e.g., to model addition, multiplication, exclusive-or (XOR), multisets, etc. In this paper we extend the Tamarin prover to allow users to specify AC symbols as part of their user-defined equational theory. To avoid termination issues, we propose a novel property that bounds certain deduction chains. We use Tamarin’s deduction algorithm to verify whether this bound is indeed correct for a given equational theory, generalizing previous work. Moreover, our work allowed to identify that Tamarin’s built-in XOR used an optimization that may lead to incorrect results, and would have influenced our results as well. Simply disabling the optimization results in non-termination on a significant fraction of examples from the Tamarin repository. We therefore design a new constraint reduction rule that discards some redundant constructor chains, and prove its correctness. We illustrate the effectiveness and efficiency of our approach using different examples, including XOR, multisets, reencryption, Diffie-Hellman exponentiation, and distributed decryption. It turns out that our property holds for all these examples, and that, compared to Tamarin’s built-in support for XOR or multisets, our approach only incurs a small overhead on startup when checking the property, but otherwise has similar performance on most examples. Re-encryption and distributed decryption were previously out of scope, and our model for Diffie-Hellman exponentiation, albeit simpler than the built-in, allows for the exponentiation symbol to be reused in further equations, which is not allowed for the built-in one.

ABSTRACT. Network protocol fingerprinting is used to identify a protocol implementation by analyzing its input-output behavior. Traditionally, fingerprinting operates under a closed-world assumption, where models of all implementations are assumed to be available. However, this assumption is unrealistic in practice. When this assumption does not hold, fingerprinting results in numerous misclassifications without indicating that a model for an implementation is missing. Therefore, we introduce an open-world variant of the fingerprinting problem, where not all models are known in advance. We propose an incremental fingerprinting approach to solve the problem by combining active automata learning with closed-world fingerprinting. Our approach quickly determines whether the implementation under consideration matches an available model using fingerprinting and conformance checking. If no match is found, it learns a new model by exploiting the structure of available models. We prove the correctness of our approach and improvements in asymptotic complexity compared to naive baselines. Moreover, experimental results on a variety of protocols demonstrate a significant reduction in misclassifications and interactions with these black-boxes.

ABSTRACT. Security protocols are concurrent processes that communicate using cryptography to achieve various security properties. Their formal verification has been the subject of much research, which has led to a number of successful tools. Several of these tools use variants of the applied pi-calculus as an input language to model protocols, though the internal representation used for verification may vary. The translation from processes to their internal representation has received relatively little attention despite its important role in the soundness and efficiency of the security analyses. We consider this problem within the Squirrel prover framework, where processes are translated to so-called systems of actions, which serve as the basis for a logic-based verification technique. Intuitively, actions consist of groups of elementary instructions. We provide a general theory for grouping instructions in a way that preserves both indistinguishability and trace properties, and we instantiate it to obtain a new translation procedure for Squirrel. We have implemented our procedure as a replacement of the original (unsound) translation, demonstrating that it can serve as an almost drop-in replacement in existing case studies.

ABSTRACT. The Lightweight Directory Access Protocol (LDAP) plays a crucial role in modern enterprise infrastructure for centralized authentication and authorization, yet lacks comprehensive formal verification. We develop a formal model capturing LDAP and its most popular authentication mechanisms (Simple Bind, SASL PLAIN, SASL-CRAM-MD5, SASL SCRAM- SHA-256 and SASL SCRAM- SHA-256-PLUS ). We bridge the gap between this formal model and the most widely used implementation of the protocol, OpenLDAP, by monitoring it using the SpecMon framework. We instrument the cryptographic library to generate an event stream which SpecMon continuously checks for compliance with the model. We use Tamarin to prove authentication properties, which thus transfer to OpenLDAP.

ABSTRACT. Ideal functionalities are used to study increasingly complex protocols within the Universal Composability framework. However, such functionalities are often complex themselves, making it difficult to assess whether they truly fulfill their promises. In this paper, we present four attacks on functionalities from various applications (e-voting, SMPC, anonymous lotteries, and smart metering), demonstrating that they do not capture the intuitively expected properties. We argue that ideal functionalities should not merely be justified secure at a high level but rigorously proven to be so. To this end, we propose a methodology that combines game-based proofs and computer-aided verification: ideal functionalities can in fact be treated as protocols, and one can use traditional game-based proofs to study them, where any game-based security property proven on the functionality does transfer to any protocol that realizes it. We also propose fixed versions of the ideal functionalities we studied, and formally define the security properties they should satisfy through a game. Finally, using Squirrel, a proof assistant for protocol security, we formally prove that the fixed functionalities verify the specified game-based security properties.

ABSTRACT. We present a formally-verified (in Lean 4) framework for translating symbolic cryptographic proofs into the computationally-sound ones. Symbolic cryptography is a well-established field that allows reasoning about cryptographic protocols in an abstract way and is relatively easy to verify using proof assistants. Unfortunately, it often lacks a connection to the computational aspects of real-world cryptography. Computationally-sound cryptography, on the other hand, captures this connection much better, but it is often more complex, less accessible, and much harder to verify formally. Several works in the past have provided a bridge between the two, but, to our knowledge, none of them have been implemented in a proof assistant. We close this gap by formalizing the translation from symbolic to computationally-sound cryptography in Lean 4. Our framework is based on the work of Micciancio (Eurocrypt, 2010) and Li and Micciancio (CSF, 2018), which builds on the idea of using co-induction (instead of induction) for reasoning about an adversary's knowledge in a symbolic setting. Our work encompasses (1) the formalization of the symbolic cryptography framework, (2) the formalization of the computationally sound cryptography framework, and (3) the formalization of the translation between the two. We also provide (4) an extended example of circuit garbling, which is a well-known cryptographic protocol frequently used in secure multi-party computation. We believe that our work will serve as a foundation for future research in the area of formal verification of cryptographic protocols, as it enables reasoning about cryptographic protocols more abstractly while still providing a formally verified connection to the computational aspects of real-world cryptography.

ABSTRACT. Hybrid arguments are prevalent in cryptographic security proofs, however, existing mechanizations in proof assistants are not as general as they could be. In this paper, we prove a general theorem about the admissibility of hybrid arguments that encompasses the query-counting, multi-instance, and nested case. We present three case studies about public-key encryption, which demonstrate the generality of the theorem. The results of this paper are achieved in the setting of state-separating proofs and the theory is integrated into and the case studies are mechanized in Nominal-SSProve.

ABSTRACT. Computer-aided cryptography (CAC) provides strong guarantees through mechanized proofs of security. Squirrel is a proof assistant specialized in CAC, but is restricted to the asymptotic setting, which limits its applicability. Recent theoretical work adapted Squirrel’s underlying logic to the concrete setting through the introduction of a higher-order logic with errors. While this allows to prove precise security bounds on paper, it only provides a low-level logical calculus which lacks an implementation. Thus, it falls short of the CAC aims. In this paper, we use this low-level calculus to build the full-fledged set of features used in a proof assistant such as Squirrel, focusing on reachability reasoning. We design higher-level logical mechanisms on top of this logic, including proof context management, introduction patterns, and bound-annotated tactics. To do so, we need to introduce a proof term calculus with dedicated features for bounds, for which we design an elaborator. This elaborator automatically infer most bound-related manipulations, improving usability and reducing user inputs, and we theoretically argue for its usability through an erasability theorem. All these improvements have been implemented in Squirrel, and we provide empirical evidence of the applicability of our framework through case studies.

ABSTRACT. Formal methods are becoming an important tool for ensuring correctness and security of cryptographic constructions. However, the support for certain advanced proof techniques, namely rewinding, is scarce among existing verification frameworks, which hinders their application to complex schemes such as multi-party signatures and zero-knowledge proofs. We expand the support for rewinding in EasyCrypt by implementing a version of the general forking lemma by Bellare and Neven. We demonstrate its usability by proving EUF-CMA security of Schnorr signatures.

ABSTRACT. We propose a variant of classic information flow analysis that permits transmission of secrets over a public network, provided that secrets are suitably encrypted. In the style of Dolev and Yao, the intruder controls the network, observing all messages sent, but can only decrypt messages for which they know the decryption key, i.e., those keys which correspond to the security level of the intruder. In contrast to similar previous works we allow the intruder to send arbitrary bit strings as input to the program without any assumption that these inputs are in some sense well-typed. This means that cryptographic messages can enter program variables that were not meant to hold cryptographic messages and become part of computations and conditions. Despite this strong intruder model, we show that a program that satisfies our information-flow analysis also enjoys Dolev-Yao noninterference, a variant of standard noninterference where the intruder cannot break cryptography. The underlying model, which combines operating on actual bit strings with a symbolic intruder model, and the entire result are formalized and proved in Isabelle/HOL.

ABSTRACT. Gradual typing effectively combines the advantages of dynamic and static typing and is utilized in Information Flow Control. The gradual guarantee ensures that removing type annotations does not affect runtime behavior. However, Toro et al. identify a tension between the gradual guarantee and noninterference, leading many gradual security-typed languages to reconcile these two properties. Recently, Chen and Siek’s language λIFC achieves both properties. Nevertheless, their cast calculus suffers from scalability issues and lacks binary operators, which limits its practical use. In this paper, we present a partial cast calculus λp for gradual information security based on the concept of partial label. Partial labels serve as concise representations for security coercions and runtime labels, which simplify the definition of operators related to security labels and facilitate cast reductions within the semantics of λp. Consequently, this calculus effectively support binary operators and can be readily extended to accommodate more complex sets of security labels. We prove both noninterference and the gradual guarantee for λp. Furthermore, we explore extensions concerning the accommodation of unknown references and a semantic interpretation of our partial labels.

ABSTRACT. We present CryptoChoreo, a choreography language for the specification of cryptographic protocols. Choreographies can be regarded as an extension of Alice-and-Bob notation, providing an intuitive high-level view of the protocol as a whole (rather than specifying each protocol role in isolation). The extensions over standard Alice-and-Bob notation that we consider are non-deterministic choice, conditional branching, and mutable long-term memory. We define the semantics of CryptoChoreo by translation to a process calculus. This semantics entails an understanding of the protocol: it determines how agents parse and check incoming messages and how they construct outgoing messages, in the presence of an arbitrary algebraic theory and non-deterministic choices made by other agents. While this semantics entails algebraic problems that are in general undecidable, we give an implementation for a representative theory. We connect this translation to ProVerif and show on a number of case studies that the approach is practically feasible.