Paper addressing two questions regarding the EMV® ECC Key Agreement protocol

Security Advisories

EMVCo Preface (April 2015) ECC Blinded Diffie-Hellman security analysis It is planned that EMV Next Generation will use an ECC (Elliptic Curve Cryptography) Key Agreement protocol called Blinded Diffie-Hellman. This was first presented by EMVCo in the EMV RFC www.emvco.com/specifications.aspx?id=243 Below is a paper by Professor Nigel Smart that supplements the security analysis and proof given in: Christina Brzuska, Nigel P. Smart, Bogdan Warinschi, and Gaven J. Watson. An analysis of the EMV channel establishment protocol. ACM Conference on Computer and Communications Security – ACM CCS 2013, 373–386, 2013 an earlier version of which can be found at http://eprint.iacr.org/2013/031.pdf This paper addresses two questions regarding the EMV ECC Key Agreement protocol:  "Can the terminal go first?", and  "Must the blinding factor be full size?" Questions on the EMV Key Agreement Protocol ‘WHO GOES FIRST?’ AND ‘HOW BIG IS THE BLIND?’ BY NIGEL SMART Thynnus Limited MARCH 15, 2015 Table of Contents 1 Introduction 2 Security Definitions 3 Weak Key Secrecy 4 The Full Analysis 1

Introduction

