[TLS] Re: Formal analysis of draft-ietf-tls-pake

[Muhammad Usama Sardar <[e-mail]>]

[ Just in case the following email was missed. ]

To avoid redundant effort, it will be good to see the current state of 
formalization, and to know which areas to focus on.

For this draft, I plan to use ProVerif and reuse many of the functions 
from my formal analysis [1] for draft-fossati-tls-attestation, which 
substantiates the attacks mentioned in [2].

Are the design options presented in the meeting explained somewhere? 
Unless I am missing something, I don't see them in the draft/repo.

Side motivation: Paul Wouters (as individual) mentioned this draft in 
his on-mic comment in the SEAT WG meeting [3], and I am trying to 
understand what exactly that means from a formal analysis perspective.

-Usama

On 16.11.25 10:20, Muhammad Usama Sardar wrote:
> If I understood correctly in the meeting, the authors have some 
> ongoing formal analysis but I could not find anything in the repo [0]. 
> Could you please point me to the repo where the formal analysis is 
> being done?
>
> From the formal analysis perspective, is there something specific 
> other than the open issue mentioned in section 8.4 that you need help 
> with?
>
> -Usama
>
> [0] https://github.com/tlswg/tls-pake
[1] https://github.com/CCC-Attestation/formal-spec-id-crisis

[2] https://mailarchive.ietf.org/arch/msg/tls/Jx_yPoYWMIKaqXmPsytKZBDq23o/

[3] 
https://datatracker.ietf.org/doc/minutes-124-seat-202511041630/#discussion-2