Proofs with Authenticators

In the last episode, we've shown that by adding the identity of the peer inside the signature as in \((\mathit{I_{Bob}}, g^b, \operatorname{sign_{Bob}}(g^a, g^b, \mathit{I_{Alice}}))\), we've fixed the unknown key share attack. What we didn't cover was how to prove that the resulting KE protocol is indeed secure. One elegant way to achieve this is by using Authenticators.

The UM and AM Link Models

Up until now, we've used the unauthenticated messages' link model (UM model). In that model, we've assumed that the attacker had active capabilities. In addition to passive capabilities like eavesdropping, an attacker could also

  • change messages on the links. It should be noted that in addition to the ability to modify the body of the messages, the attacker is also able to change message headers.
  • inject messages into the link, especially inserting her own messages.

To simplify proofs, we introduce the authenticated messages' link model (AM model). In that model, the attacker essentially turns into a passive one. In other words, she cannot change or insert messages on the link... but she may prevent delivery of messages.

It is much easier to define security in the AM link model, because the adversary is much more constrained. If we could specify an KE protocol that is secure in the AM model (and that includes of course a formal security proof), and then somehow "translate" that protocol into the UM model without losing the security requirements, we would have a secure KE protocol for the real world. One way to achieve this is an Authenticator.

As an example: unauthenticated Diffie-Hellman is secure under the AM model under the DDH assumption (Decisional Diffie-Hellman, i.e. that \((g^x, g^y, g^{xy})\) is indistinguishable from \((g^x, g^y, g^z)\) for all \(z\) uniformly chosen at random). Why is that so? Well, under this assumption, any attacker is purely passive, so that e.g. no man in the middle attack can occur.

Authenticators

Formally defining authenticators[BCK98] requires a lot of concepts that we haven't talked about here. Instead of showing a formal definition for an authenticator, we'll introduce authenticators informally, since it is much easier to grasp.

Message Passing Protocols

Since authenticators are a special kind of message passing protocol, let's start with those:

Informal Definition (message passing protocol): A message passing protocol is a possibly interactive protocol where parties send and receive messages and register their actions (registrations can be of the form "received \(m\) from A", "sent \(m\) to \(B\)").

If registering actions seem strange to you, just imagine that Alice and Bob write a line into their own log file each time they send or receive a message. That line contains the message, and the identity of the peer... or what they think that identity may be.

For example, KE protocols fall under this category (we could imagine that they have a verbose option to turn logging on).

Definition of Authenticators

As said, an authenticator is special kind of message passing protocol:

Informal Definition (Authenticator): An Authenticator is a message passing protocol, such that whenever \(A\) registers "received \(m\) from \(B\)", it also holds that \(B\) registers "sent \(m\) to \(A\)".

What does that mean? If Alice is convinced that she received a message \(m\) from Bob (she registered "received \(m\) from \(\mathit{Bob}\)"), then Bob must have actually sent that message \(m\) to Alice (he registered "sent \(m\) to \(\mathit{Alice}\)"). Messages can get lost in transit, since an attacker can prevent the delivery of messages, but if they do arrive, not only are they unchanged (\(m\) stays the same in both Alice's and Bob's registrations), but there's a guarantee that the message received by Alice is identical to the message sent by Bob.

Authenticators as Protocol Compilers

The most important point to take away from this article is:

an authenticator is a "compiler" that translates an AM-secure protocol into a UM-secure protocol.

This is possible because of the following theorem.

