research-article

Symbolically analyzing security protocols using tamarin

Authors:

Ralf SasseAuthors Info & Claims

ACM SIGLOG News, Volume 4, Issue 4

Pages 19 - 30

https://doi.org/10.1145/3157831.3157835

Published: 03 November 2017 Publication History

Abstract

During the last three decades, there has been considerable research devoted to the symbolic analysis of security protocols and existing tools have had considerable success both in detecting attacks on protocols and showing their absence. Nevertheless, there is still a large discrepancy between the symbolic models that one specifies on paper and the models that can be effectively analyzed by tools.

References

[1]

Martín Abadi and Cédric Fournet. 2001. Mobile values, new names, and secure communication. In Proceedings of the 28th Symposium on Principles of Programming Languages (POPL'01). ACM, New York, 104--115.

Digital Library

[2]

Myrto Arapinis, Joshua Phillips, Eike Ritter, and Mark Dermot Ryan. 2014. StatVerif: Verification of stateful processes. Journal of Computer Security 22, 5 (2014), 743--821.

[3]

Myrto Arapinis, Eike Ritter, and Mark Dermot Ryan. 2011. StatVerif: Verification of Stateful Processes. In Proc. CSF. IEEE.

Digital Library

[4]

Michael Backes, Jannik Dreier, Steve Kremer, and Robert Künnemann. 2017. A Novel Approach for Reasoning about Liveness in Cryptographic Protocols and its Application to Fair Exchange. In 2nd IEEE European Symposium on Security and Privacy (EuroS&P'17) (Proceedings of the 2nd IEEE European Symposium on Security and Privacy). Springer, Paris, France. https://hal.inria.fr/hal-01396282

[5]

David Basin, Cas Cremers, Tiffany Hyun-Jin Kim, Adrian Perrig, Ralf Sasse, and Pawel Szalachowski. 2016. Design, Analysis, and Implementation of ARPKI: an Attack Resilient Public-Key Infrastructure. IEEE Transactions on Dependable and Secure Computing PP, Issue: 99 (August 2016).

[6]

David Basin, Cas Cremers, Kinuhiko Miyazaki, Sasa Radomirovic, and Dai Watanabe. 2014. Improving the Security of Cryptographic Protocol Standards. IEEE Security & Privacy (2014), 24--31.

[7]

David Basin, Jannik Dreier, and Ralf Sasse. 2015a. Automated Symbolic Proofs of Observational Equivalence. In 22nd ACM SIGSAC Conference on Computer and Communications Security (ACM CCS 2015). ACM, Denver, United States, 1144--1155.

Digital Library

[8]

David Basin, Jannik Dreier, and Ralf Sasse. 2015b. Automated Symbolic Proofs of Observational Equivalence. Technical Report. https://hal.archives-ouvertes.fr/hal-01337409 https://hal.archives-ouvertes.fr/hal-01337409/file/ccs2015-extended.pdf.

[9]

David A. Basin, Cas J. F. Cremers, Tiffany Hyun-Jin Kim, Adrian Perrig, Ralf Sasse, and Pawel Szalachowski. 2014. ARPKI: Attack Resilient Public-Key Infrastructure. In Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, Scottsdale, AZ, USA, November 3--7, 2014, Gail-Joon Ahn, Moti Yung, and Ninghui Li (Eds.). ACM, 382--393.

Digital Library

[10]

Bruno Blanchet. 2001. An efficient cryptographic protocol verifier based on Prolog rules. In Proc. CSFW. IEEE.

Digital Library

[11]

Bruno Blanchet, Martín Abadi, and Cédric Fournet. 2008. Automated Verification of Selected Equivalences for Security Protocols. Journal of Logic and Algebraic Programming 75, 1 (Feb.-March 2008), 3--51.

Digital Library

[12]

Ran Canetti. 2000. Universally Composable Security: A New Paradigm for Cryptographic Protocols. Cryptology ePrint Archive, Report 2000/067. (2000). http://eprint.iacr.org/2000/067.

[13]

Rohit Chadha, Stefan Ciobâcă, and Steve Kremer. 2012. Automated Verification of Equivalence Properties of Cryptographic Protocols. In ESOP (LNCS), Helmut Seidl (Ed.), Vol. 7211. Springer, 108--127.

Digital Library

[14]

David Chaum. 1982. Blind Signatures for Untraceable Payments. In Advances in Cryptology: Proceedings of CRYPTO '82. Plenum Press, 199--203.

[15]

Vincent Cheval. 2014. APTE: An Algorithm for Proving Trace Equivalence. In TACAS (LNCS), Vol. 8413. Springer, 587--592.

[16]

Vincent Cheval, Véronique Cortier, and Stéphanie Delaune. 2013. Deciding equivalence-based properties using constraint solving. Theor. Comput. Sci. 492 (2013), 1--39.

[17]

Hubert Comon-Lundh and Stephanie Delaune. 2005. The finite variant property: How to get rid of some algebraic properties. Term Rewriting and Applications (2005), 294--307.

Digital Library

[18]

Véronique Cortier, Alicia Filipiak, Jan Florent, Said Gharout, and Jacques Traoré. 2017. Designing and proving an EMV-compliant payment protocol for mobile devices. In 2nd IEEE European Symposium on Security and Privacy (EuroSP'17). 467--480.

[19]

Cas Cremers. 2008. The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols. In Computer Aided Verification (LNCS), Vol. 5123. Springer.

Digital Library

[20]

Cas Cremers, Martin Dehnel-Wild, and Kevin Milner. 2017a. Secure Authentication in the Grid: A Formal Analysis of DNP3: SAv5. In Computer Security - ESORICS 2017 - 22nd European Symposium on Research in Computer Security, Oslo, Norway, September 11--15, 2017, Proceedings (LNCS). Springer.

[21]

Cas Cremers, Marko Horvat, Jonathan Hoyland, Sam Scott, and Thyla van der Merwe. 2017b. A comprehensive symbolic analysis of TLS 1.3. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, Dallas, USA.

Digital Library

[22]

Cas Cremers, Marko Horvat, Sam Scott, and Thyla van der Merwe. 2016. Automated Analysis and Verification of TLS 1.3: 0-RTT, Resumption and Delayed Authentication. In IEEE Symposium on Security and Privacy. IEEE Computer Society, 470--485.

[23]

Stéphanie Delaune, Steve Kremer, Mark Dermot Ryan, and Graham Steel. 2011. Formal Analysis of Protocols Based on TPM State Registers. In Proc. CSF. IEEE, 66--80.

Digital Library

[24]

Jannik Dreier, Charles Duménil, Steve Kremer, and Ralf Sasse. 2017a. Beyond Subterm-Convergent Equational Theories in Automated Verification of Stateful Protocols. In 6th International Conference on Principles of Security and Trust (POST). Uppsala, Sweden. https://hal.inria.fr/hal-01450916

Digital Library

[25]

Jannik Dreier, Maxime Puys, Marie-Laure Potet, Pascal Lafourcade, and Jean-Louis Roch. 2017b. Formally Verifying Flow Integrity Properties in Industrial Systems. In SECRYPT 2017 - 14th International Conference on Security and Cryptography. Madrid, Spain, 12. http://hal.univ-grenoble-alpes.fr/hal-01527913

[26]

Santiago Escobar, Catherine Meadows, and José Meseguer. 2006. A rewriting-based inference system for the NRL Protocol Analyzer and its meta-logical properties. TCS 367 (2006), 162--202.

Digital Library

[27]

Santiago Escobar, Ralf Sasse, and José Meseguer. 2012. Folding variant narrowing and optimal variant termination. J. Log. Algebr. Program. 81, 7--8 (2012), 898--928.

[28]

Atsushi Fujioka, Tatsuaki Okamoto, and Kazuo Ohta. 1992. A practical secret voting scheme for large scale elections. In International Workshop on the Theory and Application of Cryptographic Techniques. Springer.

Digital Library

[29]

Steve Kremer and Robert Künnemann. 2014. Automated Analysis of Security Protocols with Global State. In 2014 IEEE Symposium on Security and Privacy, SP 2014, Berkeley, CA, USA, May 18--21, 2014. 163--178.

Digital Library

[30]

Robert Künnemann and Graham Steel. 2012. YubiSecure? Formal Security Analysis Results for the YubiKey and YubiHSM. In Preliminary Proc. STM'12.

[31]

Ralf Küsters and Tomasz Truderung. 2009. Using ProVerif to Analyze Protocols with Diffie-Hellman Exponentiation. In Computer Security Foundations Symposium (CSF). IEEE, 157--171.

Digital Library

[32]

Ralf Küsters and Tomasz Truderung. 2011. Reducing Protocol Analysis with XOR to the XOR-Free Case in the Horn Theory Based Approach. J. Autom. Reasoning 46, 3--4 (2011), 325--352.

Digital Library

[33]

B.A. LaMacchia, K. Lauter, and A. Mityagin. 2007. Stronger Security of Authenticated Key Exchange. In ProvSec (LNCS), Vol. 4784. Springer, 1--16.

Digital Library

[34]

Simon Meier. 2013. Advancing Automated Security Protocol Verification. Ph.D. Dissertation.

[35]

Sebastian Mödersheim. 2010. Abstraction by set-membership: verifying security protocols and web services with databases. In Proc. CCS. ACM, 351--360.

Digital Library

[36]

Thanh Binh Nguyen and Christoph Sprenger. 2015. Abstractions for Security Protocol Verification. In POST (Lecture Notes in Computer Science), Vol. 9036. Springer, 196--215.

Digital Library

[37]

Tatsuaki Okamoto. 1996. An electronic voting scheme. In IFIP World Conference on IT Tools. 21--30.

[38]

Alisa Pankova and Peeter Laud. 2012. Symbolic Analysis of Cryptographic Protocols Containing Bilinear Pairings. In Proc CSF. IEEE.

Digital Library

[39]

Sonia Santiago, Santiago Escobar, Catherine Meadows, and José Meseguer. 2014. A Formal Definition of Protocol Indistinguishability and Its Verification Using Maude-NPA. In Security and Trust Management (STM) 2014. Springer, 162--177.

[40]

Benedikt Schmidt. 2012. Formal Analysis of Key Exchange Protocols and Physical Protocols. Ph.D. Dissertation.

[41]

Benedikt Schmidt, Simon Meier, Cas Cremers, and David Basin. 2012. Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties. In Proc. CSF. IEEE.

Digital Library

[42]

Benedikt Schmidt, Ralf Sasse, Cas Cremers, and David Basin. 2014. Automated Verification of Group Key Agreement Protocols. In 2014 IEEE Symposium on Security and Privacy, SP 2014, Berkeley, CA, USA, May 18--21, 2014. 179--194.

Digital Library

[43]

The Tamarin team. 2017. The Tamarin prover: source code, documentation, and case studies. (August 2017). Available http://tamarin-prover.github.io/.

Cited By

Kang BBae K(2024)Narrowing and heuristic search for symbolic reachability analysis of concurrent object-oriented systemsScience of Computer Programming10.1016/j.scico.2024.103097235:COnline publication date: 1-Jul-2024
https://dl.acm.org/doi/10.1016/j.scico.2024.103097
Ye KMetere RYadav P(2024)User-Guided Verification of Security Protocols via Sound AnimationSoftware Engineering and Formal Methods10.1007/978-3-031-77382-2_3(33-51)Online publication date: 4-Nov-2024
https://dl.acm.org/doi/10.1007/978-3-031-77382-2_3
Michele MJattke PZibung JRazavi K(2024)PayRide: Secure Transport e-Ticketing with Untrusted Smartphone LocationDetection of Intrusions and Malware, and Vulnerability Assessment10.1007/978-3-031-64171-8_14(261-282)Online publication date: 17-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-64171-8_14
Show More Cited By

Symbolically analyzing security protocols using tamarin
1. Information systems
  1. Data management systems
    1. Data structures
      1. Data layout
2. Security and privacy

Recommendations

Verification Method of Key-Exchange Protocols With a Small Amount of Input Using Tamarin Prover
ASSS '21: Proceedings of the 2021 International Symposium on Advanced Security on Software and Systems

We propose an automatic verification method for cryptographic protocols. Our method can verify whether or not the key-exchange protocol satisfies main security properties, requiring only the protocol specification as its input. The specification ...
Symbolic security analysis using the tamarin prover
FMCAD '17: Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design

In this talk I will present the Tamarin Prover, an analysis tool for symbolic security analysis of systems. A prime example of systems that fall within its scope are security protocols that are executed in the presence of an active attacker. Tamarins ...
Enhanced security models for network protocols.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGLOG News

ACM SIGLOG News Volume 4, Issue 4

October 2017

55 pages

EISSN:2372-3491

DOI:10.1145/3157831

Editor:
Andrzej Murawski
University of Oxford

Issue’s Table of Contents

Copyright © 2017 Authors.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 03 November 2017

Published in SIGLOG Volume 4, Issue 4

Check for updates

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
284
Total Downloads

Downloads (Last 12 months)45
Downloads (Last 6 weeks)10

Reflects downloads up to 06 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Kang BBae K(2024)Narrowing and heuristic search for symbolic reachability analysis of concurrent object-oriented systemsScience of Computer Programming10.1016/j.scico.2024.103097235:COnline publication date: 1-Jul-2024
https://dl.acm.org/doi/10.1016/j.scico.2024.103097
Ye KMetere RYadav P(2024)User-Guided Verification of Security Protocols via Sound AnimationSoftware Engineering and Formal Methods10.1007/978-3-031-77382-2_3(33-51)Online publication date: 4-Nov-2024
https://dl.acm.org/doi/10.1007/978-3-031-77382-2_3
Michele MJattke PZibung JRazavi K(2024)PayRide: Secure Transport e-Ticketing with Untrusted Smartphone LocationDetection of Intrusions and Malware, and Vulnerability Assessment10.1007/978-3-031-64171-8_14(261-282)Online publication date: 17-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-64171-8_14
Basin D(2023)Formal Methods for Payment ProtocolsProceedings of the 2023 ACM Asia Conference on Computer and Communications Security10.1145/3579856.3596440(326-326)Online publication date: 10-Jul-2023
https://dl.acm.org/doi/10.1145/3579856.3596440
Tran DOgata KEscobar SAkleylek SOtmani A(2023)Kyber, Saber, and SK-MLWR Lattice-Based Key Encapsulation Mechanisms Model Checking with MaudeIET Information Security10.1049/2023/93998872023Online publication date: 1-Jan-2023
https://dl.acm.org/doi/10.1049/2023/9399887
Kang BBae KArtho CÖlveczky P(2022)Symbolic Reachability Analysis of Distributed Systems using Narrowing and Heuristic SearchProceedings of the 8th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems10.1145/3563822.3568017(34-44)Online publication date: 29-Nov-2022
https://dl.acm.org/doi/10.1145/3563822.3568017
Hou KLi YYu YChen YZhou HBanerjee SMottola LZhou X(2021)Discovering emergency call pitfalls for cellular networks with formal methodsProceedings of the 19th Annual International Conference on Mobile Systems, Applications, and Services10.1145/3458864.3466625(296-309)Online publication date: 24-Jun-2021
https://dl.acm.org/doi/10.1145/3458864.3466625
Lundberg FFeljan JPöpper CVanhoef MBatina LMayrhofer R(2021)JuliaProceedings of the 14th ACM Conference on Security and Privacy in Wireless and Mobile Networks10.1145/3448300.3468116(90-99)Online publication date: 28-Jun-2021
https://dl.acm.org/doi/10.1145/3448300.3468116
Bojjagani SSastry V(2019)A secure end-to-end proximity NFC-based mobile payment protocolComputer Standards & Interfaces10.1016/j.csi.2019.04.00766:COnline publication date: 1-Oct-2019
https://dl.acm.org/doi/10.1016/j.csi.2019.04.007

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents