[Openid-specs-digital-credentials-protocols] Formal Analysis - OpenID for Verifiable Presentations over BLE - draft 00

[Linker Felix]

Hi Tom,

Thanks for your input! But to clarify: The spec doesn’t use TLS.

Are you aware of ongoing development using this standard?

Best,
Felix

From: Tom Jones <thomasclinganjones at gmail.com>
Date: Saturday, 11 November 2023 at 18:04
To: Digital Credentials Protocols List <openid-specs-digital-credentials-protocols at lists.openid.net>
Cc: Linker Felix <flinker at inf.ethz.ch>
Subject: Re: [Openid-specs-digital-credentials-protocols] Formal Analysis - OpenID for Verifiable Presentations over BLE - draft 00

Generally I have been opposed to channel binding using tls as tls is not generally available at the application level. I like the idea here if it can be fully controlled at the application level. We still have the problem of channel establishment but I have a solution for that as well.

This isn't so much a pr as a reboot of the whole project.

The challenge will be integration with phone OS.

I think this is a case where the implementations should drive the standard rather than the other way around.
thx ..Tom (mobile)

On Sat, Nov 11, 2023, 3:48 AM Linker Felix via Openid-specs-digital-credentials-protocols <openid-specs-digital-credentials-protocols at lists.openid.net<mailto:openid-specs-digital-credentials-protocols at lists.openid.net>> wrote:
Hi all,

Earlier this year, I started a formal analysis of the OpenID for Verifiable Presentations over BLE draft 00 and shared my early results in a call. IETF motivated me to finalize my work and I thus finished my formal Tamarin models and opened a pull request to the specification proposing two changes to improve its security properties. Notably, in comparison to my results from earlier this year, I changed my proposed fixes.

Exec. summary: The specification does not sufficiently bind the messages exchanged over the BLE channel to that channel. Thus, an interceptor can both acquire VP tokens not intended for them, and make a verifier believe that a device under the control of an attacker exchanged a VP token with them. I propose to fix this by authenticating the two ephemeral ECDH half-keys used for connection establishment. Details in the PR.

You can find a repository that describes my findings of the formal analysis here: felixlinker/tamarin_openid4vp_ble (github.com)<https://github.com/felixlinker/tamarin_openid4vp_ble> I tried to stay brief!

You can find my PR here: Formal Analysis Results by felixlinker · Pull Request #46 · openid/openid4vp_ble (github.com)<https://github.com/openid/openid4vp_ble/pull/46>

Are there any questions? 😊 Should I join one of the calls to discuss the findings?

I hope this brings some value to the spec!

Best,
Felix
--
Openid-specs-digital-credentials-protocols mailing list
Openid-specs-digital-credentials-protocols at lists.openid.net<mailto:Openid-specs-digital-credentials-protocols at lists.openid.net>
https://lists.openid.net/mailman/listinfo/openid-specs-digital-credentials-protocols
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.openid.net/pipermail/openid-specs-digital-credentials-protocols/attachments/20231112/840f40f1/attachment.html>