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. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Zunino, R., & Degano, P. (2006). Handling exp, X (and Timestamps) in protocol analysis. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3921 LNCS, pp. 413–427). https://doi.org/10.1007/11690634_28
Mendeley helps you to discover research relevant for your work.