Session Date/Time: 05 Nov 2023 11:00

UFMRG Formal Methods Training

Summary

This session provided an introduction to formal methods using the Tamarin prover. The session covered the basic syntax of Tamarin models, lemmas, and how to interpret Tamarin's output. Participants worked through several exercises, including modeling a simplified TCP handshake and a portion of the OAuth 2.0 authorization code flow. The session emphasized the importance of explicitly stating assumptions when using formal methods and how to use Tamarin to identify potential security vulnerabilities.

Key Discussion Points

Tamarin Model Structure: Rules consist of preconditions (state read, message in) and effects (state write, message out).
Tamarin Values: Constants (strings), unguessable fresh values (tilde), public values (dollar), and function applications.
Equation Theories: How Tamarin models cryptographic primitives like signatures using equations. Functions are opaque unless equations define their behavior.
Facts vs. Functions: Facts are labels for state, while functions represent values.
Interpreting Tamarin Output: Understanding the components of Tamarin traces: boxes (rule applications), bubbles (adversary actions), and arrows (dependencies).
Using Tamarin in Practice: The value of formal methods comes from explicitly stating assumptions. A four-step approach: initial spec, positive security properties, make model realistic, refine properties with explicit assumptions.
Counterexample Analysis: How to use Tamarin's counterexamples to identify deviations from expected protocol behavior and refine the model or properties.
Scope of Analysis: Whether to analyze the entire protocol or focus on subparts, depending on the goal and complexity.

Decisions and Action Items

Participants should continue working on the exercises (Exercises 1-3) at their own pace.
Refer to the Tamarin documentation (Tamarin book) and the provided syntax cheat sheet for additional information.

Next Steps

The instructors will be available to answer questions and provide assistance.
Advanced topics, such as manual proofs and custom proof heuristics, can be explored using the Tamarin documentation.
The H2 reset vulnerability case study will be discussed at the UFR MRG meeting on Wednesday afternoon.