[ 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
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
