**Session Date/Time:** 25 Jul 2024 16:30

# ufmrg Meeting Minutes

## Summary
The UFMRG session included presentations on usable formal methods. Topics covered included the application of formal methods in protocol review, a tool for debugging designs using lightweight formal methods (Forge), and formal verification of attested TLS. The session explored the challenges and usability aspects of different formal methods tools and approaches.

## Key Discussion Points

*   **Mark Putty's Presentation:**
    *   Discussion of using formal methods for reviewing IETF specifications.
    *   Explanation of proofs, propositions, and the importance of verification.
    *   Comparison of pen-and-paper proofs, proof assistants, and the Curry-Howard correspondence.
    *   Mark presented how he uses Idris to embed types and proofs directly into IETF drafts.

*   **Ben Greenman's Presentation:**
    *   Introduction to Forge, a tool for debugging designs using lightweight formal methods.
    *   Example of using Forge to model and analyze cross-site request forgery (CSRF).
    *   Discussion of custom visualization, unit testing, and language levels to improve usability.
    *   Forge differs because it provides visualization and unit testing, something most formal methods tools do not.

*   **Samma's Presentation:**
    *   Discussion on applying formal verification to attested TLS.
    *   Exploration of the challenges in using existing formal models and the need for community input.
    *   Presentation on vulnerabilities found in existing implementations related to replay attacks.
    *   There is a practical need for attested TLS, not just theoretical.

*   **Chris Wood's Presentation:**
    *   Discussion about usability of formal methods.
    *   Suggestion to focus on software and have that be the base point for the formal models.
    *   Proposed that proofs should be software.
    *   Talked about Rust and the HACS tool chain

*   **Robert Merget's Presentation:**
    *   The use of Tamarin and ProVerif for security.
    *   Most RFCs are concerned with message formats.
    *   It also permits monitoring which might be a very easy way to double check the specification if it's realistic enough

## Decisions and Action Items

*   **Action Item:** Jonathan Hui talk was cancelled because the session was already over time.

## Next Steps
*   The group will likely discuss potential next steps and future meetings via the mailing list.