Sewon Park: Designing a Modeling Language for Security Verification of Networked Systems
Abstract: Rabbit is a modeling language that provides familiar imperative-style constructs for writing processes' behaviors and communications. It supports a translation to multiset rewriting rules so that the Tamarin prover, a model-checking software, can verify or refute security properties such as authentication or secrecy automatically in the presence of a configurable Dolev–Yao-style attacker. The goal is to help system engineers describe and verify their networked systems more easily.
In this talk, I introduce Rabbit and the challenges we had during its extension, especially in handling loops. Loops are interesting because without them we cannot describe realistic scenarios, but with them Tamarin can easily run into non-termination. I explain how we added nondeterministic loops, allowing us to express unbounded iterations of client–server transactions, while still keeping their automatic verification tractable by introducing optimization techniques that reduce the number of generated rewriting rules.
This is joint work with Atsushi Igarashi, Yutaka Ishikawa, and Taro Sekiyama. Part of the talk is based on my Formal Methods in Computer-Aided Design (FMCAD) 2025 presentation with Atsushi Igarashi.
Resources:
