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

research-article

Trace equivalence decision: negative tests and non-determinism

Authors:

Vincent Cheval,

Hubert Comon-Lundh,

Stéphanie DelauneAuthors Info & Claims

CCS '11: Proceedings of the 18th ACM conference on Computer and communications security

Pages 321 - 330

https://doi.org/10.1145/2046707.2046744

Published: 17 October 2011 Publication History

Abstract

We consider security properties of cryptographic protocols that can be modeled using the notion of trace equivalence. The notion of equivalence is crucial when specifying privacy-type properties, like anonymity, vote-privacy, and unlinkability.

In this paper, we give a calculus that is close to the applied pi calculus and that allows one to capture most existing protocols that rely on classical cryptographic primitives. First, we propose a symbolic semantics for our calculus relying on constraint systems to represent infinite sets of possible traces, and we reduce the decidability of trace equivalence to deciding a notion of symbolic equivalence between sets of constraint systems. Second, we develop an algorithm allowing us to decide whether two sets of constraint systems are in symbolic equivalence or not. Altogether, this yields the first decidability result of trace equivalence for a general class of processes that may involve else branches and/or private channels (for a bounded number of sessions).

References

[1]

M. Abadi and V. Cortier. Deciding knowledge in security protocols under equational theories. Theoretical Computer Science, 387(1--2):2--32, 2006.

Digital Library

[2]

