<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
font-size:11.0pt;
font-family:"Calibri",sans-serif;
mso-ligatures:standardcontextual;
mso-fareast-language:EN-US;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:#0563C1;
text-decoration:underline;}
span.EmailStyle17
{mso-style-type:personal-compose;
font-family:"Calibri",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
mso-fareast-language:EN-US;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
--></style>
</head>
<body lang="en-CH" link="#0563C1" vlink="#954F72" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal"><span lang="EN-US">Hi all,<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="EN-US">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.
<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="EN-US">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.<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="EN-US">You can find a repository that describes my findings of the formal analysis here:
</span><a href="https://github.com/felixlinker/tamarin_openid4vp_ble">felixlinker/tamarin_openid4vp_ble (github.com)</a><span lang="EN-US"> I tried to stay brief!<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="EN-US">You can find my PR here: </span><a href="https://github.com/openid/openid4vp_ble/pull/46">Formal Analysis Results by felixlinker · Pull Request #46 · openid/openid4vp_ble (github.com)</a><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><span lang="EN-US">Are there any questions? </span><span lang="DE" style="font-family:"Apple Color Emoji"">😊</span><span lang="DE">
</span><span lang="EN-US">Should I join one of the calls to discuss the findings?<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="EN-US">I hope this brings some value to the spec!<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="EN-US">Best,<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-US">Felix<o:p></o:p></span></p>
</div>
</body>
</html>