×

Handling exp, \(\times\) (and timestamps) in protocol analysis. (English) Zbl 1180.94066

Aceto, Luca (ed.) et al., Foundations of software science and computation structures. 9th international conference, FOSSACS 2006, held as part of the joint European conferences on theory and practice of software, ETAPS 2006, Vienna, Austria, March 25–31, 2006. Proceedings. Berlin: Springer (ISBN 3-540-33045-3/pbk). Lecture Notes in Computer Science 3921, 413-427 (2006).
Summary: We present a static analysis technique for the verification of cryptographic protocols, specified in a process calculus. Rather than assuming a specific, fixed set of cryptographic primitives, we only require them to be specified through a term rewriting system, with no restrictions. Examples are provided to support our analysis. First, we tackle forward secrecy for a Diffie-Hellman-based protocol involving exponentiation, multiplication and inversion. Then, a simplified version of Kerberos is analyzed, showing that its use of timestamps succeeds in preventing replay attacks.
For the entire collection see [Zbl 1103.68001].

MSC:

94A60 Cryptography
68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Software:

Timbuk
PDFBibTeX XMLCite
Full Text: DOI