Institute of Information Security University of Stuttgart Universitätsstraße 38 D–70569 Stuttgart Masterarbeit Analysis of Selected Cryptographic Protocols with DY* Samuel Holderbach Course of Study: Softwaretechnik Examiner: Prof. Dr. Ralf Küsters Supervisor: Tim Würtele, M.Sc. Commenced: January 3, 2023 Completed: July 3, 2023 Abstract DY* is a framework implemented in the proof-oriented programming language F*, aiming at symbolic analysis of cryptographic protocols on the structural and on the implementation level. In this master’s thesis, we analyse three selected authentication and key exchange protocols with DY*: the Otway-Rees protocol, the Yahalom protocol and the Denning-Sacco protocol with public keys. Each of these protocols is designed to establish a secure channel between two users while involving a trusted third party in the authentication process. The Otway-Rees and Yahalom protocols rely on pre-shared symmetric keys with this trusted third party, while the Denning-Sacco protocol relies on digital signatures and public key encryption. In addition, the Denning-Sacco protocol proposes the use of timestamps in messages to provide users with guarantees about the timeliness of the conversation, a protocol feature that has not yet been attempted to be modeled and analyzed in DY*. We developed accurate models for each of the three protocols in DY*, documented possible attacks and proposed improvements to prevent them, and finally proved the security of the protocol or its improved version. We found several attacks on the Otway-Rees protocol that allow an adversary to impersonate one or possibly both of the users involved in the protocol, and based on these attacks, presented improvements to prevent them. For the Yahalom protocol, we show that it satisfies security goals derived from its formal specification, and draw parallels to other approaches with similar results. We also comment on the differences between our results and those of other analyses that describe the Yahalom protocol as flawed. Moreover, we developed an extension to DY* for modeling time-based properties of protocols with timestamps and demonstrated it on the Denning-Sacco protocol. As a result, we provide the first symbolic security proof, including timestamp-dependent security properties, of the Denning-Sacco protocol in DY*. 3 Kurzfassung DY* ist ein in der beweisorientierten Programmiersprache F* implementiertes Framework zur symbolischen Analyse von kryptographischen Protokollen auf der Struktur- und Implemen- tierungsebene. In dieser Masterarbeit analysieren wir drei ausgewählte Authentifizierungs- und Schlüsselaustausch- protokolle mit DY*: das Otway-Rees Protokoll, das Yahalom Protokoll und das Denning-Sacco Protokoll mit öffentlichen Schlüsseln. Jedes dieser Protokolle ist darauf ausgelegt, einen sicheren Kanal zwischen zwei Benutzern aufzubauen und dabei eine vertrauenswürdige dritte Partei in den Authentifizierungsprozess einzubeziehen. Die Protokolle Otway-Rees und Yahalom beruhen auf gemeinsam genutzten symmetrischen Schlüsseln mit dieser vertrauenswürdigen dritten Partei, während das Denning-Sacco Protokoll auf digitalen Signaturen und Verschlüsselung mit öffentlichen Schlüsseln beruht. Darüber hinaus schlägt das Denning-Sacco Protokoll die Verwendung von Zeitstempeln in Nachrichten vor, um den Benutzern Garantien in Bezug auf die Aktualität der Konversation zu geben – eine Protokolleigenschaft, die in DY* noch nicht modelliert und analysiert wurde. Wir haben präzise Modelle für jedes der drei Protokolle in DY* entwickelt, mögliche Angriffe dokumentiert und Verbesserungen vorgeschlagen, um sie zu verhindern, und schließlich die Sicherheit des Protokolls oder seiner verbesserten Version bewiesen. Wir konnten mehrere Angriffe auf das Otway-Rees Protokoll finden, die es einem Angreifer ermöglichen, sich als einer oder möglicherweise als beide am Protokoll beteiligten Benutzer auszugeben, und haben auf der Grundlage dieser Angriffe Verbesserungen zur Verhinderung derselben vorgestellt. Für das Yahalom Protokoll zeigen wir, dass es die aus seiner formalen Spezifikation abgeleiteten Sicherheitsziele erfüllt, und ziehen Parallelen zu anderen Ansätzen mit ähnlichen Ergebnissen. Wir kommentieren auch die Unterschiede zwischen unseren Ergebnissen und denen anderer Analysen, die das Yahalom Protokoll als unsicher bezeichnen. Darüber hinaus haben wir eine Erweiterung von DY* für die Modellierung zeitbasierter Eigenschaften von Protokollen mit Zeitstempeln entwickelt und diese am Denning-Sacco Protokoll demonstriert. Als Ergebnis liefern wir den ersten symbolischen Sicherheitsbeweis, einschließlich von Zeitstempeln abhängiger Sicherheitseigenschaften, für das Denning-Sacco Protokoll in DY*. 5 Contents 1 Introduction 17 2 Basics 21 2.1 Introduction to DY* . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 2.2 Authentication Protocols . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3 Related Work 31 3.1 Authentication Protocols . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 3.2 Symbolic Analysis Approach . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 3.3 Selected Protocols and Conducted Analyses . . . . . . . . . . . . . . . . . . . 33 4 Analysis of the Selected Protocols 43 4.1 General Procedure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 4.2 DY* Models and Source Code Repository . . . . . . . . . . . . . . . . . . . . 44 4.3 Otway-Rees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 4.4 Yahalom . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81 4.5 Denning-Sacco . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99 5 Conclusion and Outlook 129 Bibliography 133 A Output of the Otway-Rees Model 137 A.1 Benign Attacker Trace . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137 A.2 Impersonation Attacker Trace . . . . . . . . . . . . . . . . . . . . . . . . . . . 138 A.3 Traces of Intercept and Replay Attacks . . . . . . . . . . . . . . . . . . . . . . 140 A.4 Output and Trace of the Improved Model . . . . . . . . . . . . . . . . . . . . . 142 B Output of the Yahalom Model 145 C Output of the Denning-Sacco Model 147 C.1 Output and Trace of Benign Attacker . . . . . . . . . . . . . . . . . . . . . . . 147 C.2 Output and Trace of Fake Certificate Attacker . . . . . . . . . . . . . . . . . . 149 7 List of Figures 9 List of Tables 11 List of Listings 13 List of Algorithms 15 1 Introduction Since Needham and Schroeder [26] proposed the use of public and symmetric key encryption to authenticate communication entities – usually referred to as principals – in large computer networks, the field has received a great amount of attention by security researchers. Many protocols that use cryptography to achieve authentication have been proposed so far and at least as many flaws and attack vectors have been found on such protocols. In a benign environment it would be rather trivial to achieve authentication but not so in the case of a large and insecure network like the Internet. In the presence of powerful attackers that may control network traffic, read and tamper with messages or try to impersonate honest principals, authentication is a hard to achieve and very subtle property. Because of this, security researchers stressed the need of methods to verify the correctness of authentication protocols to ensure that their use in presence of such powerful attackers still leads to strong security guarantees between honest parties in the network. Methods that have been proposed so far, roughly divide into two fields. The first field is the field of computational analysis of the cryptographic primitives and their combination in cryptographic protocols, aiming to show their probabilistic security. This approach, however, requires a detailed understanding of these cryptographic primitives and possible attack vectors when combining them. Thus, such proofs are usually carried out in long and complex reduction or sequence of games proofs that require a huge amount of manual proof work and are hard to maintain. The other field attempts to analyze protocols at a higher, symbolic level by making strong security assumptions on the cryptographic primitives used in a protocol and finding attacks or proving certain security properties based on the specifications of protocols. This approach is called the symbolic analysis approach. Analysing Cryptographic Protocols: Symbolic Approach Dolev and Yao [17] pioneered in the field of symbolic protocol analysis with their model of a powerful symbolic attacker controlling the network, which has been used in many symbolic approaches that incorporate an active network attacker so far. Burrows et al. [11] proposed a logic based on believes of honest principals for the symbolic analysis of authentication protocols, known as BAN logic. The intention of the authors was to provide a formal logic to reason about principal’s believes throughout the execution of protocols and express authentication properties of protocols based on these believes. However, the logic was restricted to a context of honest principals, making it not so well suited when reasoning about other properties of cryptographic protocols such as secrecy. A more complete approach for security protocol verification was introduced by Ryan et al. [31] with the CSP approach. CSP is a process algebra that can be used to model parallel processes in which messages are exchanged. The work of Ryan et al. shows how CSP can be used in a trace 17 1 Introduction based approach – with a trace consisting of, e.g., messages sent, random numbers generated and events that can assist in the specification of security properties – to verify the correctness and security of cryptographic protocols. Moreover, the CSP approach allows for mechanical support of proofs via the automatic model checker FDR, making it less prone to errors in the analysis and also suited for more complex protocols. The CSP approach was also used by Lowe [23] to show, with the help of FDR, that the Needham-Schroeder public key protocol that was proposed in [26] is vulnerable to a man-in-the-middle attack. Automated Symbolic Analysis The ever growing number of new cryptographic protocols in the last twenty years has motivated the development of fast and fully automated symbolic provers for the verification of such protocols. Earlier tools like AVISPA [35] were already able to verify industrial-scale protocols within seconds and helped in the detection of some previously unknown attacks on protocols, e.g., from the ISO-PK family or the IKEv2 protocol with digital signatures. Newer provers like TAMARIN [25] can even account for protocol features like loops or mutable global state and capture all possible execution traces of a protocol within seconds, showing that they satisfy the security properties or giving a counter example (attack on the protocol). Automated provers can do within seconds, what would have required long and error prone manual proofs otherwise. However, there is a downside to the full automation of such proofs. Large protocols like TLS [30], which are an essential part of the infrastructure of the Internet today, must account for a variety of protocol modes and rounds. This makes it extremely inefficient or even impossible to perform an analysis of the whole protocol at once. In a non-modular approach like the one of TAMARIN, the time and memory required for the analysis of a protocol may grow exponentially with respect to the protocol’s size. In ratcheting protocols like the Signal protocol [29], where each key 𝐾𝑛+1 is recursively dependent on the previous key 𝐾𝑛, the complexity of the analysis grows with each ratcheting step. When considering an arbitrary number of rounds in the analysis, induction is required, a feature that is only supported in combination with some manual proof work in TAMARIN. Another problem with automated provers like TAMARIN is that they do not account for low-level implementation details given in the specifications of protocols that are often a root of attacks. For example, the Otway-Rees protocol [27] – one of the protocols analyzed with DY* as part of this master’s thesis – has been proved secure by a number of researchers (e.g., [4]) using symbolic or partially symbolic approaches that ignore low-level implementation details. However, the implementation of the protocol based on its original specification is at least vulnerable to an impersonation attack, resulting from a missing check of the identities in the plain text part of the second message by the authentication service. This attack and other attacks on the Otway-Rees protocol are described in Section 4.3.5. A more complete explanation of the disadvantages of fully automated symbolic provers, like TAMARIN, can be read in [6]. 18 DY* Framework DY* [6] is a framework for the analysis and verification of cryptographic protocols and cryptographic protocol code that aims to compensate for the problems of modern fully automated verification tools. The framework combines the approaches of using dependent type systems for the modular verification of cryptographic protocols with the approach of provers like TAMARIN that support automated trace-based verification. DY* models the global runtime semantics of protocols in terms of a mutable append-only global trace that tracks – in a sequential manner – all events that occur during the concurrent execution of arbitrary protocol sessions. This explicit notion of a global trace enables properties such as the knowledge of the attacker, secrecy lemmas about keys or random nonces, as well as assumptions about cryptographic primitives to be expressed and proved in terms of this trace and within the framework. This allows users of DY* to express and prove more fine-grained security properties, where the exact order of events on the trace matters, like perfect forward secrecy or post-compromise security, with the help of features such as long-lived mutable state and dynamic compromise. Protocol steps, unlike with many fully automated provers, can be modeled in full detail accounting for implementation details like message formats, message parsing and message validation (or the lack of validation), making it suitable for investigating real-world protocol implementations regarding their security. In fact, the authors of DY* have already used the framework for a detailed symbolic security analysis of the Signal protocol [6], which is used by messenger applications like WhatsApp. As a result of this analysis, they were able to provide the first mechanized proof of forward secrecy and post-compromise security in the Signal protocol over an unbounded number of protocol rounds. When new approaches for the symbolic analysis of cryptographic protocols arise, it is often interesting to demonstrate them on a couple of well-known protocols that are mainly of academic interest. On the one hand, to show that they are able to model basic properties of these protocols that are still found in many of today’s protocols, and on the other hand, to reason about differences and similarities in the analysis results compared to other approaches. It has already been demonstrated by the authors, that one can model Lowe’s attack on the NS-PK protocol in DY* and that the security of the proposed fix can be proven. However, there are still many protocols that could be interesting to reason about in DY*. Aim of this work The goal of this master’s thesis is to provide a symbolic analysis of three selected authentication protocols, using the DY* framework. In particular, we investigate the Otway-Rees protocol that was proposed by Otway and Rees in their attempt on Efficient and Timely Mutual Authentication [27], the Yahalom protocol, first specified by Burrows et al. in [11], and the Denning-Sacco protocol with public keys that was proposed by Denning and Sacco in their work on Timestamps in Key Distribution Protocols [16]. The analysis shows that the Otway-Rees protocol, based on its original specification, is vulnerable to multiple interception and impersonation attacks and that a fix proposed by Boyd and Mao [7] is not sufficient to prevent all found attacks. Therefore, we provide a minimal fix ourselves and prove it secure in DY* with respect to the security properties intended when the protocol was designed. We also use DY* to prove that the Yahalom and Denning-Sacco protocols are secure as long as none of the parties involved leaks secrets. Additionally, we present 19 1 Introduction an approach on how to include (security) properties about timestamps in our DY* models and demonstrate our approach based on the Denning-Sacco protocol by showing that session keys, that are compromised after their use, cannot be replayed. The outline of the rest of the thesis will be as follows: In Chapter 2 we discuss basics of the DY* framework as well as authentication protocols required for the analysis. Chapter 3 gives an overview over other (earlier) symbolic approaches used for the analysis of authentication protocols with a focus on analyses of the selected protocols. In Chapter 4, we model the selected protocols in DY*, reason about the models and prove their security or provide mitigations against discovered attacks. Finally, Chapter 5 summarizes our work and provides suggestions for improvements of DY* based on the performed analyses. 20 2 Basics The purpose of this chapter is to give a brief introduction to DY* and its aspects relevant for the analyses of the selected protocols performed in Chapter 4. We will, however, not cover all aspects of the framework in great detail. Thus, we refer to the paper of Bhargavan et al. [6] for a more general introduction to DY*. Furthermore, we discuss a few basics of authenticaton protocols in this chapter. 2.1 Introduction to DY* DY* is a framework for the verification and symbolic security analysis of cryptographic protocol code written in the programming language F* [18]. The F* programming language is a purely functional programming language with effects that aims at program verification. F* programs are verified with the help of an SMT solver and can be extracted to efficient OCaml, F# or C code and then executed. The novelty of DY* is that it bridges the gap between trace-based and type-based approaches of symbolic protocol analysis by using F*’s effects to explicitly model the global trace within the framework and by making use of the type system that F* offers. This provides the ability to express fine-grained security properties for our models in terms of the global trace, using features like long-lived mutable protocol state, fine-grained dynamic corruption, and events. Since F* is a general purpose programming language, we can also use DY* to detect flaws in implementation details of protocols, for example, in serialization and deserialization of messages. It has already been said in Chapter 1 how DY* is a modular approach for modeling and analysing cryptographic protocols. This modular approach also applies to the implementation of the framework itself. DY* is implemented via 9 verified F* modules that are organized into two layers. The lower layer is the symbolic runtime layer that provides libraries for low level features like symbolic cryptography, symbolic random number generation, storage and mutation of long-lived state (e.g., to store long term secrets or information regarding a particular protocol session) and the simulation of a network in which messages can be sent and received by principals. Moreover, it provides an API for the attacker, which is, as the name of the framework suggests, a Dolev-Yao symbolic attacker. The lower layer is already sufficient to create functional models of protocols in DY*. However, the framework also comprises a second layer on top of the symbolic runtime layer that allows for meaningful (security) proofs based on the semantics of the lower layer. Particularly, this higher layer introduces the concept of labels to ease the proof of security properties like key secrecy. 21 2 Basics Labels are essentially an over-approximation of the intended audience of a term, say, an encryption key. We could, for example, conclude that if the intended audience of a key does not contain a corrupted principal session1, this particular key is secret (not known to the attacker). In the following sections, the two layers are explained in more detail based on some selected examples in order to demonstrate how the most important protocol features like (de-)serialization, encryption and decryption, random number generation and state sessions can be modeled and what their semantics are. Further, we illustrate how we can build security proofs based on these features and their semantics. Symbolic Runtime Layer The essence of DY* is that principals run protocol code and exchange messages over an untrusted network, controlled by the Dolev-Yao attacker, in arbitrary many parallel sessions. Everything that happens within these protocol sessions is captured by a central component: the global execution trace. In particular, the global trace records the history of all principal state sessions, generated random numbers and sent messages. Additionally, it documents corrupted state sessions or versions of state sessions. Therefore, the trace determines the attackers knowledge at any point in time during the run of a protocol, which in turn, lets us precisely express security properties in terms of the trace. The trace is simply implemented as array of trace entries where each entry represents a protocol action: noeq type entry_t = | RandGen: b:bytes -> l:label -> u:usage -> entry_t | SetState: principal -> v:version_vec -> new_state:state_vec -> entry_t | Corrupt: corrupted_principal:principal -> session:nat -> version:nat -> entry_t | Event: sender:principal -> event -> entry_t | Message: sender:principal -> receiver:principal -> message:bytes -> entry_t type trace = Seq.seq entry_t The RandGen b l u trace entry represents the generation of random bytes b with intended audience l and usage u. The bytes type is the symbolic low-level respectively trace representation of data structures that may be used in protocols, e.g., literals, nonces, public keys, ciphertexts and messages, just to name a few. Usages tell us the scope in which a random value is or may be used; examples are nonce_usage or pke_usage. Intuitively, a random bytes value annotated with nonce_usage indicates that the value is simply used as nonce, while pke_usage means that the value is used as private decryption key in public key encryption. Next, SetState p v new_state holds a newly created or updated state of a principal p, where new_state is a vector of state sessions and v is a vector of versions matching the state sessions by index. State sessions can be used by principals to store, e.g., long-term private keys or current data associated with a particular protocol session. Versioning can be used to enable for even more fine-grained corruption, which can be helpful in proofs of subtle security properties 1Principals can have multiple independent sessions within their state storage that can be corrupted by the attacker. The corruption of one session only implies that the attacker gains knowledge of the terms in that particular session. We will discuss the concept of sessions later in more detail. 22 2.1 Introduction to DY* of protocols like forward secrecy or post-compromise security. Corruptions are notated by the Corrupt corrupted_principal session version entry, specifying which exact version of a principal’s session has been corrupted. The entry Event sender event shows the occurrence of a specific event during a protocol run; here, sender is the principal that “reported” the occurrence of the event. Events consist of a meaningful name and an array of associated data and can ease and assist in the formulation of security properties that require a specific order of certain protocol actions on the trace2. Finally, messages are represented by an entry Message sender receiver message, where sender and receiver are principals and message is usually a compound term. The symbolic runtime layer exposes an API with functions to perform the above protocol actions that will create the respective trace entries and append them to the global trace. For example, gen l u generates random bytes b with label l and usage u, creates a trace entry RandGen b l u, appends it to the global trace and finally outputs b. Analogous, there are functions to create and update a principal’s state or certain state sessions, corrupt a principal’s state or state sessions, trigger events or send and receive messages. The length of the global trace grows monotonically, so its length can be used as a symbolic timestamp in invariants and constraints on the trace, for example, to ensure that an event occurred or a message was sent before a given timestamp. The symbolic runtime layer defines an effect Crypto to capture these trace invariants in our protocol code. Functions we define that shall respect certain invariants on the trace are then defined in the Crypto effect, which comes with requires and ensures clauses to require properties of the input trace and to ensure properties of the resulting trace and the result of the computation, possibly depending on the input trace. Another central component of DY* that is part of the symbolic runtime model is the bytes type. It is a type for the symbolic low-level representation of data structures used in protocols; other symbolic approaches often call this concept a “term”. Terms or bytes can be atomic, e.g., a nonce that has been generated with the gen function, or they can be compound to build serialized messages or state sessions that can be sent across the network or stored in a principal’s state. The runtime layer offers concat and split functions to concatenate bytes or split them into their atomic parts. type literal = | ByteSeq of FStar.Seq.seq FStar.UInt8.t | String of string | Nat of nat type bytes_ = | Literal: literal -> bytes_ | Rand: n:nat -> l:label -> u:usage -> bytes_ | Concat: bytes_ -> bytes_ -> bytes_ | PK: secret:bytes_ -> bytes_ | PKEnc: pk:bytes_ -> n:bytes_ -> msg:bytes_ -> bytes_ | Extract: key:bytes_ -> salt:bytes_ -> bytes_ | Expand: key:bytes_ -> info:bytes_ -> bytes_ | AEnc: k:bytes_ -> iv:bytes_ -> msg:bytes_ -> ad:bytes_ -> bytes_ | VK: secret:bytes_ -> bytes_ | Sig: sk:bytes_ -> n:bytes_ -> msg:bytes_ -> bytes_ | Mac: k:bytes_ -> msg:bytes_ -> bytes_ | Hash: m:bytes_ -> bytes_ | DH_PK: s:bytes_ -> bytes_ 2This can be particularly useful when showing authentication properties, as we will see later. 23 2 Basics | DH: k:bytes_ -> s:bytes_ -> bytes_ Atomic bytes are either literals or random values. The concrete value of a literal can be a byte sequence, a string or a natural number. This definition of literals also allows for the extension of DY* with concrete implementations of, say, cryptography, in order to proof protocols secure under consideration of computational aspects. The symbolic runtime API has functions like string_to_bytes, bytes_to_string, nat_to_bytes, bytes_to_nat, etc., for the conversion of literals from and to its concrete values for use in higher-level data structures like message implementations that might determine the control flow in protocol steps. All other constructors of bytes create higher-order terms like public keys, ciphertexts, signatures, or even messages and state sessions. Thus, bytes do not only serve as a way to represent data within protocols but also carry the semantics of symbolic cryptographic primitives and of the model itself. To demonstrate this, let us have a look at how public key encryption has been realized in DY*: val pk:bytes -> bytes // interface let pk s = (PK s) // implementation val pke_enc:pub_key:bytes -> randomness:bytes -> msg:bytes -> bytes // interface let pke_enc p n s = (PKEnc p n s) // implementation val pke_dec:priv_key:bytes -> ciphertext:bytes -> result bytes // interface let pke_dec s c = // implementation match c with | PKEnc (PK s') n m -> if s = s' then Success m else Error "pke_dec: key mismatch" | _ -> Error "pke_dec: not a pke ciphertext" The pk function takes a secret key of type bytes as input and outputs the corresponding public key of type bytes. Under the hood, this is done by invoking the PK constructor of bytes. Symbolic public key encryption has been implemented with a function pke_enc that accepts inputs public key, randomness and some message in plaintext – all of type bytes – and outputs a ciphertext of type bytes. Analogous to pk, the encryption function simply invokes the PKEnc constructor of bytes. Thus, we need the decryption function pke_dec that only outputs the plaintext if the secret key passed as input to the function corresponds to the public key that was used for encryption. Since the actual implementation of the encryption and decryption functions is not part of the interface of the symbolic runtime layer, F* Lemmas are used to prove semantically relevant properties of these functions, like those outlined here, to the public. For example, the pke_dec_enc_lemma ensures the correctness property of pke_enc and pke_dec: val pke_dec_enc_lemma: sk:bytes -> n:bytes -> msg:bytes -> Lemma (pke_dec sk (pke_enc (pk sk) n msg) == Success msg) From the perspective of the interface, the semantics of real and symbolic cryptography are equivalent (ignoring the negligible probability that real cryptography can be broken): We encrypt a plaintext of type bytes and receive a ciphertext of type bytes but we cannot infer the structure of the ciphertext without the help of the decryption function and the secret key because its visible structure does not deviate from that of the plaintext. 24 2.1 Introduction to DY* Symbolic implemenations for other cryptographic primitives also exist in the symbolic crypto API. The ones relevant for this thesis are symmetric encryption, which is realized by Authenticated Encryption with Associated Data3 (AEAD) [24] in DY*, and signatures. AEAD is realized by functions aead_enc and aead_dec for authenticated encryption and decryption with a symmetric key, and signatures are created with a function sign and verified with a corresponding function verify. val aead_enc: key:bytes -> iv:bytes -> msg:bytes -> ad:bytes -> bytes val aead_dec: key:bytes -> iv:bytes -> ciphertext:bytes -> ad:bytes -> result bytes val aead_dec_enc_lemma: k:bytes -> iv:bytes -> m:bytes -> ad:bytes -> Lemma (aead_dec k iv (aead_enc k iv m ad) ad == Success m) The aead_enc function takes as input the symmetric encryption key key, a symbolic random initialization vector iv simulating randomness in the encryption, the message to encrypt denoted by msg, and the public associated data ad to be authenticated. Returned is the ciphertext resulting from the encryption. The corresponding decryption function aead_dec is given the key, initialization vector and associated data from the encryption, as well as the ciphertext to decrypt, and it outputs the previously encrypted plaintext. The ciphertext is returned only if the key, initialization vector, and associated data match in the encryption and decryption. The correctness property for AEAD is captured by a lemma called aead_dec_enc_lemma, analogous to the pke_dec_enc_lemma for public key cryptography. val sign: priv_key:bytes -> randomness:bytes -> msg:bytes -> bytes val verify: pub_key:bytes -> msg:bytes -> tag:bytes -> bool val verify_sign_lemma: sk:bytes -> n:bytes -> m:bytes -> Lemma (verify (vk sk) m (sign sk n m) == true) The sign function receives as input a private signing key priv_key, a symbolic randomness for signing, and the message to sign dentoted by msg. Returned is the resulting signature tag. For verification, the verify function accepts the public key pub_key corresponding to the private key used for signing, the original message, again denoted by msg, and the signature tag to verify denoted by tag. verify yields true on a valid signature, which is the case if the public key used for verification matches the private signing key and the message verified matches the message signed; otherwise it returns false. The verify_sign_lemma ensures that the verification is sound, i.e. the verify function must return true for all valid signature tags. It has already been pointed out that the attacker in DY* has the capabilities of a Dolev-Yao style attacker [17]. That is, it is in control of the network, can read, modify, schedule or block messages, compromise state sessions or call cryptographic functions on messages it already knows. DY* offers an API for the attacker that defines messages and terms known to the attacker via a refinement type of bytes called pub_bytes (i:timestamp). In particular, the type is defined as t:bytes{attacker_knows_at i t}, meaning that the attacker knows the term t at trace index i. Functions in the attacker’s API wrap the functions from the symbolic runtime layer but only accept inputs of type pub_bytes i instead of the more general bytes type to ensure that the attacker uses terms already known to it when calling these functions. For example, public key encryption is defined as val pke_enc: #i:timestamp -> pub_key:pub_bytes i -> randomness:pub_bytes i -> msg:pub_bytes i -> pub_bytes i. Besides this 3AEAD combines symmetric encryption and message authentication (MACs) into a single cryptographic primitive that provides confidentiality, as well as authenticity and integrity. 25 2 Basics subtle difference, the functions have syntax and semantics similar to the original functions used by honest principals, which demonstrates that the attacker’s API provides the attacker with the same capabilities as honest principals with respect to the processing of public bytestrings; this is also called attacker typability. Similar to the Dolev-Yao intruder, the DY* adversary can grow its knowledge as the global trace grows by using the (cryptographic) functions in the attacker’s API, e.g., to read messages that were sent on the network, split messages into their atomic parts, or even decrypt messages if the decryption key is known to the attacker. This behavior of the adversary is captured by a predicate attacker_can_derive: idx:timestamp -> steps:nat -> t:bytes -> Type0, which is used in statements about the derivability of a term t at trace index idx in a certain number of steps. If the attacker can derive a term from terms it already knows, then it holds per definition that the derived term is also part of the attackers knowledge (at a given trace index). As we have seen so far, the symbolic runtime model already offers everything we need to create models of cryptographic protocols. A model of a protocol can be constructed with a set of functions, where each function models an honest principal taking on some role in the protocol and executing a single protocol step. Protocol steps usually include that a principal retrieves its current state associated with the protocol run; receives a message from the network; decrypts, parses and validates the message or parts of it; builds, serializes and encrypts the response; and finally updates it’s state. In principle, since F* is what we would call a Turing Complete programming language, protocol steps could even perform arbitrary computations. The attacker cannot alter the protocol steps because it cannot control how honest principals behave but it can schedule the execution of protocol steps in any order and with arbitrary parameters and perform its own actions in between. From the attacker’s point of view, the functions implementing the protocol steps are simply black boxes that he can use to interact with honest principals. The executable part of a model thus consists of attack scenarios, where the attacker uses the protocol step functions and its own API, trying to find a way to break security. To verify the correctness of a model it generally makes sense to also implement a function that represents a benign environment in which the attacker remains passive and schedules the protocol steps as intended. Labeled Security Layer In the previous section we have learned how we can use the symbolic runtime layer of DY* to create executable models of cryptographic protocols. However, our main goal is to formulate and prove security properties for our models in DY* and mechanically verify these proofs using F*’s typechecker. This venture – although feasible in theory – would still require a huge effort with the symbolic runtime model because we would have to reason about secrecy implications of cryptographic functions in the symbolic runtime library each time we want to prove a new protocol secure. For this reason, the DY* framework consists of a second layer that was build on top of the runtime layer, namely the labeled security layer. With this layer, the concept of labels is introduced, which enables the formulation of reusable statements about the secrecy implications of cryptographic primitives and other crypto-related functions in the runtime library. Labels carry secrecy implications of terms by annotating them with the audience that is allowed to know them. This is especially useful for terms like nonces, keys or other secrets that should remain secret with respect to their intended audience. The labeled layer specifies another trace invariant, namely valid_trace, which ensures that the secrecy implications of labels hold at each trace index throughout protocol execution. Particularly, a valid trace is a trace containing only publishable 26 2.1 Introduction to DY* messages, and state sessions and events valid with respect to state session and event invariants that can be specified on the level of individual protocols. The valid_trace invariant also holds true in presence of the DY* adversary, which was defined on the lower symbolic runtime layer. Functions on the labeled layer are executed in terms of an effect LCrypto that wraps the Crypto effect from the symbolic layer and additionally ensures the validity of the resulting trace. The LCrypto effect also comes with requires and ensures predicates for specifying pre- and post-conditions of functions, but has the additional advantage that the case of an erroneous computation may be ignored in the post-condition. There are four types of labels, namely public, readers (ids:list id), join and meet. A term annotated with the public label can be safely published and transferred over the network without the use of encryption. The readers label is used to specify the allowed readers of a term. The fine-granularity of the readers is determined by the id type, which specifies the exact subset of state sessions belonging to a principal that can read the annotated term; that can either be all state sessions of a principal p (P p), a specific state session s of p (S p s), or only a specific version v of a state session (V p s v). Lastly, the labels join and meet denote unions and intersections of labels. In addition to the labels, the labeled layer annotates terms with a usage to ensure that keys are only to be used within the context for which they were established. For example, private decryption keys should not be used for signing as this might cause confidential information to leak if the adversary gets the owner of the key to sign a ciphertext and send it back to the adversary. The labeled layer refines all the cryptographic and stateful functions, originally defined in the symbolic runtime API, to ensure the preservation of a valid trace as well as labeling and usage constraints for these functions. Protocol code that builds on these refinements implicitly preserves or ensures the secrecy and usage implications of their inputs respectively outputs. This tremendously eases the proof of security properties involving keys and secrets, that are supposed to hold at a later time; particularly, after a successful protocol run. Since the labeled layer does not restrict the DY* adversary and even ensures that the attacker does not violate the valid trace property, all security properties that can be proven on the labeled layer specifically hold in presence of the DY* adversary. Let us take a look at our previous example of public key encryption and how it has been refined in the labeled crypto API: val pke_enc: #p:global_usage -> #i:timestamp -> #nl:label -> public_key:msg p i public -> nonce:pke_nonce p i nl -> message:msg p i (get_sk_label p.key_usages public_key){ can_flow i (get_label p.key_usages message) nl /\ (forall s. is_public_enc_key p i public_key (get_sk_label p.key_usages public_key) s ==> pke_pred p.usage_preds i s public_key message)} -> msg p i public val pke_dec: #p:global_usage -> #i:timestamp -> #l:label -> private_key:lbytes p i l{is_publishable p i private_key \/ (exists s. is_private_dec_key p i private_key l s)} -> ciphertext:msg p i public -> result (msg p i l) 27 2 Basics The type msg p i l is a refinement type of bytes that restricts possible values to bytes, valid with respect to some usage predicate p at trace index i and annotated with a label that can flow to l, i.e., is covered by the allowed readers of l4. Analogously, lbytes p i l denotes valid bytes with exact label l. is_publishable p i b holds true if b has type msg p i public; that is, if b’s label can flow to the public label5. The pke_nonce p i l type constrains the randomness that may be used for public key encryption to lbytes p i l with a fixed usage string that identifies it as randomness used for public key encryption. Given arbitrary bytes b, get_label outputs the label of b. Similarly, get_sk_label outputs the label of the corresponding private key if and only if b is a public key. The predicate pke_pred is a protocol specific constraint on the key usages and keys that may be used for encryption as well as the plaintexts that may be encrypted. The pke_enc function of the labeled API expects implicit arguments #p, #i and #nl, where #p is a protocol specific usage predicate, #i is a trace index and #nl denotes the label of the randomness used for encryption. The key used for encryption is safely publishable and the nonce has been specifically generated to be used as randomness in public key encryption. Further, the label of the message to be encrypted can flow to the label of the private key corresponding to the public key. This is necessary so that no information is encrypted that is more confidential than the key used for decryption. Finally, if the key material used for encryption really is a public key, i.e., has been strictly generated for the purpose of being used in public key encryption, then we have that the protocol specific usage constraint specified in pke_pred must hold for the used public key and the encrypted message. If all the above constraints are fulfilled, then the pke_enc function returns a publishable ciphertext that can be safely transmitted over the network. The pke_dec function also expects a global usage predicate #p and a timestamp #i. The label #l denotes the label of the key used for decryption. The key material used for decryption must either be publishable or must really be a decryption key and the ciphertext must be publishable. If all constraints are fulfilled and the decryption was successful, then pke_dec returns the original plaintext, which can flow to l and is hence readable by the owner of the decryption key. A lemma pke_dec_lemma ensures that if the correct key was used for decryption and pke_dec yields the plaintext, then it is either publishable (e.g. if it comes from the adversary), or the pke_pred must hold for the public key used in the encryption and the plaintext. The labeled layer defines similar refinements and usage constraints for AEAD and signatures. The refined aead_enc function requires that the key used for encryption is either publishable (for example, a key compromised by the adversary) or a valid secret key for AEAD, and that the label of the message can flow to the label of the key, i.e. that the message is not more secret than the key. Moreover, aead_enc requires, analogous to public key encryption, that the protocol specific usage constraint for AEAD (aead_pred) holds for the key and message. The corresponding decryption function aead_dec in conjunction with the aead_dec_lemma ensures that the aead_pred holds if the decryption was successful and the key is not publishable. Similarly, the labeled sign function requires that the key is publishable or a valid signing key and that sign_pred holds for the message to be signed and the verification key corresponding to the secret signing key if it is indeed a signing key. sign guarantees that both the signed message and the signature tag flow to a common label, so when signing confidential information labeled with a readers label, for example, the signature tag must be additionally protected by encryption under a key with a label that is at least as restrictive. 4It should be noted that in general, less restrictive labels can always flow to more restrictive labels but not the other way around, except for the case when the more restrictive label contains a corrupted identity. 5Since the can flow relation is reflexive, the public label can flow to itself. However, it is also possible that a more restrictive label flows to public if one of its readers has been corrupted. 28 2.2 Authentication Protocols The verify function and verify_lemma ensure that the usage predicate holds for the successfully verified message and the used verification key, or that the sign key label is publishable, which means that the signature guarantees do not apply. In general, the functions in the labeled API are more subtle with respect to their inputs and outputs and the types carry useful information about labels and usages of terms. While the symbolic runtime layer was mostly concerned with establishing correctness, e.g., that pke_dec returns the plaintext that was originally encrypted with pke_enc on a matching key pair, the labeled security layer is mostly concerned with the secrecy and usage context of terms. We can use the usage predicates for the cryptographic primitives to explicitly pass information about label and usage of an encrypted secret, or about logged events with attached data that matches the data in the encrypted or signed message, to the principal who will receive and decrypt or verify the message. As mentioned above, the decrypting or verifying principal can infer from the lemmas pke_dec_lemma, aead_dec_lemma, or verify_lemma that the respective usage predicate holds if the decryption or verification was successful and the key is not compromised nor does the message originate from the attacker. The properties ensured by the usage predicates can thus be carried across multiple protocol steps and can then be used to formulate and proof, among other things, secrecy and authentication properties of the respective protocols. Often, these properties are defined based on the final protocol state of principals or relations of trace events, which are ensured to be valid by the implicit state and event invariants also specified on the individual protocol level. The labeled layer already yields some generic security lemmas that were proven sound once and for all based on the implementation of the labeled API. A central lemma useful for secrecy proofs is the secrecy_lemma, which states that the secrecy of a bytes value b depends on the honesty of the principals who can read b according to its label: val secrecy_lemma: #pr:preds -> b:bytes -> LCrypto unit pr (requires (fun t0 -> True)) (ensures (fun t0 _ t1 -> t0 == t1 /\ (forall ids. (is_labeled pr.global_usage (trace_len t0) b (readers ids) /\ attacker_knows_at (trace_len t0) b) ==> (exists id. List.Tot.mem id ids /\ corrupt_at (trace_len t0) id)))) Precisely, the secrecy lemma states that if b is labeled with readers ids and the attacker knows b at trace_len t0, then there must be a corrupt state session identifier within ids. Hence, we can use the lemma to derive statements about a term’s secrecy if we know the label of that term. 2.2 Authentication Protocols Authentication protocols or authentication and key exchange protocols (short AKE protocols) are protocols that aim at establishing a secure channel for communication between two or more parties as well as mutually authenticating the parties to each other, i.e., to provide each party with the correct identities of the other parties. Strictly speaking, authentication protocols do not necessarily perform key establishment between parties but for the sake of simplicity we assume so and use the term interchangeably with the term AKE protocol. In this Master Thesis, we only take a look at the case where two parties want to communicate with each other. We use the term user to denote any principal that participates in a protocol with the goal of establishing a communication channel with 29 2 Basics another party – apparently, also a user. Trusted third parties tasked with session key generation or public key certification, we call authentication server or simply server. The term principal is used for any party participating in a protocol, including all users and possible servers. There are plenty of different protocol architectures that aim to achieve authentication and key establishment. In the context of this work, they can be classified in two categories based on the question, what keys have to be established in advance to be able to run the protocol [8]. The rationale behind this question is that there is no way to securely exchange keys if there is no previously established secure channel already available for the key exchange. We call keys that are already available at the beginning of a protocol run long-term keys and keys that are being established as a result of a protocol run session keys or communication keys. An AKE protocol requires one of the following to provide each party with guarantees about the channel that will be established: • symmetric long-term keys, or • asymmetric public keys In protocols that require symmetric long-term keys readily available, these keys are established either between • the users directly, such that the presence of an authentication server is not required, or • each user and an authentication server, where the server is in charge of the key exchange and often also its generation. The latter has the advantage that users do not need to maintain long-term keys with all the other users they want to talk to, but only with a single principal who is trusted to never leak them. The two protocols investigated in this master’s thesis that build on symmetric long-term secrets, i.e., the Otway-Rees [27] and Yahalom protocols [11], both rely on a trusted authentication server to generate and securely exchange sessions keys using the established long-term keys. Similarly, in protocols that rely on public key encryption and the availability of public keys, we have that either • users need to know the public keys of all other users they want to talk to, or • an authentication server takes over the role of a certification authority to distribute public keys to users that wish to communicate. Public keys have the advantage that no symmetric long-term secrets need to be established in advance. The second variant further simplifies key management because a user only needs to know their own public key and that of the authentication server. On the other hand, public key encryption adds computational overhead to the protocol [8]. The third protocol that we analyze, namely the Denning-Sacco protocol [16], falls into the second category of AKE protocols that rely on public key encryption. 30 3 Related Work This chapter comprises a summary of available literature on authentication protocols and different techniques and approaches for their symbolic analysis with a special focus on the three authentication protocols that are discussed as part of this thesis. Because the analyzed protocols all date back more than three decades ago, we will mainly present literature that was released in the nineties and early two thousands. For an overview of more recent approaches with fully automated proof techniques, we refer to the DY* paper by Bhargavan et al. [6]. 3.1 Authentication Protocols Detailed introductions to the nature of authentication and key establishment protocols are given in “A Survey of Authentication Protocol Literature” by Clark and Jacob [14] (1997) and in the book “Protocols for Authentication and Key Establishment” by Boyd et al. [8] (2003). Both give a detailed overview over cryptographic tools, architectural styles, design patterns, security goals and attack types that come with such protocols and hence complement the short introduction to authentication protocols that we gave in Section 2.2. Clark and Jacob also summarize formal methods used to analyze such protocols. Further, both literatures provide large lists with descriptions of well known authentication protocols and possible attacks, including the protocols studied in this thesis. Clark and Jacob document attacks on all three protocols, while Boyd et al. only present attacks on two of them. 3.2 Symbolic Analysis Approach The symbolic approach for the analysis of cryptographic protocols was introduced by Dolev and Yao [17] (1983) with their work on the notion of a symbolic attacker that is still used in modern symbolic provers like DY* as of today. Another milestone with respect to symbolic analysis methods is the work of Burrows et al. [11] (1989) on the BAN logic for authentication protocols. The BAN logic was the first approach to capture the goals and assumptions of authentication protocols in terms of a formal language for principal beliefs. A BAN analysis always starts with a set of initial beliefs representing a protocol’s prerequisites and a set of belief goals representing the authentication goals of a protocol. Further beliefs can be derived from the initial beliefs using a fixed set of inference rules, as messages are received. This process eventually results in a set of final beliefs representing the actual assumptions that principals can make when running the protocol successfully. Burrows et al. demonstrated their logic on multiple well known authentication protocols, including the Otway-Rees and Yahalom protocols. Justified criticism against the BAN logic was mainly concerned with optimizations, which the BAN authors proposed based on their analysis results, that turned out to be less secure (e.g., [7] and [33]) and with its lack of sensibility against the permutation of 31 3 Related Work protocol steps [32]. Based on this criticism, multiple extensions to the logic were proposed and later unified in the so-called SVO logic by Syverson and Van Oorschot [34] (1994). The SVO logic has been used by researchers to analyze and improve the Otway-Rees [12] and Yahalom [13] protocols, among others. Mid and late nineties Ryan et al. [31] developed a completely new approach to the symbolic analysis of cryptographic protocols based on a process algebra named Communicating Sequential Process (CSP). CSP itself is a mathematical notation to describe and analyze systems of processes communicating with each other via messages. Ryan et al. present a trace-based approach that uses CSP to model the roles of principals and the messages in a protocol. Additionally, they include the notion of an active adversary that can be equipped with different capabilities. Secrecy and authentication properties are defined with the help of trace events that claim messages secret or commit to protocol runs. The verification of protocol models and security properties is automated via the model checker FDR and a compiler named Casper that translates models and properties to FDR code. The CSP approach was followed by a whole series of new approaches with automated tool support. For example, Brackin developed an Automatic Authentication Protocol Analyzer (AAPA) [9] (1998) based on an extension of the GNY belief logic1 [19], the BGNY logic. The AAPA tool was able to analyze 52 of the 53 protocols presented in “A Survey of Authentication Protocol Literature” (see Section 3.1) and detected 9 flaws (including a flaw on the Yahalom protocol) of which 3 flaws were previously unidentified. However, it also missed 19 flaws that Clark and Jacob had found in their protocol library, including flaws on the Otway-Rees protocol and the Denning-Sacco protocol with symmetric cryptography. Brackin was able to give an explanation for 18 of these misses and sketched how the AAPA could be further improved to account for the undetected flaws. Later fully automated provers like AVISS [3] (2002) or its successor AVISPA [35] (2006) came with an expressive formal language for the specification of security protocols and properties as well as support for multiple backends implementing different automatic analysis techniques, like protocol falsification or abstraction-based verification, to account for a large variety of protocols. Furthermore, the network over which messages are exchanged has been modeled in terms of a Dolev-Yao style intruder to simulate an inherently insecure environment for the execution of protocols. The AVISS tool could find 31 flaws in the protocol library of Clark and Jacob; this also includes a flaw in the Otway-Rees protocol and a previously unreported flaw in the Denning-Sacco protocol. The authors of AVISPA tested their tool on their own library consisting of 33 industrial-scale security protocols, which have been used to derive a total of 215 security problems. Their results include unreported flaws on protocols from the ISO-PK family as well as on the IKEv2 protocol with digital signatures. Tools like AVISPA were followed by the latest generation of fully automated provers like TAMARIN [25] (2013), which even support complex protocol features such as loops or mutable global state and capture all possible traces of a protocol in the time of a wink. Other modern approaches try to combine the advantages of symbolic and computational methods for the analysis of cryptographic protocols. Symbolic methods treat the ability to produce much simpler and often automated proofs against weaker security guarantees because of restrictions on the capability of an adversary. On the other hand, computational methods result in powerful security guarantees in presence of a probabilistic polynomial-time attacker but proofs are usually 1A successor of the BAN logic that accounts for the permutation of protocol steps, motivated by [32] 32 3.3 Selected Protocols and Conducted Analyses complex and more prone to errors. The results of the research on unifying the two approaches and their advantages were captured in a survey by Cortier et al. [15]. The pioneers in this field were Backes et al. [5] (2003) with their proposal of an abstract cryptographic library based on Dolev-Yao style primitives, for which they proved that a real cryptographic implementation of their library is as least as secure as the abstract library itself. Their abstract library accounts for all kinds of protocol features like public-key encryption, digital signatures, nonces, list operations and application data. Furthermore, active attacks are modeled by embedding the library in a stateful Dolev-Yao system, where honest principals and the attacker can both perform any cryptographic operation that is possible based on previous events. The proof provided by Backes et al. for the security of the real cryptographic library is based on simulatability, i.e., that the abstract library simulates the real library, which is a common proof technique used in computational proofs. To proof the adequacy of their work, one of the authors (Backes) [4] used the ideal cryptographic library to obtain a cryptographically sound security proof of the Otway-Rees protocol. 3.3 Selected Protocols and Conducted Analyses In the previous section, we gave an overview over some of the most important milestones in the symbolic approach to cryptographic protocol analysis. Many of the discussed methods have been used, among other things, for the analysis of the protocols Otway-Rees, Yahalom, and Denning- Sacco, which we investigate in this work. In the rest of this chapter, we present the three protocols and discuss and reason about the results of their analyses under consideration of the assumptions made by the used approaches and also by the authors who conducted the analyses. 3.3.1 Otway-Rees The Otway-Rees protocol is an authentication protocol that performs a session key exchange between two users via symmetric long-term keys and a trusted authentication server. The protocol was proposed by Otway and Rees in their paper “Efficient and Timely Mutual Authentication” [27] and goes as follows: 1. 𝐴→ 𝐵 : 𝑁𝑐𝑖𝑑 , 𝐴, 𝐵, {𝑁𝑎, 𝑁𝑐𝑖𝑑 , 𝐴, 𝐵}𝑠𝑘𝑎𝑠 2. 𝐵 → 𝐴𝑆 : 𝑁𝑐𝑖𝑑 , 𝐴, 𝐵, {𝑁𝑎, 𝑁𝑐𝑖𝑑 , 𝐴, 𝐵}𝑠𝑘𝑎𝑠 , {𝑁𝑏, 𝑁𝑐𝑖𝑑 , 𝐴, 𝐵}𝑠𝑘𝑏𝑠 3. 𝐴𝑆 → 𝐵 : 𝑁𝑐𝑖𝑑 , {𝑁𝑎, 𝑘𝑎𝑏}𝑠𝑘𝑎𝑠 , {𝑁𝑏, 𝑘𝑎𝑏}𝑠𝑘𝑏𝑠 4. 𝐵 → 𝐴 : 𝑁𝑐𝑖𝑑 , {𝑁𝑎, 𝑘𝑎𝑏}𝑠𝑘𝑎𝑠 The users 𝐴 and 𝐵 initially share symmetric long-term keys 𝑘𝑎𝑠 and 𝑘𝑏𝑠 with an authentication server 𝐴𝑆. The protocol is initiated by 𝐴 who first chooses a random conversation identifier 𝑁𝑐𝑖𝑑 and a challenge 𝑁𝑎. 𝐴 then sends 𝑁𝑐𝑖𝑑 along with its own identifier, the identifier of the responder 𝐵 and a part encrypted under 𝑘𝑎𝑠 that contains the initiator’s challenge as well as copies of the identifiers to 𝐵. Upon receiving of the first message, the responder 𝐵 chooses its own random challenge 𝑁𝑏, appends a part encrypted under 𝑘𝑏𝑠 with a structure similar to 𝐴’s part to the message and forwards it to the server. The server uses the identifiers of 𝐴 and 𝐵 in the plaintext part of the second message to retrieve 𝐴’s and 𝐵’s long term-keys, decrypts the encrypted parts and checks whether the components 𝑁𝑐𝑖𝑑 , 𝐴 and 𝐵 match in these parts. If they match, it chooses a fresh 33 3 Related Work key 𝑘𝑎𝑏 for communication between 𝐴 and 𝐵 and encrypts the key respectively with each of the principals’ challenges. The server then sends the encrypted keys and challenges together with the conversation identifier 𝑁𝑐𝑖𝑑 back to the responder who decrypts his part, verifies his challenge 𝑁𝑏 and obtains 𝑘𝑎𝑏. Finally, the responder forwards the rest of the message to the initiator such that it can also verify its challenge and obtain the key. Analyses and Results The Otway-Rees protocol is one of the protocols that have been investigated in the BAN paper [11]. In the paper, a short description of the protocol is given that essentially matches the original description by Otway and Rees as well as ours. The BAN authors also account for the fact that the identifiers 𝑁𝑐𝑖𝑑 , 𝐴 and 𝐵 in the plaintext part of the second message are never compared with their copies in the encrypted parts. This is however disregarded in the BAN analysis, as the plaintext parts of messages are discarded in the protocol idealization process that precedes the analysis. With their BAN analysis, Burrows et al. come to the conclusion that the protocol is well designed and provides strong guarantees regarding the exchanged key and timeliness of the messages. The initial assumptions made by the authors are that 𝐴, 𝐵 and the 𝐴𝑆 trust their shared long-term keys to be suitable for secret communication between them and that 𝐴 and 𝐵 trust in the 𝐴𝑆 to choose a key that is suitable for secret communication between 𝐴 and 𝐵. From that, they conclude – using the BAN logic – that 𝐴 as well as 𝐵 both belief that 𝑘𝑎𝑏 is a good key for communication between them, i.e., is only known to them or parties trusted by them. Moreover, they state that 𝐵 authenticates to 𝐴 via the second message from 𝐵 to the 𝐴𝑆, which contains an encrypted part with 𝐴’s challenge in it. However, they admit that the authentication is one sided in that 𝐵 cannot say the same about 𝐴 because 𝐴 never sends a message containing something that 𝐵 believes to be fresh. Boyd and Mao [7] later pointed out the limitations of the BAN logic on the example of the Otway-Rees protocol. They show that the Otway-Rees protocol is not secure under the assumptions made in the BAN paper and that the optimizations proposed by Burrows et al. are dangerous in that they do not result in a secure version of the protocol either. The attack pointed out by Boyd and Mao on the original protocol is the following: 1. 𝐴→ 𝐼 (𝐵) : 𝑁𝑐𝑖𝑑 , 𝐴, 𝐵, {𝑁𝑎, 𝑁𝑐𝑖𝑑 , 𝐴, 𝐵}𝑠𝑘𝑎𝑠 2. 𝐼 (𝐵) → 𝐴𝑆 : 𝑁𝑐𝑖𝑑 , 𝐴, 𝐸, {𝑁𝑎, 𝑁𝑐𝑖𝑑 , 𝐴, 𝐵}𝑠𝑘𝑎𝑠 , {𝑁𝑒, 𝑁𝑐𝑖𝑑 , 𝐴, 𝐵}𝑠𝑘𝑒𝑠 3. 𝐴𝑆 → 𝐼 (𝐵) : 𝑁𝑐𝑖𝑑 , {𝑁𝑎, 𝑘𝑎𝑒}𝑠𝑘𝑎𝑠 , {𝑁𝑒, 𝑘𝑎𝑒}𝑠𝑘𝑒𝑠 4. 𝐼 (𝐵) → 𝐴 : 𝑁𝑐𝑖𝑑 , {𝑁𝑎, 𝑘𝑎𝑒}𝑠𝑘𝑎𝑠 They explain that this attack is possible because the 𝐴𝑆 does not compare the conversation identifier 𝑁𝑐𝑖𝑑 and the user identifiers 𝐴 and 𝐵 in the plaintext part of the second message with their copies in the encrypted parts. Boyd and Mao see the main problem in the idealization process applied to protocols in order to derive initial assumptions for the BAN analysis. Their argument is that the implementation-level behavior of the 𝐴𝑆 does not reflect in the abstractions made by the idealization process and that an implementation-level fix to prevent the attack would not have affected the BAN analysis in any way. Based on their research, they introduce the concept of robust protocols as generic fix for the problem encountered in the Otway-Rees protocol and similar problems. Intuitively, robust protocols are designed such that messages contain all the information necessary to authenticate them. Boyd and Mao argue that this is not the case for the original Otway-Rees 34 3.3 Selected Protocols and Conducted Analyses protocol since the third message, issued by the 𝐴𝑆, does not make explicit to the users who the respective peer of the key 𝑘𝑎𝑏 is. Based on this observation, they propose the following fix for the third message: 3. 𝐴𝑆 → 𝐵 : 𝑁𝑐𝑖𝑑 , {𝐴, 𝑁𝑎, 𝑘𝑎𝑏}𝑠𝑘𝑎𝑠 , {𝐵, 𝑁𝑏, 𝑘𝑎𝑏}𝑠𝑘𝑏𝑠 We show that the proposed fix is actually not sufficient to prevent the previously discussed impersonation attack and present our own improved version of the Otway-Rees protocol in Section 4.3. A more recent effort to perform a symbolic analysis of the Otway-Rees protocol using a belief logic has been made by Chen [12] who proposed a new improved version of the Otway-Rees protocol and used the SVO logic [34] to show that their version fulfills the desired authentication properties. They refer to the impersonation attack detected by Boyd and Mao [7] as well as their proposed fix to include users’ identities in the third message and argue that it is not sufficient to establish authentication between 𝐴 and 𝐵. Chen’s improved version of the Otway-Rees protocol goes as follows: 1. 𝐴→ 𝐵 : 𝑁𝑐𝑖𝑑 , 𝐴, {𝑁𝑎, 𝑁𝑐𝑖𝑑 , 𝐵}𝑠𝑘𝑎𝑠 2. 𝐵 → 𝐴𝑆 : 𝑁𝑐𝑖𝑑 , 𝐴, 𝐵, {𝑁𝑎, 𝑁𝑐𝑖𝑑 , 𝐵}𝑠𝑘𝑎𝑠 , {𝑁𝑏, 𝑁𝑐𝑖𝑑 , 𝐴}𝑠𝑘𝑏𝑠 3. 𝐴𝑆 → 𝐵 : 𝑁𝑐𝑖𝑑 , {𝑁𝑎, 𝐵, 𝑘𝑎𝑏}𝑠𝑘𝑎𝑠 , {𝑁𝑏, 𝐴, 𝑘𝑎𝑏}𝑠𝑘𝑏𝑠 4. 𝐵 → 𝐴 : 𝑁𝑐𝑖𝑑 , {𝑁𝑎, 𝐵, 𝑘𝑎𝑏}𝑠𝑘𝑎𝑠 , {𝑁𝑏, 𝐵}𝑠𝑘𝑎𝑏 5. 𝐴→ 𝐵 : 𝑁𝑐𝑖𝑑 , {𝑁𝑏 − 1, 𝐴}𝑠 𝑘𝑎𝑏 The initial assumptions that Chen defines for their improved protocol are the same as those made by Burrows et al. [11] in their BAN analysis plus the assumption that 𝐴 and 𝐵 trust the 𝐴𝑆 to generate a communication key that is fresh. The security goals are however slightly stronger than the goals originally intended by Otway and Rees [27]. In particular, 𝐴 and 𝐵 should both be convinced that the communication key 𝑘𝑎𝑏 is secret to 𝐴 and 𝐵 or parties they trust (including the 𝐴𝑆), and that the key is also fresh. Moreover, users should be convinced that the other party has the same beliefs about 𝑘𝑎𝑏 as they do. Chen then goes on to show that their improved protocol is in fact secure by providing the respective SVO derivations for 𝐴 and 𝐵 that lead to the specified security goals. However, the improved protocol significantly deviates from the original protocol in that all four messages have been modified and two parts encrypted under 𝑘𝑎𝑏 have been added in the fourth and respectively in an additional fifth message to reassure each user that the other user is in possession of the same key and has the same beliefs about it. In Section 4.3, we show that less modifications already suffice to achieve the originally intended security goals. Yu et al. [37] very recently suggested multiple possible improvements to the Otway-Rees protocol based on the results of their analysis with Enhanced Authentication Tests (EAT). Guttman and Thayer [20] first proposed Authentication Tests (AT) as a symbolic method for the analysis of cryptographic protocols regarding their authentication properties. The method was later improved by Yang and Luo [36] to also reason about confidentiality aspects of protocols, which led to EAT. The proposed improvements have the advantage over those of Chen in [12] that they achieve the same strong security goals with only minimal alternations to the original messages of the protocol and only one additional part encrypted with 𝑘𝑎𝑏 in the fourth message. Nonetheless, we will 35 3 Related Work propose our own improved version of the protocol in Section 4.3 that does not even require the additional encrypted component to achieve key secrecy of the communication key 𝑘𝑎𝑏 and mutual authentication between the principals 𝐴 and 𝐵. In contrast to the previously discussed analyses stands that of Backes [4], who used the abstract cryptographic library [5] presented in Section 3.2 to receive “A Cryptographically Sound Dolev-Yao Style Security Proof of the Otway-Rees Protocol”. The approach of Backes includes a symbolic security proof of the Otway-Rees protocol in the abstract library and exploits the fact that the abstract library can be safely realized using real cryptography – proven in [5] – to further derive its security in a computational setting. The proof assumes that the protocol is implemented such that commonly known type-flaw and implementation dependent attacks like those pointed out in [14] or [8] are not possible. Backes defines the security of the Otway-Rees protocol in the ideal (abstract) library in terms of a secrecy and consistency property. The secrecy property states that the adversary cannot learn a key shared by two honest users after successfully running the protocol; the consistency property refers to the consistency of users’ views regarding the peer of their respective key session. Secrecy of the communication key 𝑘𝑎𝑏 is proven based on the fact that the key is only exchanged over channels secured by the long-term keys 𝑘𝑎𝑠 and 𝑘𝑏𝑠 shared between 𝐴 and the 𝐴𝑆 respectively 𝐵 and the 𝐴𝑆; the proof for consistency is directly derived from the secrecy proof. Backes then carries the properties over to the cryptographic setting by using the proof work in [5] and showing that the so-called commitment problem does not occur in the Otway-Rees protocol, i.e., that the long-term keys used to encrypt the communication key are never leaked. This is derived from the assumption that the long-term keys of honest principals are secret. Thus, Backes is able to show that the secrecy and consistency properties also hold for an implementation of the library that uses real cryptography. 3.3.2 Yahalom The Yahalom protocol is an authentication protocol that, similarly to the Otway-Rees protocol, performs a key exchange using symmetric long-term keys shared with an authentication server. The protocol originates from personal communication and was formalized in [11]: 1. 𝐴→ 𝐵 : 𝐴, 𝑁𝑎 2. 𝐵 → 𝐴𝑆 : 𝐵, {𝐴, 𝑁𝑎, 𝑁𝑏}𝑠𝑘𝑏𝑠 3. 𝐴𝑆 → 𝐴 : {𝐵, 𝑘𝑎𝑏, 𝑁𝑎, 𝑁𝑏}𝑠𝑘𝑎𝑠 , {𝐴, 𝑘𝑎𝑏} 𝑠 𝑘𝑏𝑠 4. 𝐴→ 𝐵 : {𝐴, 𝑘𝑎𝑏}𝑠𝑘𝑏𝑠 , {𝑁𝑏}𝑠𝑘𝑎𝑏 The long-term keys that 𝐴 and 𝐵 share with the 𝐴𝑆 are denoted – similar as in Otway-Rees – 𝑘𝑎𝑠 and 𝑘𝑏𝑠. The first message is emitted by the initiator 𝐴 who chooses a random nonce 𝑁𝑎 and sends its identity together with the generated nonce to 𝐵. On receipt of the first message, the responder 𝐵 chooses its own nonce 𝑁𝑏 and encrypts a message containing 𝐴’s identity and the two nonces under 𝑘𝑏𝑠. 𝐵 then sends the second message containing its own identity and the encrypted part to the 𝐴𝑆. Using 𝐵’s identity, the 𝐴𝑆 is able to retrieve 𝑘𝑏𝑠 and decrypt the ciphertext in the second message. Among other things, it obtains 𝐴’s identity, which it needs to retrieve the other long-term key corresponding to 𝐴. The 𝐴𝑆 goes on to choose a fresh session key 𝑘𝑎𝑏 for the communication of 𝐴 and 𝐵 and then sends the third message containing two parts encrypted under the users’ long-term keys to 𝐴. The first part is encrypted under 𝑘𝑎𝑠 and intended for 𝐴; it contains 𝐵’s identity, the 36 3.3 Selected Protocols and Conducted Analyses session key 𝑘𝑎𝑏, and the nonces 𝑁𝑎 and 𝑁𝑏. Likewise, the second part is encrypted under 𝑘𝑏𝑠 and intended for 𝐵; it only contains 𝐴’s identity and 𝑘𝑎𝑏. When the initiator receives the third message, it decrypts the part encrypted under 𝑘𝑎𝑠 and verifies the responder’s identity as well as its own challenge 𝑁𝑎. If the verification succeeds, it accepts 𝑘𝑎𝑏 as session key and uses it to encrypt 𝑁𝑏 for verification by the responder. 𝐴 then forwards the second encrypted part from the third message together with 𝐵’s encrypted nonce to 𝐵. In the last step, 𝐵 receives the fourth message, decrypts the part from the 𝐴𝑆 using 𝑘𝑏𝑠, verifies 𝐴’s identity, and, if successful, uses 𝑘𝑎𝑏 to decrypt 𝐴’s part and verify its challenge 𝑁𝑏. Finally, if the challenge is correct, it also accepts 𝑘𝑎𝑏 as session key. Analyses and Results As mentioned, the Yahalom protocol was first formalized in the BAN paper [11] and was therefore naturally subject to a BAN analysis. The initial assumptions made for Yahalom are quite similar to those in the analysis of Otway-Rees – the principals believe in the appropriateness of their long-term keys and the users believe in the freshness of their nonces and trust the authentication server to choose an appropriate session key. However, in case of Yahalom, several additional assumptions were needed due to the unusual protocol design. For example, 𝐵 requires a statement about the freshness of 𝑘𝑎𝑏 to infer that the last message has been sent timely and 𝐴 must trust the 𝐴𝑆 to pass on 𝐵’s challenge in the third message. From the initial assumptions and the third message Burrows et al. easily derive that 𝐴 trusts in the suitability of 𝑘𝑎𝑏 as communication key. To derive the same belief for 𝐵, a small adaption to the logic was necessary allowing 𝐵 to use the session key 𝑘𝑎𝑏 for the decryption of 𝑁𝑏 before it can assume that the key is good by verifying 𝑁𝑏. This adaption and the fact that 𝐵 trusts 𝐴𝑆 and 𝐴 to generate and respectively use a fresh session key 𝑘𝑎𝑏 suffice to infer that 𝐵 also beliefs in the suitability of the session key. Further, 𝐵 is convinced 𝐴 has the same beliefs about 𝑘𝑎𝑏 as itself and therefore 𝐵 would not notice if 𝐴 decides to replay an old key in the fourth message. According to the authors this does however not impose a major flaw in the protocol because principals are generally assumed to be honest in the context of a BAN analysis. Based on the analysis results, the BAN authors have proposed a modified version of Yahalom that should lead to the same outcome with less encryption and fewer assumptions. The modified version was later proven insecure by Syverson [33] who documented an attack in which the attacker is able to make 𝐴 accept a public nonce chosen by 𝐵 as session key. The results of the BAN analysis were later taken up by Chen and Shi [13] in an analysis of the Yahalom protocol with the SVO logic [34]. Chen and Shi interpret the fact highlighted by Burrows et al. [11] that a malicious 𝐴 could replay an old session key in the fourth message such that the protocol cannot achieve the authentication goals it intends to achieve. To proof their point, they first formalize the security goals of Yahalom in terms of the SVO logic and then show that the goals are not achieved by the original protocol. The initial assumptions overlap with those of the BAN analysis in assumptions about 𝐴’s and 𝐵’s trust in the long-term keys they share with 𝐴𝑆, the secrecy and suitability of the session key generated by 𝐴𝑆, and the freshness of their respective nonces, as well as 𝐵’s trust in a statement about the freshness of the session key from 𝐴𝑆. In addition to the BAN assumptions, Chen and Shi assume that 𝐴 trusts 𝐴𝑆 equally regarding the freshness of 𝑘𝑎𝑏. Further assumptions that were required in the BAN analysis to derive 𝐵’s belief in the freshness and thus the secrecy of the session key are not included in the SVO analysis because 𝐴 may act maliciously. The goals defined by Chen and Shi are stronger than the ones raised by the BAN authors. Naturally, the users 𝐴 and 𝐵 shall both be convinced that the session key is secret and 37 3 Related Work a good communication key. However, they also shall be satisfied in their belief that the session key is fresh and that the respective other party is equally convinced about its suitability and freshness. The analysis shows that 𝐴 is not convinced that 𝐵 shares its beliefs about the key and 𝐵 itself is not convinced that the key is fresh. This leads Chen and Shi to propose the following improved protocol: 1. 𝐴→ 𝐵 : 𝐴, 𝑁𝑎 2. 𝐵 → 𝐴𝑆 : 𝐵, {𝐴, 𝑁𝑎, 𝑁𝑏}𝑠𝑘𝑏𝑠 3. 𝐴𝑆 → 𝐴 : {𝐵, 𝑘𝑎𝑏, 𝑁𝑎, 𝑁𝑏}𝑠𝑘𝑎𝑠 , {𝐴, 𝑁𝑏, 𝑘𝑎𝑏}𝑠𝑘𝑏𝑠 4. 𝐴→ 𝐵 : {𝐴, 𝑁𝑏, 𝑘𝑎𝑏}𝑠𝑘𝑏𝑠 , {𝐴, 𝑁𝑏}𝑠𝑘𝑎𝑏 5. 𝐵 → 𝐴 : {𝐵, 𝑁𝑎 − 1}𝑠 𝑘𝑎𝑏 They show that their improvements suffice to derive the remaining security goals and hence complete the SVO derivations of 𝐴 and 𝐵. The improved Yahalom protocol’s structure is somewhat similar to that of the improved Otway-Rees protocol proposed by Chen [12] and discussed in Section 3.3.1; it therefore also achieves the same strong security goals. Although the improved Yahalom protocol only slightly deviates from the original protocol in the third and fourth message, it still requires the additional fifth message to achieve its security goals. Besides symbolic analyses based on belief logics, the Yahalom protocol further was subject to an analysis with the CSP approach [31]. Ryan et al. used the Yahalom protocol as running example to demonstrate how to formalize and proof security properties using the CSP approach. We have already explained in Section 3.2 how CSP supports the notation of trace events, which mark certain points passed during a protocol run and allow for the deduction of assumptions about the state of the particular principal triggering them. Ryan et al. denote the secrecy property in CSP as the requirement that if a principal claims that a message is secret and sender as well as receiver of the message are honest, then this message should never leak to the adversary. This must particularly apply to the session key contained in the third message from the 𝐴𝑆 to 𝐴 and claimed to be only known to 𝐴 and 𝐵. Mutual authentication is formalized in two separate properties for the initiator and respectively, the responder. Authentication of the initiator to the responder requires that an honest initiator 𝐴 triggers a running signal before 𝐵 commits to the run and both should agree on their identities and nonces as well as the exchanged key. Responder authentication is a little weaker in that Ryan et al. only require an honest 𝐵 to emit a running signal before 𝐴 completes the run and that both parties should agree on their identities as well as nonces, but not necessarily on the session key. This simply comes from the fact that 𝐴 gets no reassurance whether 𝐵 really receives or accepts the key 𝑘𝑎𝑏 within the scope of the protocol (because 𝐵 never encrypts a message for 𝐴 using 𝑘𝑎𝑏). Finally, Ryan et al. use CSP to show that the specified security properties indeed hold for the Yahalom protocol, i.e., the session key 𝑘𝑎𝑏 remains secret as long as principals do not act in a malicious way, and initiator and responder achieve timely mutual authentication. Another effort to analyze the Yahalom protocol was made by Paulson [28], who used an inductive method based on possible protocol traces over time. Paulson’s approach also includes the model of an active adversary that controls the communication and can occasionally compromise session keys. Their work aims to confirm the results of the BAN analysis [11] regarding both, the original Yahalom protocol, as well as the modifications proposed by the BAN authors. The secrecy property for the Yahalom protocol is formalized and proven in terms of multiple theorems and lemmas. The session key compromise theorem states that the loss of one session key does not affect the secrecy of 38 3.3 Selected Protocols and Conducted Analyses other session keys. The session key secrecy theorem ensures that if the server issues a key to 𝐴 and 𝐵, only 𝐴 and 𝐵 will obtain the key. Additionally, the third message from which the users obtain the session key and deduce timeliness guarantees must really originate from the 𝐴𝑆. This already suffices to prove that the session key, which 𝐴 accepts, is unknown to the adversary. To conclude the same for 𝐵, Paulson shows that, under certain condiditions, 𝑁𝑏 remains secret and therefore 𝐵 is able to deduce that the session key is fresh. Mutual authentication is directly derived from the secrecy of the long-term keys and the session key. Paulson argues that if 𝐴 receives its certificate from the 𝐴𝑆 in the third message and 𝐵 is honest, then 𝐵 must have sent the second message in which it encrypted 𝑁𝑎 using 𝑘𝑏𝑠. 𝐵 on the other hand gets its guarantees from the fourth message containing 𝑁𝑏 encrypted under the session key 𝑘𝑎𝑏, which 𝐵 believes to be only known to 𝐴 (and the 𝐴𝑆, which it trusts not to act maliciously), and therefore, the encryption must have originated from 𝐴. Our analysis in Section 4.4 confirms the results of Paulson’s analysis and formalizes the security properties of the Yahalom protocol in a corresponding DY* model. In contrast to security proofs such as those of Ryan et al. [31] or Paulson [28] are attacks such as the replay attack described in [11] and mentioned in [13]. Another attack on the Yahalom protocol was documented by Clark and Jacobs in ”A Survey of Authentication Protocol Literature“ [14]: 1. 𝐼 (𝐴) → 𝐵 : 𝐴, 𝑁𝑎 2. 𝐵 → 𝐼 (𝐴𝑆) : 𝐵, {𝐴, 𝑁𝑎, 𝑁𝑏}𝑠𝑘𝑏𝑠 3. omitted in the attack, but certainly relevant for the adversary to get a handle to the key 4. 𝐼 (𝐴) → 𝐵 : {𝐴, 𝑁𝑎, 𝑁𝑏}𝑠𝑘𝑏𝑠 , {𝑁𝑏}𝑠𝑁𝑎 ,𝑁𝑏 Here, the adversary plays the role of 𝐴 and the 𝐴𝑆 to establish a session key with 𝐵 that has not been issued by the 𝐴𝑆. However, it is clear to see that in order for the adversary to benefit from this attack, it must somehow learn 𝑁𝑏, which it can only do if it gets a handle to 𝐴’s long-term key 𝑘𝑎𝑠. As the BAN authors already clarified in their analysis, the Yahalom protocol is not designed to protect against such attacks based on compromised long-term secrets like the attack outlined here or the replay attack mentioned in the BAN paper. Therefore, these attacks are not in conflict with the DY* security proof of the Yahalom protocol we give in Section 4.4. 3.3.3 Denning-Sacco The Denning-Sacco protocol with public keys is an authentication and key exchange protocol based on public key encryption and signatures. Public keys are known to an authentication server or certification authority that helps distributing them. The protocol was outlined by Denning and Sacco in “Timestamps in Key Distribution Protocols” [16] and has the following structure: 1. 𝐴→ 𝐴𝑆 : 𝐴, 𝐵 2. 𝐴𝑆 → 𝐴 : 𝐶𝐴, 𝐶𝐵 3. 𝐴→ 𝐵 : 𝐶𝐴, 𝐶𝐵, {{𝑘𝑐, 𝑇}𝑎𝑆𝐴 }𝑎 𝑃𝐵 𝐶𝐴 and 𝐶𝐵 are certificates issued by the 𝐴𝑆 for public key distribution, where 𝐶𝐴 = {𝐴, 𝑃𝐴, 𝑇}𝑎𝑆𝐴𝑆 and 𝐶𝐵 = {𝐵, 𝑃𝐵, 𝑇}𝑎𝑆𝐴𝑆 . 𝑃_ denotes public keys for usage in public key encryption or signature schemes, 𝑆_ denotes the corresponding private keys for decryption of ciphertexts or signature verification, 𝑘𝑐 is the communication key established as a result of the protocol, and 𝑇 denotes a 39 3 Related Work timestamp. Denning and Sacco proposed the use of timestamps to ensure timeliness of messages and certificates and to eliminate the need of handshake messages between users. They suggested that principals should synchronize their local clocks by setting them according to some standard source. A timestamp 𝑇 is valid as long as |𝐶𝑙𝑜𝑐𝑘 −𝑇 | < Δ𝑡1+Δ𝑡2 holds true, where Δ𝑡1 is a tolerance value to account for discrepancies between users’ local clocks (more precisely, between possibly different standard sources) and Δ𝑡2 is the time needed to send a message over the network, i.e., the network delay time. Therefore, the timestamps can protect against replays of old messages, especially of the third message containing the communication key. More precisely, if a communication key between 𝐴 and 𝐵 somehow leaks, the attacker cannot use it to establish communication with 𝐵 under the name of 𝐴 at a later time, particularly any time 𝑇 ′ such that 𝑇 ′ >= 𝑇 + Δ𝑡1 + Δ𝑡2. Moreover, the timeliness guarantees we get from the timestamps make a handshake between the users obsolete. The protocol begins with 𝐴 telling the 𝐴𝑆 its own identity and the identity of the other user it wants to talk to, here denoted as 𝐵, in the first message. The 𝐴𝑆 then retrieves the users public keys based on the identities provided in the first message and issues the certificates 𝐶𝐴 for 𝐴 and 𝐶𝐵 for 𝐵, with 𝑇 set to the 𝐴𝑆’s current local clock. The certificates are included in the second message to 𝐴 who first validates its own certificate by checking whether identity and public key are correct, and whether 𝑇 is valid and the certificate therefore current. If 𝐶𝐴 is valid and has been issued timely, 𝐴 goes on by verifying the identity of 𝐵 and the timestamp 𝑇 in 𝐶𝐵, before it retrieves 𝐵’s public key 𝑃𝐵. 𝐴 then chooses a fresh communication key 𝑘𝑐 and signs it with its private key 𝑆𝐴, together with the timestamp 𝑇 from the certificates 𝐶𝐴 and 𝐶𝐵. Finally, it encrypts the certificate for the communication key under 𝑃𝐵 such that only 𝐵 can obtain 𝑘𝑐, and forwards it together with the server certificates 𝐶𝐴 and 𝐶𝐵 to 𝐵. 𝐵 receives the last message and, similarly to 𝐴, validates its own certificate and retrieves 𝐴’s public key from 𝐶𝐴. Afterwards, 𝐵 decrypts 𝐴’s certificate containing 𝑘𝑐 with 𝑆𝐵 and then verifies it with 𝑃𝐴. To ensure that 𝑘𝑐 is not a replay, 𝐵 moreover checks 𝑇 contained in the certificate issued by 𝐴, before it finally accepts 𝑘𝑐. Ambiguities regarding the Message Structure The paper of Denning and Sacco is not completely clear when it comes to the origin of the timestamp in the communication key certificate issued by 𝐴 and sent to 𝐵 in message (3). Recognized literature commonly interprets the protocol such that the timestamp in the certificate for the communication key originates from 𝐴 instead of the 𝐴𝑆 (e.g., [1], [2], [8], [22]). This interpretation would leave the third message with the following structure: 3. 𝐶𝐴, 𝐶𝐵, {{𝑘𝑐, 𝑇𝐴}𝑎𝑆𝐴 }𝑎 𝑃𝐵 𝑇𝐴 denotes a new timestamp with the value of 𝐴’s local clock at the time the third message is created. This interpretation allows for an attack in which 𝐵 can masquerade as 𝐴 and reuse 𝐴’s certificate to establish communication with a third user in the name of 𝐴. We will discuss this attack in more detail in the next section. It was a little bit surprising that none of the existing literature about the Denning-Sacco protocol with public keys interpreted the protocol such that 𝐴 reuses the timestamp from the server certificates. From our point of view, this is the more logical interpretation since all timestamps are denoted with the same identifier 𝑇 . It also makes the protocol more efficient, since 𝐵 only needs to check that the timestamps are the same and then ensure its validity for one of those timestamps. One could argue that Denning and Sacco do not indicate in the scope of their paper that checks on the relation of 40 3.3 Selected Protocols and Conducted Analyses timestamps in different certificates are performed. We claim that it is reasonable to assume that 𝐴 compares the timestamps in the server certificates before it reuses one of them in the certificate for the communication key. Consequently, if 𝐴 performs such a check, so does 𝐵. We therefore argue that our interpretation of the protocol and the behavior of principals is reasonable in itself. Nevertheless, we also wanted to make sure that our research on the Denning-Sacco protocol is sound with respect to the protocols originally intended structure. From personal communication with Giovanni Maria Sacco, one of the protocol’s authors, we got the confirmation that our interpretation of the protocol is valid and the timestamp in 𝐴’s certificate is actually the same timestamp that the server used in the public key certificates. Documented Attacks Abadi and Needham [1] were the first to find an attack on the Denning-Sacco protocol with public keys. Their attack bases on the interpretation of the protocol where 𝐴 uses the value of its current local clock for the timestamp in the communication key certificate. It was later mentioned again by Anderson and Needham in [2] and also recognized in general authentication protocol literature such as [8]. Abadi and Needham regard the public key certificates provided by the 𝐴𝑆 as black boxes so that no checks are performed regarding the relation of possible timestamps they contain. The attack they describe can thus be carried out by a malicious 𝐵 in two parallel sessions as follows: Session 1: 1. (3) 𝐴→ 𝐼 (𝐵) : 𝐶𝐴, 𝐶𝐵, {{𝑘𝑐, 𝑇𝐴}𝑎𝑆𝐴 }𝑎 𝑃𝐵 Session 2: 2. (1) 𝐼 (𝐵) → 𝐴𝑆 : 𝐴,𝐶 3. (2) 𝐴𝑆 → 𝐼 (𝐵) : 𝐶𝐴, 𝐶𝐶 4. (3) 𝐼 (𝐵) → 𝐶 : 𝐶𝐴, 𝐶𝐶 , {{𝑘𝑐, 𝑇𝐴}𝑎𝑆𝐴 }𝑎 𝑃𝐶 In Session 1, 𝐴 establishes communication with 𝐵. 𝐵 continues in a new session by requesting new certificates for the public keys of 𝐴 and a third user 𝐶 from the 𝐴𝑆. The 𝐴𝑆 responds to 𝐵 by issuing the requested certificates. As stated, the attack abstracts from the actual contents of the certificates, so we may just assume that they suffice to distribute public keys and to provide reassurance of their correctness. Hence, 𝐵 obtains 𝐶’s public key 𝑃𝐶 from 𝐶𝐶 , re-encrypts the certificate for 𝑘𝑐, which was originally issued by 𝐴 in the third message of Session 1, with 𝑃𝐶 , and finally forwards the public key certificate and the re-encrypted communication key certificate to 𝐶. When 𝐶 receives this message from 𝐵, it successfully verifies 𝐶𝐴 and 𝐶𝐶 , obtains 𝐴’s public key 𝑃𝐴, decrypts the last part using 𝑃𝐶 , and finally uses 𝑃𝐴 to verify the signature of 𝐴 containing 𝑘𝑐 and 𝑇𝐴, which consequently must originate from 𝐴. If 𝑇𝐴 is valid, 𝐶 accepts 𝑘𝑐 assuming it has established a secure channel with 𝐴, when in fact it is talking to the attacker. Although we clarified in Section 3.3.3 that the attack does not fully reflect the properties of the original protocol as specified by Denning and Sacco in [16], it is still interesting because it highlights the subtlety required in the specification of security properties regarding assumptions about the protocol’s structure and also its implementation. Moreover, it once again shows the importance of a core principle for the design of security protocols – robustness [7] –, that messages should include all the information to unambiguously authenticate them. This particularly holds true for the 41 3 Related Work inclusion of key peer identities where they are not clear, for example, the inclusion of 𝐵’s identity in 𝐴’s signature in the third message of the Denning-Sacco protocol containing the communication key 𝑘𝑐, which is generated by 𝐴 for secret communication with 𝐵. Security Proofs There are no formal security proofs of the Denning-Sacco protocol in existing literature that we know of. Generally, there seems to be a lack of effort regarding the symbolic analysis of the Denning-Sacco protocol. This lack may come from the fact that the protocol includes timestamps, which are hard to model, and for which it is hard to express security properties in a symbolic setting because this presupposes the existence of a global notion of time that cannot be controlled by the attacker, but does not restrict it either. One example for a symbolic prover that has been used to analyze the Denning-Sacco protocol is the AVISS tool [3]. In their work, the authors state that they could find one man-in-the-middle attack on the protocol, which was previously not documented. However, they neither explain how the attack can be carried out nor what assumptions have been made and what the exact outcome of the attack is. We counteract the shortage of sufficiently documented formal analyses of the Denning-Sacco protocol with a detailed symbolic security proof for the protocol with DY* in Section 4.5 of this thesis. 42 4 Analysis of the Selected Protocols In the course of this thesis, we performed an elaborate security analysis of three cryptographic protocols concerned with authentication and key exchange with the DY* symbolic prover. The investigated protocols are the Otway-Rees protocol [27], the Yahalom protocol [11], and the Denning-Sacco protocol with public keys [16]. This chapter documents the procedure and results of our analysis in full detail and further puts our results in a context with results of other approaches – summarized in Section 3.3 – where they can be interpreted. 4.1 General Procedure Each analysis follows roughly the same procedure. We start by creating a precise outline of the protocol in question based on its formal description taken from the paper in which the protocol was first presented or formalized. Our main goal in this phase of the analysis is to answer questions about the following protocol properties or goals that are bound to those properties: • principal roles, e.g., users, authentication servers, initiator, responder, etc.; • initial knowledge of principals, e.g., other principals’ identities, or previously established long-term or public keys; • messages, i.e., origin, destination and structure of messages; • generated nonces, i.e., origin, purpose and intended audience of generated nonces; • exchanged keys or secrets, i.e., keys or secrets that are established as a result of a protocol run and their intended audience; and • authentication goals. The question of message origin, destination, and structure has already been answered in Section 3.3. Given the formal outline of the protocol, we continue by developing a symbolic model of the protocol in the labeled security layer of DY*. To ensure the correctness of our model, we verify it with F* and check whether its execution results in a reasonable trace. We also substantiate the coherence of our model with the actual protocol as depicted in Section 3.3 and with the properties elaborated in our outline by explaining the key parts of the model in greater detail. In case of ambiguities in the protocol description, we furthermore justify the validity of our interpretation and the resulting parts of the model. Having established correctness and validity, we derive security properties that can be expressed in DY* from the protocol goals defined in our formal outline of the protocol, complement them with our own suggestions, and finally formulate them in terms of our DY* model. Since the security properties are bound to the model, they are verified together with the model using F*. If the specified security properties cannot be proven, we explore resulting attack 43 4 Analysis of the Selected Protocols vectors and augment our DY* model based on found attacks. Additionally, we propose minimal changes sufficient to counter the deficiencies of the protocol and then apply these fixes to the DY* model with the ultimate goal to prove the remaining security properties in the enhanced model, and hence complete the security proof of the protocol. In the last part of the analysis, we compare our results to the results of other proof efforts or analyses, i.e., those outlined in Section 3.3. That is, we look at other security proofs and the concrete security properties proven by them as well as documented attacks, and put them into a context with the security properties and attacks we were able to model and verify in DY*. We then interpret differences and similarities in the results of our approach and other approaches under consideration of the general proof setting, the attacker model (i.e., active or passive) and attacker capabilities, as well as assumptions and abstractions made in this and in other approaches. 4.2 DY* Models and Source Code Repository The complete source code of the DY* models of the authentication protocols analyzed as part of this master’s thesis has been published in a GitHub repository [21]. In total, the repository contains five DY* models, where each model represents one of the three investigated protocols or variations of these protocols, possibly based on different assumptions. Each DY* model divides into a set of modules that model different parts of the protocol, e.g. messages, protocol states, the individual protocol steps performed by honest principals, or possible attacks carried out by the DY* adversary. In particular, the repository comprises the following five DY* models: • otway-rees: contains a model of the original Otway-Rees protocol • otway-rees-fixed: contains a model of an improved version of the Otway-Rees protocol that prevents known attacks on the protocol and renders it secure with respect to the goals of the original version (see Section 4.3.1) • yahalom: contains a model of the Yahalom protocol, including a security proof based on the properties and goals stated in Section 4.4.1 • denning-sacco: contains a model of the Denning-Sacco protocol and a DY* extension to capture protocol properties dependent on timestamps, resulting in an incomplete security proof regarding the properties and goals stated in Section 4.5.1 • denning-sacco-central-auth: contains the Denning-Sacco model, but defines the authenti- cation server as a global singleton to account for some shortcomings of DY* that render a general security proof of the protocol in DY* as yet impossible To illustrate our work and the results of our analyses, we will use selected code examples from the DY* models listed above. 44 4.3 Otway-Rees 4.3 Otway-Rees This section comprises the analysis of the Otway-Rees protocol. We show that the protocol as originally proposed and described by Otway and Rees [27] does not achieve intended secrecy a