Sciweavers

CONCUR
2005
Springer

Timed Spi-Calculus with Types for Secrecy and Authenticity

13 years 9 months ago
Timed Spi-Calculus with Types for Secrecy and Authenticity
Abstract. We present a discretely timed spi-calculus. A primitive for key compromise allows us to model key compromise attacks, thus going beyond the standard Dolev–Yao attacker model. A primitive for reading a global clock allows us to express protocols based on timestamps, which are common in practice. We 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.
Christian Haack, Alan Jeffrey
Added 26 Jun 2010
Updated 26 Jun 2010
Type Conference
Year 2005
Where CONCUR
Authors Christian Haack, Alan Jeffrey
Comments (0)