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

[Linker Felix]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.openid.net/pipermail/openid-specs-digital-credentials-protocols/attachments/20231111/035d8a39/attachment.html>