This report discusses the EMV Key Agreement protocol which was formally analysed in [1]. The report answers two key questions: 1. Whether the security proof is affected by the terminal sending its message before the card. 2. What is the affect on the security proof of the size of the card’s ephemeral secret? In this document we refer to what in the EMV document is called the "blinding factor" as the card’s ephemeral secret key. This is because the role of this value is not only to blind the public key, but also provides entropy of the card into the key agreement process. This is done via means of a novel ephemeral public key (using the public key as a base point), for which the "blinding factor" is the associated ephemeral secret key. The original protocol is described in Figure 1, and it is to this protocol that the paper [1] addresses its analysis. For the first question we shall be considering the modified protocol in Figure 2; note the only difference is in the order of the first two messages. The second question is related to how the element a should be chosen; in [1] it is recommended to be selected from the full range of the finite field Fq uniformly at random. In both protocols the reader should note that if the card ephemeral secret key a, a.k.a. blinding factor, is equal to one, then the key agreement part of the protocol becomes what is known in the literature as "one-sided static Diffie–Hellman". This is the genesis of the EMV protocol. However, one-sided static Diffie–Hellman on its own does not provide a secure key agreement protocol (without other mechanisms being added, such as additional message flows). This report will show that if the card’s value of a is not chosen uniformly at random then the security proofs of all properties of the EMV protocol break down (including message privacy, entity authentication and message authentication). Rather than essentially reproduce the paper [1] with changes marked this report will discuss the various aspects of the paper in relation to the above points and explain their relevance to the questions above. Readers wishing to understand the technical details in more depth should consult the paper [1]; which includes full definitions and a historical discussion in addition to the proofs explained here. One main reason for doing this is that much of [1] discusses how the security of the key agreement phase (the upper part of the Figures 1 and 2) composes with the secure channel phase (the lower part), and in addition what security properties are needed of the secure channel protocol and how to achieve such properties. The paper [1] discusses two issues: Whether the key agreement protocol provides a form of anonymity for the card, as well as whether the key agreement protocol is itself secure. In this report we do not discuss in detail issues related to anonymity since it is clear how the size of the 3 Card (C) Terminal (T) a ←r Fq (κCe, κCd) = H(daE) A=aQC −−−−−−−−→ E=eP ←−−−−−−−− e ←r Fq (κTd, κTe) = H(eA) ch (ch, stCe) = SendChκC (certC a QC; st C e) −−−−−−−−→ (certC a QC, stTd) = ReceiveChκT (ch; stTd) e d Check verpk(certC, QC) =? true Check aQC =? A (ch1, stCe) = SendChκC (m1; stCe) e ··· (m2, stCd) = ReceiveChκC (ch2; stCd) d ch1 −−−−−−−−→ ch2 ←−−−−−−−− (m1, stTd) = ReceiveChκT (ch1; stTd) d ··· (ch2, stTe) = SendChκT (m2; stTe). e Fig. 1. The Original EMV Key Agreement Protocol Card (C) Terminal (T) E=eP ←−−−−−−−− e ←r Fq a ←r Fq (κCe, κCd) = H(daE) A=aQC −−−−−−−−→ (κTd, κTe) = H(eA) ch (ch, stCe) = SendChκC (certC a QC; st C e) −−−−−−−−→ (certC a QC, stTd) = ReceiveChκT (ch; stTd) e d Check verpk(certC, QC) =? true Check aQC =? A (ch1, stCe) = SendChκC (m1; stCe) e ··· (m2, stCd) = ReceiveChκC (ch2; stCd) d ch1 −−−−−−−−→ ch2 ←−−−−−−−− (m1, stTd) = ReceiveChκT (ch1; stTd) d ··· (ch2, stTe) = SendChκT (m2; stTe). e Fig. 2. The Modified EMV Key Agreement Protocol card’s ephemeral secret affects the anonymity property1. Thus all of our discussion in relation to the second question is about how the size affects the security of the key agreement aspects. The report is structured as follows: In Section 2 we give a slightly informal discussion of the relevant security properties which we require; this is just a simplified statement of the definitions to be found in [1]. In Section 3 we discuss the main guts of the proof where most of the analysis 1 Technically, the unlinkability/anonymity is proved to hold in [1] if the authenticated encryption scheme is CCA secure and the Gap Diffie–Hellman problem is hard. The authenticated encryption protects the public key upon transport to the terminal, and the Gap Diffie–Hellman problem ensures it is sufficiently blinded in the key agreement part of the protocol. The Gap Diffie– Hellman problem requires that the full range card ephemeral key. In addition practical attacks which break the anonymity are known if the ephemeral key is selected to be too short. 4 for this report focused on. Then in Section 4 we discuss the parts of the analysis in [1] which are relevant to the questions above. Summary: The proof does hold if the terminal goes first. No security guarantees at all can be provided by the proof if the card’s ephemeral secret is not selected from the uniform distribution over Fq. 5 2 Security Definitions The EMV protocol only provides one-sided authentication, only the card is authenticated, thus our security definitions for key agreement security are of a one-sided variant which were introduced formally in [1]. In this section we outline these properties informally: WEAK ONE-SIDED ENTITY AUTHENTICATION: Informally this property ensures that a genuine card is authenticated to an unauthenticated terminal. The paper [1] defines a relevant security game and gives an associated advantage statement; the property is named weak one-sided entity authentication as the obvious notion of one-sided entity authentication leads to an attack against the EMV protocol which is not relevant in real life. The property is defined as the probability that the adversary can make certain "bad" events happen; events which will contradict the security goal of weak one-sided entity authentication. A protocol is deemed secure if one can then prove that this advantage is small for all polynomial time adversaries A. In particular the definition is Definition 1. (Weak One-Sided EA (OS-EA)) A protocol P = {Π, G} is a (t, wEA)-secure weak OS-EA protocol if for all adversaries Aent running in time at most t, AdvΠwos-entauth(Aent) ≤ wEA. The reader should note that the term weak here is so as to distinguish the property from a strong notion of one-sided entity authentication. As discussed in [1] the strong notion is irrelevant for the use-case of the EMV system, and hence the weaker notion of entity authentication is perfectly suitable for the purposes of EMV. ONE-SIDED MESSAGE AUTHENTICATION AND PRIVACY: Informally this property ensures that the messages transmitted across the established secure channel are both private and are authenticated in the sense they have been sent be the relevant parties who have participated in the key agreement phase. Again the paper [1] defines a formal security game, and defines relevant advantages given by the probability of an adversary making certain events happen. The formal definitions for these two properties are then given by Definition 2. (OS-MA/OS-MP) A protocol P = {Π, G} is a (t,)-secure OS-MA protocol (or OSMP resp.) if for all adversaries A running in time at most t, AdvoΠs-auth(A) ≤ (or AdvoΠs-priv(A) ≤ resp.). SUMMARY: The entire protocol is deemed to be secure if all three properties are satisifed. Definition 3. (OS-EAMAP) A protocol P = {Π, G} is a (t,)-secure OS-EAMAP protocol if it is a (t,)-secure OS-EA protocol, a (t,)-secure OS-MA protocol and a (t,)-secure OS-MP protocol. This report examines how the two questions stated at the beginning affect the three security definitions outlined above. MAIN THEOREM: The main theorem in [1] is the following 6 Theorem 1. If the Gap Diffie–Hellman problem is hard, the CDH problem is hard, AE = (enc, dec) is an ind-sfcca secure and int-sfptxt secure AE scheme, and the signature scheme (sig, ver) used to produce card certificates is EUF-CMA, then the EMV protocol P = {Π, G} in Figure 1 is secure in the sense of OS-EAMAP. In particular we have – If there exists an adversary A running in time at most t against the entity authentication property of OS-EAMAP security then there are adversaries B,C, D, E, F, such that AdvwΠos-entauth(A) ≤ 2 · Adve(suifgc,mvear)(B) + nC · (1 − 1/|h|) · AdvGEa(pF-pD) H(C) + nS · nC · AdviAnEt-0(D) + n2C · AdvCED(FHp)(E) + nS · nC · AdvDEL(Fp)(F), where B, C, D, E, F each run in time t + O(µ) where µ is total number of bits queried. – If there exists an adversary A running in time at most t against the message authentication property of OS-EAMAP security then there are adversaries B, C and D, such that AdvoΠs-auth(A) ≤ nS·(nC +nT)·AdviAnEtsfptxt(D)+nC ·(1−1/|h|)·AdvGEa(pF-pD) H(C)+AdvΠwos-entauth(B), where B runs in time t and, C and D each run in time t + O(µ) where µ is total number of bits queried. – If there exists an adversary A against the message privacy property of OS-EAMAP security then there are adversaries B, C and D, such that AdvΠos-priv(A) ≤ nS·(nC +nT)·AdviAnEdsfcca(D)+nC ·(1−1/|h|)·AdvGEa(pF-pD),H(C)+AdvwΠos-entauth(B), where B runs in time t and, C and D each run in time t + O(µ) where µ is total number of bits queried. where nC is the number of cards in the system, nT the number of terminals, nS the number of sessions and |h| is the output size of the hash function. Note that message privacy and message authentication of the established secure channel (i.e. AdvoΠs-auth and AdvoΠs-priv in the above theorem) depend on the security of the entity authentication of the key agreement protocol (i.e. AdvΠwos-entauth). Our task is to examine this theorem in the light of the two questions at the start of this report; i.e. in relation to the modified protocol in Figure 2 and in relation to the distribution of the value of a selected by the card 7 To understand the main theorem we first need to understand the security properties related to the various building blocks. The theorem only holds if the following advantages are negligible, or equivalently the associated building blocks are secure. – Adve(suifgc,mvear): This is essentially the security of the signature scheme used in the certificate for the cards public key. – AdviAnEtsfptxt: This relates to the integrity protection provided by the authenticated encryption scheme used to implement the secure channel. – AdviAnEt-0: Is a related notion to intsfptxt but is slightly weaker. – AdviAnEdsfcca: This relates to the privacy protection provided by the authenticated encryp- tion scheme used to implement the secure channel. – AdvEGa(pF-pD) H: This is the standard gap-Diffie–Hellman problem for the elliptic curve group. – AdvCED(FHp): This is the standard computational Diffie–Hellman problem for the elliptic curve group. – AdvDEL(Fp): This is the standard discrete logarithm problem for the elliptic curve group. In this report only the last three terms will be of relevance to our analysis. For example let us look at the least well known of these problems: Definition 4. (Gap Diffie–Hellman Problem) Let ODDH be an oracle that solves the DDH problem in G, i.e. takes as input rP, sP, tP ∈ G, and outputs one if tP = rsP and zero otherwise. The Gap Diffie–Hellman problem then asks that given aP, bP ∈ G where a, b ←r Fq, and access to ODDH, compute abP (i.e. solve CDH). The advantage of an adversary A against the Gap Diffie– Hellman problem is defined by AdvGGap-DH(A) = Pr[a, b ←r Fq: AODDH(aP, bP) = abP ]. The Gap Diffie–Hellman problem is a stronger assumption than the Diffie–Hellman problem. However, it is widely accepted in much of the provable security community as a reasonable assumption on which to base security. Many standardized protocols and encryption schemes, for example ECIES, have security proofs which reduce to the Gap Diffie–Hellman problem. The most important point to note for this report is that the problem is based on the fact that two random values a and b are selected uniformly at random from Fq. If this selection does not happen in this way then we not have the gap-Diffie–Hellman problem; we will have a different problem. This different problem may or may not be hard, and hence all security would rest on a non-standard assumption. The goal of provable security is to reduce security to well established standard problems, and thus reducing to non-standard problems is considered to be very poor practice. Thus in discussing our second problem we need to pay particular attention how if selecting the card’s ephemeral secret in a different way will affect the reduction to the above gap-Diffie– Hellman problem. Similar discussions apply to the computational Diffie–Hellman problem and the discrete logarithm problem: 8 Definition 5. (Computational Diffie–Hellman Problem) The Computational Diffie–Hellman problem then asks that given aP, bP ∈ G where a, b ←r Fq, compute abP The advantage of an adversary A against the Computational Diffie–Hellman problem is defined by AdvCGDH(A) = Pr[a, b ←r Fq: A(aP, bP) = abP ]. Again, the standard problem assumes a and b are selected uniformly at random from Fq. Definition 6. (Discrete Logarithm Problem) The Discrete Logarithm problem then asks that given aP ∈ G where a ←r Fq, compute a The advantage of an adversary A against the Discrete Logarithm problem is defined by AdvDGL(A) = Pr[a ←r Fq: A(aP) = a]. Again, the standard problem assumes a is selected uniformly at random from Fq. 9 3 Weak Key Secrecy In [1] the proof proceeds by first examining a simpler property called weak key secrecy. It is in fact this property for which our two main questions have most relevance. Hence, the most technical part of this report is devoted to this part of the paper [1]. The notion of weak key secrecy is related to the simpler sub-component of the protocol given in Figure 3 (where we denote the terminal going first as per our requirements). Card (C) Terminal (T) E=eP ←−−−−−−−− e ←r Fq a ←r Fq A=aQC −−−−−−−−→ κ = H(daE) κ = H(eA) Fig. 3. Unauthenticated Key-Agreement Scheme The property of weak key secrecy is relatively straight forward as it just focuses on the key agreement part of the protocol. We define the following game ExecwΠKSec(A) between an adversary A and challenger C: 1. The challenger C, generates public/secret key pairs for each user i ∈ I (by running G) and returns the public keys to A. 2. Adversary A is allowed to make as many NewSession, Send, Reveal, Corrupt queries as it likes. 3. Finally A outputs a pair Π∗ and κ∗. We say the adversary A wins the wKSec experiment if OSF(Π∗) = true and κ∗ is the key agreed by Π∗. In this case the output of ExecwΠKSec(A) is set to one, otherwise the output is zero. We define the advantage of A to be AdvKΠSec(A) = | Pr[ExecwΠKSec(A) = 1]|. Definition 7. (Weak Key Secrecy) P = {Π, G} is a (t, wKSec)-weak Key-secure AK protocol if for all adversaries A running in time t the following holds: 1. In the presence of a benign adversary on Πis and Πjt both oracles accept holding the same session identifier sid, the same session key κ and this key is distributed uniformly at random on {0, 1}k. 2. A’s advantage is bounded by AdvwΠKSec(A) ≤ wKSec. We now go through the proof of the key result in [1] about weak key secrecy of the protocol; with suitable changes made to reflect that in our case the terminal transmits their message first. We anotate the proof with comments which remarks how the proof technique relates to the second of our questions in relation to the choice of the card’s ephemeral secret a. 10 Lemma 1. The weak key secrecy of the reduced protocol π in Figure 3 is reducible to the Gap Diffie–Hellman assumption, i.e. we have for all adversaries A there exists an adversary B such that Advwπ KSec(A) ≤ nC · (1 − 1/|h|) · AdvGEa(pF-pD) H(B), where nC is the number of cards in the system and |h| is the output length of the hash function (which is modelled as a random oracle). Proof. Assume we have an adversary A against the key secrecy of π we shall use this to construct an adversary B against Gap Diffie–Hellman, where B is given the challenge aP, bP. Note that this implies that a and b are uniformly selected at random from Fq. The algorithm B begins by setting up nC authenticated participants by choosing a secret key di ←r Fq for each authenticated participant i ∈ C and sets the public key Qi = diP except for one participant i∗ ∈ C where we set the public key to aP. B also sets up nT unauthenticated participants. Algorithm B will then use its DDH oracle ODDH to provide simulations of A’s oracles as follows: – NewSession(i, ρ) – B starts a new session for i. All participants may have a total of ns sessions. – Send(πis, m) –

  • For i ∈ T (ρ = initiator), select at random βis ←r Fq to create message E = βisbP.
  • For i ∈ C (and ρ = responder), select at random αis ←r Fq to create message A = αisQi. This will result in a shared key κ = H (α s i∗ β s i∗ abP) for oracle πis∗ with partner πjt, where j ∈ T. Compared to [1] the role of initiator and responder have been switched around, as in our case the terminal goes first. However, we see that the value of the ephemeral key selected by the card is given by αis, which is not related to the input values a and b from the gap-Diffie–Hellman problem. Thus from the point of view of this part of the proof the card’s ephemeral secret can be selected to be from any sub-distribution of Fq. – Corrupt(i, d) –
  • For i ∈ C, then return di and replace it with d unless i = i∗ in which case abort
  • For i ∈ T, return ⊥. – Reveal(πis) – To answer Reveal queries, B will maintain a Guess session key list (G-List). Each element on the G-List is a tuple of the form (τ, i, j, κR). Queries are answered as follows:
  • First B checks the G-list and if there is an entry for i, j then B outputs the corresponding κR.
  • If not then B checks whether the H-list (see below) contains an (M, h, sth) with ODDH(αisQi, βisbP, M) = 1. If it does then B sets sth = {i, j} and adds to G-list (τ, i, j, h).
  • Otherwise B returns a randomly chosen key. – H(M) – To answer hash queries, B maintains an H-List containing tuples of the form (M, h, sth). Queries are answered as followed: 11
  • B first checks whether M is on the H-list. If it is, then B outputs h.
  • If not then B must check whether H(M) is already an valid entry on the G-list for some pair of participants (i, j) by calling its ODDH.
  • If it is a valid entry for some pair of participants (i, j) then B returns the corresponding κR from the G-list and adds (M, κR, {i, j}) to the H-list.
  • Otherwise B chooses a random hash h and adds (M, h, sth) to list. Eventually, A will output its guess π∗ = πis and κ∗, The probability that A chooses i = i∗ is 1/nC Note that in this case i∗ will not have been corrupted so the simulation has been perfect. At this point B searches the H-list for the entry (M ∗, κ∗, st∗κ) corresponding to κ∗, using ODDH to verify that the entry corresponds to i∗, j. If this entry does not exist then A must have output a random guess for the key, in which case his probability of success is at best 1/|h|, where |h| is the size of the output to the function H. Since we assume A to be a winning adversary with probability (1 − 1/|h|) A queries H such that his guess is on the H-list. If it is on the list then B calculates the solution to the gap-DH problem as (1/αis∗βis∗)M ∗. From the point of view of the weak key secrecy property there is no problem in selecting the card’s ephemeral secret from any distribution. This corresponds to our intuition about the security of the standalone one-sided static Diffie–Hellman problem; however this does not imply that the protocol built from this simpler reduced protocol is secure if the card ephemeral secret key is selected from any distribution. Indeed we will show that this naive intuition is false. On the positive side this part of the proof shows that it makes no difference who goes first. 12 4 The Full Analysis We now discuss the main proofs of [1]. To aid the discussion we refer to page number in the ePrint version of [1]2.