Theorem (Authenticator Theorem): Let \(A\) be an authenticator.

  • if \(P\) is a protocol secure in the AM model,
  • and \(P'\) is the protocol resulting from applying \(A\) to each message in \(P\)

then \(P'\) is secure in the UM model.

In other words: given an authenticator, we can turn a message passing protocol that is secure in the easy idealized AM model into a message passing protocol that remains secure in the hairier real-world UM model. All we need to do is to apply this authenticator to each message (sent and received) in the AM model. The term "applying" is used informally here. In reality, what happens is some kind of composition of two message passing protocols: \(P\) and \(A\).

If we can prove the security of the protocol \(P\) in the AM model, simply by applying an authenticator \(A\) to that protocol gives us a protocol \(P'\) that is secure in the UM model "for free".

Exercise 1: Does the condition for the authenticator still hold when an attacker suppresses delivery of a message in the AM-model? In the UM-model? Explain.

Exercise 2: An attacker can't inject messages in the AM model, but in the UM model, she may replay messages sent from Alice to Bob. How does the protocol \(P'\) derived from \(P\) by applying an authenticator reacts to such replay attacks? Are mitigations such as adding counters, timestamps and the like needed?

Now, you may be left wondering if authenticators exist, and if so, how they look like.

A signature-based Authenticator

It turns out that authenticators not only exist, some of them are quite short and sweet. Here's an easy one[JG06]. Replace \(A \rightarrow B \colon \mathit{msg}\) by:

Signature-based authenticator (applied to message \(A \rightarrow B \colon \mathit{msg}\)):

  1. \(A \rightarrow B \colon (A, \mathit{msg})\)
  2. \(A \leftarrow B \colon (B, \mathit{nonce})\)
  3. \(A \rightarrow B \colon (A, \operatorname{sig}_A(\mathit{msg}, \mathit{nonce}, B))\)

Now, for each message \(\mathit{msg}\) of the secure protocol \(P\) in the AM model, apply this authenticator, and you get a secure protocol \(P'\) in the UM model. Easy, isn't it? Of course, this transformation (compilation) of protocols adds overhead in the form of additional messages, but that's a small price to pay for security.

Proving ISO-9796 secure using the Sig-Authenticator

Recall the ISO-9796 protocol:

  1. \(A \rightarrow B \colon (A, g^a)\)
  2. \(A \leftarrow B \colon (B, g^b, \operatorname{sig_{B}}(g^a, g^b, A))\)
  3. \(A \rightarrow B \colon \operatorname{sig_{A}}(g^a, g^b, B)\)

 Let's see how to prove that this protocol is UM-secure. We start with the simpler protocol in the AM model:

  1. \(A \rightarrow B \colon g^a\)
  2. \(A \leftarrow B \colon g^b\)

This is merely the good ole unauthenticated Diffie-Hellman KE protocol. Remember that under the DDH assumption, this protocol is secure in the AM model. There are two messages \(g^a\) and \(g^b\) in this protocol. To each of these messages, we apply the sig-authenticator independently.

Applying the Sig-Authenticator to the Message from Alice to Bob

We start by applying the signature authenticator to the message \(g^a\) like so: we set the message that \(A\) sends to \(B\): \(\mathit{msg} := g^a\). We also set the nonce that \(B\) sends back to \(A\): \(\mathit{nonce} := g^b\). This we can do, since for all practical purposes, the ephemeral \(g^b\) has all the characteristics of a nonce, provided the cyclic group of \(g^b\) is large enough. We transform the first message \(A \rightarrow B \colon \mathit{msg}\) according to the sig-authenticator like this:

  1. \(A \rightarrow B \colon (A, \mathit{msg} (= g^a))\)
  2. \(A \leftarrow B \colon (B, \mathit{nonce} (= g^b))\)
  3. \(A \rightarrow B \colon \operatorname{sig_{A}}(\mathit{msg}, \mathit{nonce}, B) (= \operatorname{sig_{A}}(g^a, g^b, B))\)
Applying the Sig-Authenticator to the Message from Bob to Alice

Now, for the other direction. We apply again the signature authenticator to the message \(g^b\), by setting \(\mathit{msg} := g^b\). We set the nonce to \(\mathit{nonce} := g^a\). Remember that since \(g^a\) has all the characteristics of a nonce, we are allowed to do this. We then apply the sig-authenticator to the message \(A \leftarrow B \colon \mathit{msg}\). We obtain:

  1. \(A \leftarrow B \colon (B, \mathit{msg} (= g^b))\)
  2. \(A \rightarrow B \colon (A, \mathit{nonce} (= g^a))\)
  3. \(A \leftarrow B \colon \operatorname{sig_{B}}(\mathit{msg}, \mathit{nonce}, A) (= \operatorname{sig_{B}}(g^b, g^a, A) = \operatorname{sig_{B}}(g^a, g^b, A))\)
Combining both substitutions

We now combine both protocols, collecting the messages sent, and taking care of dependencies (i.e. send a message \(m_1\) that depends on message \(m_0\) only after we received \(m_0\)):

  1. \(A \rightarrow B \colon (A, g^a)\)
  2. \(A \leftarrow B \colon (B, g^b, \operatorname{sig_{B}}(g^a, g^b, A))\)
  3. \(A \rightarrow B \colon \operatorname{sig_{A}}(g^a, g^b, B)\)

and this is exactly the ISO-9796 protocol!

Note that instead of blindly concatenating the 3 messages resulting from \(A \rightarrow B \colon g^a\) with the 3 messages resulting from \(A \leftarrow B \colon g^b\), creating a 6 message handshake, we slightly reordered the resulting messages before combining them. In fact, for the second message with \(g^b\), we used a variant of the sig-authenticator that sends the nonce before the message, i.e. that swapped step 1 and 2:

  • \(A \leftarrow B \colon (B, \mathit{nonce})\)
  • \(A \rightarrow B \colon (A, \mathit{msg})\)
  • \(A \rightarrow B \colon (A, \operatorname{sig}_A(\mathit{msg}, \mathit{nonce}, B))\)

The authenticator theorem as stated above doesn't cover this, but in can be proven that this variant is not only an authenticator too, but that the result is still secure in the UM model. We'll ignore this issue in the following.

Proof(-sketch) that ISO-9796 is secure

By the authenticator theorem above, since unauthenticated Diffie-Hellman is secure under the DDH assumption in the AM model, and since ISO-9796 is the result of applying the sig-authenticator to unauthenticated Diffie-Hellman, it follows that ISO-9796 is secure under the DDH assumption in the UM model. \(\Box\)

PK-Encryption based Authenticator

Signature-based authenticators aren't the only game in town. By starting with unauthenticated Diffie-Hellman, and applying a different authenticator, we obtain a different authenticated Diffie-Hellman protocol that is secure in the UM model. One such authenticator uses public keys and MACs like so:

PK-Encryption-based authenticator (applied to message \(A \rightarrow B \colon \mathit{msg}\)):

  1. \(A \rightarrow B \colon (A, \mathit{msg})\)
  2. \(A \leftarrow B \colon (B, \operatorname{Enc}(\mathit{pk}_A, k))\)
  3. \(A \rightarrow B \colon (A, \mathit{msg}, \operatorname{MAC}(k, \mathit{msg}, B))\)

where \(\mathit{pk}_A\) is the public key of \(A\), \(k\) is an ephemeral random key suitable to MACing, and \(\operatorname{MAC}(k, \mathit{msg}, B)\) computes the MAC of \(\mathit{msg} || B\) with the key \(k\).

Exercise 3: Apply the PK-Encryption-based authenticator in both directions to unauthenticated Diffie-Hellman, just like we did above with the sig-based authenticator. Show the resulting protocol.

Solution to Exercise 3: We get:

  1. \(A \rightarrow B \colon (A, \operatorname{Enc}(\mathit{pk}_B, k_1))\)
  2. \(A \leftarrow B \colon (B, g^b, \operatorname{MAC}(k_1, g^b, A), \operatorname{Enc}(\mathit{pk}_A, k_2))\)
  3. \(A \rightarrow B \colon (A, g^a, \operatorname{MAC}(k_2, g^a, B))\)

This happens to be the SKEME protocol[K96] in IPSec's IKEv1.

Designing KE Protocols with Authenticators

We've seen that just by using different authenticators, we can effectively design new key exchange protocols. Authenticators can thus function as a protocol design tool. While this paradigm can generate useful and sometimes beautiful protocols, it is not a panacea. Some resulting protocols are often way too technical and overly complex, but on the flip side, they have the advantage of being free of hidden flaws. Whether authenticator-designed KE protocols are the way of the future, remains to be seen.

The KE Saga Continues...

This concludes this crypto bite, but it is not the end of the KE protocol design saga. In the next article, we'll explore the STS protocol, which tries to provide privacy, but fails at UKS. The lessons learned from STS will ultimately lead to the design of the SIGMA protocols.

Sources

This article is my transcript and understanding of the first 29 minutes of Hugo Krawczyk's talk "Diffie-Hellman Protocols and Authenticators" at the 8th BIU Winter School on Cryptography on Secure Key Exchange, February 11-15 2018 (all videos). Slides (pages 48-59).

Literature

  • [K96] Hugo Krawczyk: SKEME: a versatile secure key exchange mechanism for Internet. In: Network and Distributed System Security, Symposium on(SNDSS) DOI. (IEEE, paywalled; computer.org, paywalled)
  • [JG06] Shaoquan Jiang, Guang Gong: Efficient Authenticators with Application to Key Exchange. In: Won D.H., Kim S. (eds) Information Security and Cryptology - ICISC 2005. ICISC 2005. Lecture Notes in Computer Science, vol 3935. Springer, Berlin, Heidelberg (springer.com, paywalled)
  • [BCK98] Mihir Bellare, Ran Canetti, and Hugo Krawczyk: A Modular Approach to the Design and Analysis of Authentication and Key Exchange Protocols (iacr.org 1998/009)
  • [S99] Victor Shoup: On formal models for secure key exchange (version 4), November 15, 1999 revision of IBM Research Report RZ 3120 (April 1999) (full pdf)