Session Date/Time: 05 Nov 2024 13:00

ufmrg

Summary

This meeting of the UFM Research Group focused on two presentations: one on attested TLS and its usability perspective, and another on the formal analysis of Apple's iMessage PQ protocol. The TLS session of the IETF was also mentioned with a process for cryptographic review. There was also some discussion of publishing formal methods results in academic journals and conferences.

Key Discussion Points

TLS Formal Analysis Triage: Discussion of formal cryptographic protocol review process and incentives for researchers to conduct analyses. The TLS session on Friday was mentioned as a place for further discussion. A suggestion was made to notify the UFM list as the process evolves and to forward relevant emails, especially those relating to usability issues, to the UFM group.
Attested TLS: A presentation on the design space for attested TLS, considering pre-handshake, intra-handshake, and post-handshake attestation methods. The motivation for composing attestation efficiently within TLS rather than creating a new secure channel was discussed. Questions and comments centered on the possibility of interleaving attestation and TLS messages, security properties of different composition methods, and potential issues with replay protection. Channel binding properties was also discussed.
iMessage PQ Formal Analysis: A presentation on the formal analysis of Apple's iMessage PQ protocol using the Tamarin Prover, demonstrating the verification of secrecy, forward secrecy, and post-compromise security. This showed that it's possible to analyze looping protocols.
Publishing Analysis Results: The IRTF has its own academic work which publishes its results in the EASPA and consideration should be given to have a special session to publish formal methods results.

Decisions and Action Items

Action Item: Stephen Farrell and Jonathan Hoyland to investigate the AANRW/publication route for publishing formal methods results and report back in the next month or two.

Next Steps

Attend the TLS session on Friday to further discuss the formal cryptographic protocol review process.
Continue discussion on attested TLS design options and properties on the mailing list.