[Openid-specs-ab] Early Formal/Security Analysis "OpenID for Verifiable Presentations over BLE"

[Linker Felix]

Hi everyone,

 

I briefly introduced myself 3 weeks ago in the SIOP call already. I am
Felix, a PhD student in the information security group of David Basin at
ETHZ. Pieter Kasselman encouraged me to join the work on the OpenID for
Verifiable Presentations over BLE standard to conduct a formal analysis of
it. It took a while for me to be able to join, but now I am here and have
some early thoughts to discuss.

 

First of all, the standard does neither mention a threat model nor desired
security properties. So for the formal analysis, I just invented my own! But
I would argue that it's worth reflecting both a threat model and desired
security properties in the standard. As for an attacker, I considered an
active network adversary (can read, drop, re-route, replay, send any
message) and assumed that the wallet can obtain an authentic public key of
the verifier. I analyzed the secrecy of the shared verified credential, and
injective agreement between wallet and verifier. Injective agreement here
means that the wallet and verifier agree on recipient of the credential,
shared BLE-layer key, nonce within VC, and the VC itself. Furthermore, there
is an injective mapping from "sharing a VC" to "accepting a VC" events,
i.e., no replay of tokens is possible.

 

During my modeling phase, I specifically wondered about the key material
that should be used. (As an outcome of my head scratching, I assumed that
the wallet can obtain an authentic public key of the verifier in my threat
model.) In particular:

*	The standard mentions that both the wallet and verifier use
ephemeral keys, but it is not specified to what extent these keys should be
ephemeral. When should they be generated? I assumed, that the verifier
generates a fresh key per BLE connection, and the wallet generates its key
freshly when it engages in a new BLE connection.
*	The standard mentions that the authorization request should be
signed (Sec 7.2
<https://openid.bitbucket.io/connect/openid-4-verifiable-presentations-over-
ble-1_0.html#name-payload> ), but not with what key, and also doesn't
specify how the wallet should verify the signature. I presume that the
wallet has obtained an authentic public key of the verifier in advance as
the standard assumes no connectivity. This seems to fit the scope of this
standard well (when I buy a ticket, I can anticipate who will check it).
Nevertheless, this (in my eyes) should be addressed.

 

In my analysis of the secrecy of the token, I found that an active network
attacker can MITM the Bluetooth connection and forward tokens to the
verifier, thus, associating a VC with their Bluetooth session. A
straight-forward defense here would be to include the shared key for the
BLE-layer in the signed authorization request, binding the request to the
BLE channel. Have you considered this?

 

I have many small points on phrasing of the standard, but I think it would
be futile to list them all in this mail (the mail is long enough already).
Should I open an issue for this?

 

It was a lot of fun getting my hands dirty with the standard! I hope I could
provide useful feedback.

 

Thanks, and best,

Felix

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.openid.net/pipermail/openid-specs-ab/attachments/20230712/930a4da9/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5719 bytes
Desc: not available
URL: <http://lists.openid.net/pipermail/openid-specs-ab/attachments/20230712/930a4da9/attachment-0001.p7s>