Timed Spi-Calculus With Types for Secrecy and Authenticity

Overview

This paper presents a discretely timed spi-calculus. A primitive for key compromise allows to model key compromise attacks, thus going beyond the standard Dolev-Yao attacker model. A primitive for reading a global clock allows the authors to express protocols based on timestamps, which are common in practice. The authors accompany the timed spi-calculus with a type system, prove that well-typed protocols are robustly safe for secrecy and authenticity and present examples of well-typed protocols as well as an example where failure to typecheck reveals a (well-known) flaw.