More Web Proxy on the site http://driver.im/

research-article

Public Access

Strand spaces with choice via a process algebra semantics

Authors:

Santiago Escobar,

Catherine Meadows,

José Meseguer,

Sonia SantiagoAuthors Info & Claims

PPDP '16: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming

Pages 76 - 89

https://doi.org/10.1145/2967973.2968609

Published: 05 September 2016 Publication History

Abstract

Roles in cryptographic protocols do not always have a linear execution, but may include choice points causing the protocol to continue along different paths. In this paper we address the problem of representing choice in the strand space model of cryptographic protocols, particularly as it is used in the Maude-NPA cryptographic protocol analysis tool.

To achieve this goal, we develop and give formal semantics to a process algebra for cryptographic protocols that supports a rich taxonomy of choice primitives for composing strand spaces. In our taxonomy, deterministic and non-deterministic choices are broken down further. Non-deterministic choice can be either explicit, i.e., one of two paths is chosen, or implicit, i.e. the value of a variable is chosen non-deterministically. Likewise, deterministic choice can be either an (explicit) if-then-else choice, i.e. one path is chosen if a predicate is satisfied, while the other is chosen if it is not, or implicit deterministic choice, i.e. execution continues only if a certain pattern is matched. We have identified a class of choices which includes finite branching and some cases of infinite branching, which we address in this paper.

Our main theoretical results are two bisimulation results: one proving that the formal semantics of our process algebra is bisimilar to the forwards execution semantics of its associated strands, and another showing that it is also bisimilar with respect to the symbolic backwards semantics of the strands such as that supported by Maude-NPA. At the practical level, we present a prototype implementation of our process algebra in Maude-NPA, illustrate its expressive power and naturalness with various examples, and show how it can be effectively used in formal analysis.

References

[1]

Martín Abadi. Leslie lamport's properties and actions. In Proceedings of the Twentieth Annual ACM Symposium on Principles of Distributed Computing, PODC 2001, page 15, 2001.

Digital Library

[2]

Martín Abadi and Cédric Fournet. Mobile values, new names, and secure communication. In Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 104--115, 2001.

Digital Library

[3]

Iliano Cervesato, Nancy A. Durgin, John C. Mitchell, Patrick Lincoln, and Andre Scedrov. Relating strands and multiset rewriting for security protocol analysis. In Proceedings of the 13th IEEE Computer Security Foundations Workshop, CSFW '00, pages 35--51, 2000.

Digital Library

[4]

Federico Crazzolara and Glynn Winskel. Composing strand spaces. In FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science, pages 97--108, 2002.

Digital Library

[5]

Cas Cremers, Marko Horval, Sam Scott, and Thyla van der Merwe. Automated analysis and verification of TLS 1.3:0-RTT, resumption and delayed authentication. In IEEE Security and Privacy, 2016, to appear: 2016.

[6]

Santiago Escobar, Catherine Meadows, and José Meseguer. Maude-NPA: Cryptographic protocol analysis modulo equational properties. In Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures, LNCS vol. 5705, pages 1--50. Springer, 2009.

Digital Library

[7]

Santiago Escobar, Catherine Meadows, José Meseguer, and Sonia Santiago. A rewriting-based forwards semantics for Maude-NPA. In Proceedings of the 2014 Symposium and Bootcamp on the Science of Security, HotSoS 2014. ACM, 2014.

Digital Library

[8]

Santiago Escobar, Catherine Meadows, José Meseguer, and Sonia Santiago. Symbolic protocol analysis with disequality constraints modulo equational theories. In Programming Languages with Applications to Biology and Security, pages 238--261, 2015.

[9]

F. J. Thayer Fabrega, J. Herzog, and J. Guttman. Strand Spaces: What Makes a Security Protocol Correct? Journal of Computer Security, 7:191--230, 1999.

Digital Library

[10]

Sibylle B. Fröschle. Adding branching to the strand space model. Electr. Notes Theor. Comput. Sci., 242(1):139--159, 2009.

Digital Library

[11]

Jean Goubault-Larrecq, Catuscia Palamidessi, and Angelo Troina. A probabilistic applied pi-calculus. In Programming Languages and Systems, 5th Asian Symposium, APLAS 2007, pages 175--190, 2007.

Digital Library

[12]

Simon Meier, Benedikt Schmidt, Cas Cremers, and David A. Basin. The TAMARIN prover for the symbolic analysis of security protocols. In Computer Aided Verification - 25th International Conference, CAV 2013, pages 696--701, 2013.

[13]

José Meseguer. Conditional rewriting logic as a united model of concurrency. Theor. Comput. Sci., 96(1):73--155, 1992.

Digital Library

[14]

Robin Milner. Communicating and mobile systems - the Pi-calculus. Cambridge University Press, 1999.

Digital Library

[15]

Carlos Olarte and Frank D. Valencia. The expressivity of universal timed CCP: undecidability of monadic FLTL and closure operators for security. In Proceedings Principles and Practice of Declarative Programming 2008, pages 8--19, 2008.

Digital Library

[16]

Eric Rescorla. The transport layer security (tls) protocol version 1.3. Technical Report draft-ietf-tls-tls13-12, IETF, 2016.

Cited By

