Posted by: jonkatz | January 14, 2014

Real-World Crypto, Day 2, Session 1

The workshop kicked off with two talks on OPACITY. OPACITY is a protocol suite with two protocols: ZKM and FS. Both of these are Diffie-Hellman-based authenticated key-agreement protocols, geared toward smartcards, that incorporate some privacy measures. It was developed by the company ActiveIdentity, is apparently supported by the US Department of Defense, and has been standardized.

Marc Fischlin began with a talk about a cryptographic analysis of OPACITY. Marc pointed out that the fact that the protocol is standards-compliant does not imply anything about whether or not it is secure; following a standard is no substitute for a rigorous analysis/proof. (This is clearly true, since the standards don’t contain or imply any particular security definition.)

Both protocols use two rounds, and assume the smartcard holds a long-term, certified public key. The ZKM protocol is a static-ephemeral Diffie-Hellman protocol, where the card reader generates an ephemeral key and the smartcard uses its long-term (“static”) Diffie-Hellman public key to derive a shared key. Interestingly (or surprisingly), there is no authentication from reader to client, and anyone can easily impersonate a reader. The FS protocol is similar, though in this case both the smartcard and the reader have long-term, certified public keys. Here, two ephemeral-static Diffie-Hellman protocols are run to derive shared values, and these are then used in a “cascading” fashion to derive shared keys.

One complicated part of both protocols is that, for efficiency reasons, they allow what is called “persistent binding”: the card reader can cache the public key of a smartcard it has interacted with before. There is also a way for the smartcard to “blind” the certificate it sends, which is supposed to provide some measure of privacy for the smartcard.

In trying to analyze the protocol, Marc found that the security goals were unclear. (This is a general problem when security goals are stated informally, and demonstrates why formal models/definitions are useful even in the absence of a security proof.) Marc and his co-authors used a well-known security definition for authenticated key agreement by Bellare and Rogaway, adapted to capture one-way auhtentication (which is all we can hope for ZKS to provide). Marc was able to prove that ZKM achieves one-way authentication, and that the derived, shared keys are hidden from a passive attacker. FS also satisfies some notion of identity hiding for the card. In both cases, the analysis break down if persistent binding is used (it ws not clear to me whether there is a concrete attack in that case).

The second talk in the session was by Eric Le Saint, who introduced the OPACITY protocol. He noted that OPACITY was designed for protecting contactless transactions between chip-based mobile devices and terminals, where currently no security mechanisms are in place. For this reason, the protocol was designed to be fast: the reader/terminal can pre-process things so that it is ready to sent the first message of the protocol as soon as a card comes into close proximity; the card can then quickly compute and send the second (and final) protocol message. This can all be done in the time it takes to physically swipe a card at a reader, without inconveniencing the user holding the card.

Eric addressed a statement from Marc’s papers to the effect that the security guarantees of OPACITY are rather weak. In response he noted that one-way authentication may be sufficient for the intended applications, and resistance to eavesdropping may also be enough in practice. (Frankly, the justification for this did not make sense to me, but perhaps it was just poor presentation.) He also claims (without any explanation) that the notion of identity hiding achieved by ZKM is considered strong enough for US government applications.

He concluded by stating that he was currently working on an improved version of OPACITY that would achieve stronger security goals. He described the protocol using a high-level block diagram but I was unable to follow the details. I hope he (or someone else) will be attempting the prove security this time around.

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

Categories

%d bloggers like this: