Abstract
The Tamarin prover supports the automated, unbounded, symbolic analysis of security protocols. It features expressive languages for specifying protocols, adversary models, and properties, and support for efficient deduction and equational reasoning. We provide an overview of the tool and its applications.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Cremers, C.J.F.: The Scyther Tool: Verification, falsification, and analysis of security protocols. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 414–418. Springer, Heidelberg (2008)
LaMacchia, B., Lauter, K., Mityagin, A.: Stronger security of authenticated key exchange. In: Susilo, W., Liu, J.K., Mu, Y. (eds.) ProvSec 2007. LNCS, vol. 4784, pp. 1–16. Springer, Heidelberg (2007)
Schmidt, B., Meier, S., Cremers, C., Basin, D.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: Proc. CSF. IEEE (2012)
Meier, S.: Advancing Automated Security Protocol Verification. PhD thesis (2013)
Schmidt, B.: Formal Analysis of Key Exchange Protocols and Physical Protocols. PhD thesis (2012)
Comon-Lundh, H., Delaune, S.: The finite variant property: How to get rid of some algebraic properties. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 294–307. Springer, Heidelberg (2005)
Arapinis, M., Ritter, E., Ryan, M.: Statverif: Verification of stateful processes. In: Proc. CSF. IEEE (2011)
Mödersheim, S.: Abstraction by set-membership: verifying security protocols and web services with databases. In: Proc. CCS, pp. 351–360. ACM (2010)
Delaune, S., Kremer, S., Ryan, M.D., Steel, G.: Formal analysis of protocols based on TPM state registers. In: Proc. CSF, pp. 66–80. IEEE (2011)
Künnemann, R., Steel, G.: YubiSecure? Formal security analysis results for the YubiKey and YubiHSM. In: Jøsang, A., Samarati, P., Petrocchi, M. (eds.) STM 2012. LNCS, vol. 7783, pp. 257–272. Springer, Heidelberg (2013)
Escobar, S., Meadows, C., Meseguer, J.: A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties. TCS 367, 162–202 (2006)
Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: Proc. CSFW. IEEE (2001)
Küsters, R., Truderung, T.: Reducing protocol analysis with xor to the xor-free case in the Horn theory based approach. J. Autom. Reasoning 46(3-4), 325–352 (2011)
Pankova, A., Laud, P.: Symbolic analysis of cryptographic protocols containing bilinear pairings. In: Proc. CSF. IEEE (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Meier, S., Schmidt, B., Cremers, C., Basin, D. (2013). The TAMARIN Prover for the Symbolic Analysis of Security Protocols. In: Sharygina, N., Veith, H. (eds) Computer Aided Verification. CAV 2013. Lecture Notes in Computer Science, vol 8044. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39799-8_48
Download citation
DOI: https://doi.org/10.1007/978-3-642-39799-8_48
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39798-1
Online ISBN: 978-3-642-39799-8
eBook Packages: Computer ScienceComputer Science (R0)