4.1 Weak One-Sided Authentication We first examine the proof of wos-entauth given in Lemma 2 on pages 17–20. The main inequality which is established is AdvwΠos-entauth(A) ≤ 2 · Adve(suifgc,mvear)(B) + Advwπ KSec(A) + nS · nC · AdviAnEt-0(D) + n2C · AdvCED(FHp)(E) + nS · nC · AdvDEL(Fp)(F), The only properties of the proof which concern us are the choice of the card’s ephemeral secret; since the property of who goes first is dealt with in the modified proof of wKSec given above (the relevant modifications in this respect to the proof of Lemma 2 are trivial and hence not discussed here). The card’s ephemeral secret comes into play in various parts of the proof. In most parts it is simply chosen according to the distribution inherent in the protocol, in other parts it is related to the input problem of the challenger. Thus we focus on these latter parts only, which are related to the CDH and DL terms in the above inequality; so we concentrate on just these two parts of the proof which we present below: PART (II): Consider for example part (ii); the bounding of the term denoted by Pr[notuni] in [1]. We reproduce this component below: Here we must consider the case when two card sessions establish the same key with a single terminal. Let A be an adversary against the uniqueness of sessions. We shall use A to construct a new adversary E that solves the CDH problem given challenge rP, sP. Algorithm E begins by setting up nC authenticated participants by choosing secret keys di ∈ Fq for each authenticated participant and sets the public keys to be Qi = diP. Except for two cards C1 and C2 chosen at random (note we also consider the case that C1 = C2). First E chooses d, a1 and a2 at random from Fq. Next E sets the public key of C1 to be Q1 = a−1 1drP and (when C1 = C2) the public key of C2 to be Q2 = a−2 1dP. E models A’s NewSession, Reveal, Corrupt, Send queries appropriately using the key material it has generated and necessary randomness. Except for cards C1 and C2 where Send queries are modelled such that: – Tj first sends sP – C1 responds with a1Q1 = drP to some terminal Tj. – The key established between C1 and Tj is H(d(rsP)). (To model any further send queries with type = ap or ch E, chooses this hash uniformly at random and uses this as the key to perform the necessary encryptions and decryptions.) – Next start a new session for C2 by responding to a terminal request with dP. In the case of C1 = C2 this corresponds to a2Q2 and in the case of C1 = C2 this corresponds to a2Q1 for some a2 ←r Fq. Finally, adversary A must impersonate the terminal and send rsP to C2. This will ensure that C2 establishes the same session key as the previous session of C1 and Tj, (κ = H(drsP)). The adversary E then uses A’s impersonated terminal message rsP as its CDH solution. Pr[notuni] ≤ n2C · AdvCED(FHp)(E). 2 This is ePrint number 2013/031 and is available from http://eprint.iacr.org/2013/031. 13 For this proof to work the distributions produced by the challenger must be the same as the distributions which the adversary expects to see. Let us examine the blinded public keys produced by the challenger, these are – a1Q1, in C1’s first session. – a2Q2, in C2’s session when C1 = C2. – a2Q1, in the case when C1 = C2. In particular we have that a2Q1 = dP and Q1 = a−1 1drP and so a2 = a1 · r−1. Suppose we select the card’s ephemerals secret keys from distribution D then we require that the challenger needs to select a1 and a2 from D and that no matter what choice of r from Fq we have that a2 is also selected as if distributed from D. This implies that D must be the uniform distribution on Fq. PART (III): Here the proof proceeds in bounding a term called Pr[os-notval ∧ ¬F ]. Again we reproduce this part of the proof below: We shall use A to construct an adversary F against the Discrete Log Problem with challenge rP. Algorithm F begins by setting up nC authenticated participants by choosing secret keys di ∈ Fq for each authenticated participant and sets the public keys to be Qi = diP. F models A’s NewSession, Reveal, Corrupt, Send queries appropriately using the key material it has generated and necessary randomness. Except for one card session Πis for which F sets the message it outputs to be d∗(rP), where d∗ is the long-term secret of some other card initialised by F with certificate cert∗. The protocol then proceeds as normal where Πis will be sent eP by its partner the terminal Πjt. If F has chosen the correct card session then A will now output a forged confirmation message encκd (cert∗, a∗, d∗P; ste), (recall A is permitted a Reveal query to obtain κd). Upon receipt of encκd (cert∗, a∗, d∗P; ste), B decrypts using κd and then outputs a∗ as the solution to the discrete log problem. Therefore, Pr[os-notval ∧ ¬F ] ≤ nS · nC · AdvDEL(Fp)(F) Again let us look at the values output by the challenger to the adversary for card responses. The input Discrete Logarithm problem has r selected uniformly at random from Fq. In the "target" session the challenger makes the card output a value d∗(rP), but the card public key for this session is diP, for di = d∗. The underlying ephemeral secret key is then equal to d∗ · r/di. Again this needs to be selected from a distribution D, irrespective of what r is. Thus D must be the uniform distribution on Fq. In Summary: If the property of wos-entauth is going to hold, via the above proof, then we must have that the card ephemeral secret key is chosen uniformly at random from Fq. Thus we see that the choice of card ephemeral secret key not only affects the anonymity properties of the EMV protocol, but also the underlying security of the entire key agreement protocol itself.

4.2 One-Sided Message Authentication and Message Privacy The other parts of the proof in [1] go through with no issues. However, since they all depend on the wos-entauth property, and thus we cannot even guarantee security of the message authentication 14 and privacy in the resulting secure channel unless the card’s emphemeral secret is chosen uniformly at random from Fq. 15 References 1. Christina Brzuska, Nigel P. Smart, Bogdan Warinschi, and Gaven J. Watson. An analysis of the EMV channel establishment protocol. ACM Conference on Computer and Communications Security – ACM CCS 2013, 373–386, 2013. 16