Li YJiang HZhao Y(2024)A Formally Verified Scheme for Security Protocols with the Operational Semantics of Strand SpaceTheoretical Aspects of Software Engineering10.1007/978-3-031-64626-3_18(306-323)Online publication date: 29-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-64626-3_18
Piramuthu OCaesar MHong JBures MPark JCerny T(2022)UAV-VANET authentication for real-time highway surveillanceProceedings of the 37th ACM/SIGAPP Symposium on Applied Computing10.1145/3477314.3507021(1925-1931)Online publication date: 25-Apr-2022
https://dl.acm.org/doi/10.1145/3477314.3507021
Aparicio-Sánchez DEscobar SMeadows CMeseguer JSapiña J(2021)Protocol Analysis with Time and SpaceProtocols, Strands, and Logic10.1007/978-3-030-91631-2_2(22-49)Online publication date: 19-Nov-2021
https://doi.org/10.1007/978-3-030-91631-2_2
Show More Cited By

Strand spaces with choice via a process algebra semantics
1. Theory of computation
  1. Semantics and reasoning

Recommendations

State and Progress in Strand Spaces: Proving Fair Exchange

Many cryptographic protocols are intended to coordinate state changes among principals. Exchange protocols, for instance, coordinate delivery of new values to the participants, i.e. additions to the set of values they possess. An exchange protocol is ...
Strand spaces: proving security protocols correct

A strand is a sequence of events; it represents either an execution by a legitimate party in a security protocol or else a sequence of actions by a penetrator. A strand space is a collection of strands, equipped with a graph structure generated by causal ...
Process Algebra Having Inherent Choice: Revised Semantics for Concurrent Systems

Process algebras are standard formalisms for compositionally describing systems by the dependencies of their observable synchronous communication. In concurrent systems, parallel composition introduces resolvable nondeterminism, i.e., nondeterminism ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

PPDP '16: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming

September 2016

249 pages

ISBN:9781450341486

DOI:10.1145/2967973

Conference Chair:
James Cheney
University of Edinburgh, UK
,
Program Chair:
Germán Vidal
Universitat Politècnica de València, Spain

Copyright © 2016 ACM.

© 2016 Association for Computing Machinery. ACM acknowledges that this contribution was authored or co-authored by an employee, contractor or affiliate of the United States government. As such, the United States Government retains a nonexclusive, royalty-free right to publish or reproduce this article, or to allow others to do so, for Government purposes only.

In-Cooperation

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 September 2016

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

PPDP '16

PPDP '16: 18th International Symposium on Principles and Practice of Declarative Programming

September 5 - 7, 2016

Edinburgh, United Kingdom

Acceptance Rates

PPDP '16 Paper Acceptance Rate 17 of 37 submissions, 46%;

Overall Acceptance Rate 230 of 486 submissions, 47%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
346
Total Downloads

Downloads (Last 12 months)133
Downloads (Last 6 weeks)15

Reflects downloads up to 30 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Li YJiang HZhao Y(2024)A Formally Verified Scheme for Security Protocols with the Operational Semantics of Strand SpaceTheoretical Aspects of Software Engineering10.1007/978-3-031-64626-3_18(306-323)Online publication date: 29-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-64626-3_18
Piramuthu OCaesar MHong JBures MPark JCerny T(2022)UAV-VANET authentication for real-time highway surveillanceProceedings of the 37th ACM/SIGAPP Symposium on Applied Computing10.1145/3477314.3507021(1925-1931)Online publication date: 25-Apr-2022
https://dl.acm.org/doi/10.1145/3477314.3507021
Aparicio-Sánchez DEscobar SMeadows CMeseguer JSapiña J(2021)Protocol Analysis with Time and SpaceProtocols, Strands, and Logic10.1007/978-3-030-91631-2_2(22-49)Online publication date: 19-Nov-2021
https://doi.org/10.1007/978-3-030-91631-2_2
Focardi RLuccio F(2021)Secure Key Management Policies in Strand SpacesProtocols, Strands, and Logic10.1007/978-3-030-91631-2_10(175-197)Online publication date: 19-Nov-2021
https://doi.org/10.1007/978-3-030-91631-2_10
Aparicio-Sánchez DEscobar SMeadows CMeseguer JSapiña J(2020)Protocol Analysis with TimeProgress in Cryptology – INDOCRYPT 202010.1007/978-3-030-65277-7_7(128-150)Online publication date: 8-Dec-2020
https://doi.org/10.1007/978-3-030-65277-7_7
Escobar SMeseguer J(2019)Canonical Narrowing with Irreducibility Constraints as a Symbolic Protocol Analysis MethodFoundations of Security, Protocols, and Equational Reasoning10.1007/978-3-030-19052-1_4(15-38)Online publication date: 28-Apr-2019
https://doi.org/10.1007/978-3-030-19052-1_4
Meseguer J(2018)Symbolic Reasoning Methods in Rewriting Logic and MaudeLogic, Language, Information, and Computation10.1007/978-3-662-57669-4_2(25-60)Online publication date: 27-Jun-2018
https://doi.org/10.1007/978-3-662-57669-4_2
Gazeau IKremer S(2017)Automated Analysis of Equivalence Properties for Security Protocols Using Else BranchesComputer Security – ESORICS 201710.1007/978-3-319-66399-9_1(1-20)Online publication date: 12-Aug-2017
https://doi.org/10.1007/978-3-319-66399-9_1

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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

Media

Figures

Other

Tables

View Table of Contents