article

Strand spaces: proving security protocols correct

Author:

F. Javier Thayer FábregaAuthors Info & Claims

Journal of Computer Security, Volume 7, Issue 2-3

Pages 191 - 230

Published: 01 March 1999 Publication History

Abstract

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 interaction. In this framework, protocol correctness claims may be expressed in terms of the connections between strands of different kinds.

Preparing for a first example, the Needham-Schroeder-Lowe protocol, we prove a lemma that gives a bound on the abilities of the penetrator in any protocol. Our analysis of the example gives a detailed view of the conditions under which it achieves authentication and protects the secrecy of the values exchanged. We also use our proof methods to explain why the original Needham-Schroeder protocol fails.

Before turning to a second example, we introduce ideals as a method to prove additional bounds on the abilities of the penetrator. We can then prove a number of correctness properties of the Otway-Rees protocol, and we clarify its limitations.

We believe that our approach is distinguished from other work by the simplicity of the model, the precision of the results it produces, and the ease of developing intelligible and reliable proofs even without automated support.

Cited By

View all

Sempreboni DViganò L(2023)A mutation-based approach for the formal and automated analysis of security ceremoniesJournal of Computer Security10.3233/JCS-21007531:4(293-364)Online publication date: 1-Jan-2023
https://dl.acm.org/doi/10.3233/JCS-210075
Joy SChandran P(2019)Towards a Secure Development Environment for Collaborative ApplicationsInternational Journal of e-Collaboration10.4018/IJeC.201901010115:1(1-20)Online publication date: 1-Jan-2019
https://dl.acm.org/doi/10.4018/IJeC.2019010101
Yao MZhu YTang L(2019)Research on Formal Analysis Method of Computational Soundness Based on Strand SpaceProceedings of the 2019 4th International Conference on Mathematics and Artificial Intelligence10.1145/3325730.3325750(141-145)Online publication date: 12-Apr-2019
https://dl.acm.org/doi/10.1145/3325730.3325750
Show More Cited By

Index Terms

Strand spaces: proving security protocols correct

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 ...
Mixed Strand Spaces
CSFW '99: Proceedings of the 12th IEEE workshop on Computer Security Foundations

Strand space analysis is a method for stating and proving correctness properties for cryptographic protocols. In this paper we apply the same method to the related problem of mixed protocols, and show that a protocol can remain correct even when used in ...
Analysis of Offline Fair Exchange Protocols in Strand Spaces
CIS '08: Proceedings of the 2008 International Conference on Computational Intelligence and Security - Volume 01

Formal and efficient protocol analysis by pen and paper is highly desired when informal and model-checking methods are not trusted in proving correctness of complicated e-commerce protocols. Based on strand spaces, this paper presents a method for ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Journal of Computer Security

Journal of Computer Security Volume 7, Issue 2-3

Jan. 1999

165 pages

ISSN:0926-227X

Editor:
Sushil Jajodia
George Mason Univ. Fairfax, VA

Issue’s Table of Contents

Publisher

IOS Press

Netherlands

Publication History

Published: 01 March 1999

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

116
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 30 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Sempreboni DViganò L(2023)A mutation-based approach for the formal and automated analysis of security ceremoniesJournal of Computer Security10.3233/JCS-21007531:4(293-364)Online publication date: 1-Jan-2023
https://dl.acm.org/doi/10.3233/JCS-210075
Joy SChandran P(2019)Towards a Secure Development Environment for Collaborative ApplicationsInternational Journal of e-Collaboration10.4018/IJeC.201901010115:1(1-20)Online publication date: 1-Jan-2019
https://dl.acm.org/doi/10.4018/IJeC.2019010101
Yao MZhu YTang L(2019)Research on Formal Analysis Method of Computational Soundness Based on Strand SpaceProceedings of the 2019 4th International Conference on Mathematics and Artificial Intelligence10.1145/3325730.3325750(141-145)Online publication date: 12-Apr-2019
https://dl.acm.org/doi/10.1145/3325730.3325750
Hagihara SShimakawa MYonezaki N(2019)Verification of Verifiability of Voting Protocols by Strand Space AnalysisProceedings of the 2019 8th International Conference on Software and Computer Applications10.1145/3316615.3316629(363-368)Online publication date: 19-Feb-2019
https://dl.acm.org/doi/10.1145/3316615.3316629
Ferrag MMaglaras LArgyriou AKosmanos DJanicke H(2018)Security for 4G and 5G cellular networksJournal of Network and Computer Applications10.1016/j.jnca.2017.10.017101:C(55-82)Online publication date: 1-Jan-2018
https://dl.acm.org/doi/10.1016/j.jnca.2017.10.017
Babel KCheval VKremer S(2017)On Communication Models When Verifying Equivalence PropertiesProceedings of the 6th International Conference on Principles of Security and Trust - Volume 1020410.1007/978-3-662-54455-6_7(141-163)Online publication date: 22-Apr-2017
https://dl.acm.org/doi/10.1007/978-3-662-54455-6_7
Shen JFeng D(2016)Vulnerability Analysis of CSP Based on Stochastic Game TheoryJournal of Control Science and Engineering10.1155/2016/41472512016(3)Online publication date: 1-Oct-2016
https://dl.acm.org/doi/10.1155/2016/4147251
Yang FEscobar SMeadows CMeseguer JSantiago SCheney JVidal G(2016)Strand spaces with choice via a process algebra semanticsProceedings of the 18th International Symposium on Principles and Practice of Declarative Programming10.1145/2967973.2968609(76-89)Online publication date: 5-Sep-2016
https://dl.acm.org/doi/10.1145/2967973.2968609
Honda KYoshida NCarbone M(2016)Multiparty Asynchronous Session TypesJournal of the ACM10.1145/282769563:1(1-67)Online publication date: 3-Mar-2016
https://dl.acm.org/doi/10.1145/2827695
Dolev SKrzywiecki ŁPanwar NSegal M(2016)Optical PUF for Non-Forwardable Vehicle AuthenticationComputer Communications10.1016/j.comcom.2016.05.01693:C(52-67)Online publication date: 1-Nov-2016
https://dl.acm.org/doi/10.1016/j.comcom.2016.05.016
Show More Cited By

Abstract

Cited By

Index Terms

Recommendations

State and Progress in Strand Spaces: Proving Fair Exchange

Mixed Strand Spaces

Analysis of Offline Fair Exchange Protocols in Strand Spaces

Comments

Information

Published In

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations