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. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Haack, C., & Jeffrey, A. (2005). Timed spi-calculus with types for secrecy and authenticity. In Lecture Notes in Computer Science (Vol. 3653, pp. 202–216). Springer Verlag. https://doi.org/10.1007/11539452_18
Mendeley helps you to discover research relevant for your work.