M. Abadi and C. Fournet. Mobile values, new names, and secure communication. In Proc. 28th Symposium on Principles of Programming Languages (POPL'01), pages 104--115. ACM Press, 2001.

Digital Library

[3]

M. Abadi and C. Fournet. Private authentication. Theoretical Computer Science, 322(3):427--476, 2004.

Digital Library

[4]

M. Abadi and A. Gordon. A calculus for cryptographic protocols: The spi calculus. In Proc. 4th Conference on Computer and Communications Security (CCS'97), pages 36--47. ACM Press, 1997.

Digital Library

[5]

M. Arapinis, T. Chothia, E. Ritter, and M. Ryan. Analysing unlinkability and anonymity using the applied pi calculus. In Proc. of 23rd IEEE Computer Security Foundations Symposium (CSF'10), pages 107--121. IEEE Computer Society Press, 2010.

Digital Library

[6]

A. Armando et al. The AVISPA Tool for the automated validation of internet security protocols and applications. In Proc. 17th Int. Conference on Computer Aided Verification (CAV'05), volume 3576 of LNCS, pages 281--285. Springer, 2005.

Digital Library

[7]

M. Baudet. Deciding security of protocols against off-line guessing attacks. In Proc. 12th Conference on Computer and Communications Security (CCS'05), pages 16--25. ACM Press, 2005.

Digital Library

[8]

M. Baudet. Sécurité des protocoles cryptographiques : aspects logiques et calculatoires. Phd thesis, École Normale Supérieure de Cachan, France, 2007.

[9]

B. Blanchet. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In Proc. 14th Computer Security Foundations Workshop (CSFW'01), pages 82--96. IEEE Comp. Soc. Press, 2001.

Digital Library

[10]

B. Blanchet, M. Abadi, and C. Fournet. Automated verification of selected equivalences for security protocols. Journal of Logic and Algebraic Programming, 75(1):3--51, 2008.

[11]

V. Cheval, H. Comon-Lundh, and S. Delaune. Automating security analysis: symbolic equivalence of constraint systems. In Proc. 5th International Joint Conference on Automated Reasoning (IJCAR'10), volume 6173 of LNAI, pages 412--426. Springer-Verlag, 2010.

Digital Library

[12]

Y. Chevalier and M. Rusinowitch. Decidability of symbolic equivalence of derivations. Journal of Automated Reasoning, 2011. To appear.

Digital Library

[13]

H. Comon-Lundh and S. Delaune. The finite variant property: How to get rid of some algebraic properties. In Proc. 16th International Conference on Rewriting Techniques and Applications (RTA'05), LNCS, pages 294--307. Springer, 2005.

Digital Library

[14]

V. Cortier and S. Delaune. A method for proving observational equivalence. In Proc. 22nd Computer Security Foundations Symposium (CSF'09), pages 266--276. IEEE Comp. Soc. Press, 2009.

Digital Library

[15]

S. Delaune, S. Kremer, and M. D. Ryan. Symbolic bisimulation for the applied pi-calculus. In Proc. 27th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'07), pages 133--145, 2007.

Digital Library

[16]

S. Delaune, S. Kremer, and M. D. Ryan. Verifying privacy-type properties of electronic voting protocols. Journal of Computer Security, 17(4):435--487, July 2009.

[17]

D. Dolev and A. C. Yao. On the security of public key protocols. In Proc. 22nd Symposium on Foundations of Computer Science (FCS'81), pages 350--357. IEEE Computer Society Press, 1981.

Digital Library

[18]

L. Durante, R. Sisto, and A. Valenzano. Automatic testing equivalence verification of spi calculus specifications. ACM Transactions on Software Engineering and Methodology, 12(2):222--284, 2003.

Digital Library

[19]

N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov. Undecidability of bounded security protocols. In Workshop on Formal Methods and Security Protocols, 1999.

[20]

H. Hüttel. Deciding framed bisimulation. In Proc. 4th Int. Workshop on Verification of Infinite State Systems (INFINITY'02), pages 1--20, 2002.

[21]

J. Millen and V. Shmatikov. Constraint solving for bounded-process cryptographic protocol analysis. In Proc. 8th ACM Conference on Computer and Communications Security (CCS'01). ACM Press, 2001.

Digital Library

[22]

S. Mödersheim, L. Viganò, and D. A. Basin. Constraint differentiation: Search-space reduction for the constraint-based analysis of security protocols. Journal of Computer Security, 18(4):575--618, 2010.

Digital Library

[23]

R. Ramanujam and S. Suresh. Tagging makes secrecy decidable for unbounded nonces as well. In Proc. 23rd Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'03), 2003.

[24]

M. Rusinowitch and M. Turuani. Protocol insecurity with finite number of sessions is NP-complete. In Proc. 14th Computer Security Foundations Workshop (CSFW'01), pages 174--190. IEEE Comp. Soc. Press, 2001.

Digital Library

[25]

A. Tiu and J. E. Dawson. Automating open bisimulation checking for the spi calculus. In Proc. 23rd IEEE Computer Security Foundations Symposium (CSF'10), pages 307--321. IEEE Computer Society Press, 2010.

Digital Library

Cited By

Li RWu JHu W(2023)Investigating Trace Equivalences in Information NetworksElectronics10.3390/electronics1204086512:4(865)Online publication date: 8-Feb-2023
https://doi.org/10.3390/electronics12040865
Kazm AKanwal MFakhir MQasim AIshaq A(2022)Automated Verification of Star-Vote in the Applied Pi CalculusVFAST Transactions on Software Engineering10.21015/vtse.v10i4.121810:4(175-180)Online publication date: 31-Dec-2022
https://doi.org/10.21015/vtse.v10i4.1218
Rakotonirina IAmbrona MAguirre ABarthe GSuga YSakurai KDing XSako K(2022)Symbolic Synthesis of Indifferentiability AttacksProceedings of the 2022 ACM on Asia Conference on Computer and Communications Security10.1145/3488932.3497759(667-681)Online publication date: 30-May-2022
https://dl.acm.org/doi/10.1145/3488932.3497759
Show More Cited By

Index Terms

Trace equivalence decision: negative tests and non-determinism
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods

Recommendations

Automated Verification of Equivalence Properties of Cryptographic Protocols

Indistinguishability properties are essential in formal verification of cryptographic protocols. They are needed to model anonymity properties, strong versions of confidentiality, and resistance against offline guessing attacks. Indistinguishability ...
A Method for Proving Observational Equivalence
CSF '09: Proceedings of the 2009 22nd IEEE Computer Security Foundations Symposium

Formal methods have proved their usefulness for analyzing the security of protocols. Most existing results focus on trace properties like secrecy (expressed as a reachability property) or authentication. There are however several security properties, ...
Decidability of Trace Equivalence for Protocols with Nonces
CSF '15: Proceedings of the 2015 IEEE 28th Computer Security Foundations Symposium

Privacy properties such as anonymity, unlink ability, or vote secrecy are typically expressed as equivalence properties. In this paper, we provide the first decidability result for trace equivalence of security protocols, for an unbounded number of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CCS '11: Proceedings of the 18th ACM conference on Computer and communications security

October 2011

742 pages

ISBN:9781450309486

DOI:10.1145/2046707

General Chair:
Yan Chen
Northwestern University, USA
,
Program Chairs:
George Danezis
Microsoft Research Cambridge, UK
,
Vitaly Shmatikov
University of Texas at Austin, USA

Copyright © 2011 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGSAC: ACM Special Interest Group on Security, Audit, and Control

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 17 October 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

CCS'11

Sponsor:

SIGSAC

CCS'11: the ACM Conference on Computer and Communications Security

October 17 - 21, 2011

Illinois, Chicago, USA

Acceptance Rates

CCS '11 Paper Acceptance Rate 60 of 429 submissions, 14%;

Overall Acceptance Rate 1,261 of 6,999 submissions, 18%

Upcoming Conference

CCS '25

Sponsor:
sigsac

ACM SIGSAC Conference on Computer and Communications Security

October 13 - 17, 2025

Taipei , Taiwan

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

43
Total Citations
View Citations
339
Total Downloads

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

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Li RWu JHu W(2023)Investigating Trace Equivalences in Information NetworksElectronics10.3390/electronics1204086512:4(865)Online publication date: 8-Feb-2023
https://doi.org/10.3390/electronics12040865
Kazm AKanwal MFakhir MQasim AIshaq A(2022)Automated Verification of Star-Vote in the Applied Pi CalculusVFAST Transactions on Software Engineering10.21015/vtse.v10i4.121810:4(175-180)Online publication date: 31-Dec-2022
https://doi.org/10.21015/vtse.v10i4.1218
Rakotonirina IAmbrona MAguirre ABarthe GSuga YSakurai KDing XSako K(2022)Symbolic Synthesis of Indifferentiability AttacksProceedings of the 2022 ACM on Asia Conference on Computer and Communications Security10.1145/3488932.3497759(667-681)Online publication date: 30-May-2022
https://dl.acm.org/doi/10.1145/3488932.3497759
Cortier VDallon ADelaune S(2022)A small bound on the number of sessions for security protocols2022 IEEE 35th Computer Security Foundations Symposium (CSF)10.1109/CSF54842.2022.9919670(33-48)Online publication date: Aug-2022
https://doi.org/10.1109/CSF54842.2022.9919670
Babel KCheval VKremer S(2020)On the semantics of communications when verifying equivalence propertiesJournal of Computer Security10.3233/JCS-191366(1-57)Online publication date: 29-Jan-2020
https://doi.org/10.3233/JCS-191366
Cheval VKremer SRakotonirina I(2020)The Hitchhiker’s Guide to Decidability and Complexity of Equivalence Properties in Security ProtocolsLogic, Language, and Security10.1007/978-3-030-62077-6_10(127-145)Online publication date: 28-Oct-2020
https://doi.org/10.1007/978-3-030-62077-6_10
Dreier JHirschi LRadomirović SSasse R(2019)Verification of stateful cryptographic protocols with exclusive ORJournal of Computer Security10.3233/JCS-191358(1-34)Online publication date: 13-Nov-2019
https://doi.org/10.3233/JCS-191358
Hirschi LBaelde DDelaune S(2019)A method for unbounded verification of privacy-type propertiesJournal of Computer Security10.3233/JCS-171070(1-66)Online publication date: 23-Apr-2019
https://doi.org/10.3233/JCS-171070
Chrétien RCortier VDallon ADelaune S(2019)Typing Messages for Free in Security ProtocolsACM Transactions on Computational Logic10.1145/334350721:1(1-52)Online publication date: 12-Sep-2019
https://dl.acm.org/doi/10.1145/3343507
Blanchet BSmyth B(2018)Automated reasoning for equivalences in the applied pi calculus with barriersJournal of Computer Security10.3233/JCS-17101326:3(367-422)Online publication date: 1-Jan-2018
https://dl.acm.org/doi/10.3233/JCS-171013
Show More Cited By

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 Table of Contents