Article

Automated Verification of Selected Equivalences for Security Protocols

Authors:

Bruno Blanchet,

Cedric FournetAuthors Info & Claims

LICS '05: Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science

Pages 331 - 340

https://doi.org/10.1109/LICS.2005.8

Published: 26 June 2005 Publication History

Publisher Site

Abstract

In the analysis of security protocols, methods and tools for reasoning about protocol behaviors have been quite effective. We aim to expand the scope of those methods and tools. We focus on proving equivalences P ? Q in which P and Q are two processes that differ only in the choice of some terms. These equivalences arise often in applications. We show how to treat them as predicates on the behaviors of a process that represents P and Q at the same time. We develop our techniques in the context of the applied pi calculus and implement them in the tool ProVerif.

Cited By

View all

Bauereiβ TPesenti Gritti APopescu ARaimondi F(2018)CoSMedJournal of Automated Reasoning10.1007/s10817-017-9443-361:1-4(113-139)Online publication date: 1-Jun-2018
https://dl.acm.org/doi/10.1007/s10817-017-9443-3
Chadha RSistla AViswanathan MAceto LIngólfsdóttir A(2017)Verification of randomized security protocolsProceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3329995.3330061(1-12)Online publication date: 20-Jun-2017
https://dl.acm.org/doi/10.5555/3329995.3330061
Basin DCremers CDreier JSasse R(2017)Symbolically analyzing security protocols using tamarinACM SIGLOG News10.1145/3157831.31578354:4(19-30)Online publication date: 3-Nov-2017
https://dl.acm.org/doi/10.1145/3157831.3157835
Show More Cited By

Index Terms

Automated Verification of Selected Equivalences for Security Protocols
1. Mathematics of computing
  1. Continuous mathematics
    1. Calculus
      1. Lambda calculus
  2. Mathematical analysis
    1. Calculus
      1. Lambda calculus
2. Theory of computation
  1. Logic
    1. Logic and verification
  2. Semantics and reasoning
    1. Program semantics
      1. Operational semantics

Recommendations

Verification of security protocols with lists: From length one to unbounded length
Security and Trust Principles

We present a novel, simple technique for proving secrecy properties for security protocols that manipulate lists of unbounded length, for an unbounded number of sessions. More specifically, our technique relies on the Horn clause approach used in the ...
Automatic verification of correspondences for security protocols

We present a new technique for verifying correspondences in security protocols. In particular, correspondences can be used to formalize authentication. Our technique is fully automatic, it can handle an unbounded number of sessions of the protocol, and ...
Security protocols: from linear to classical logic by abstract interpretation

We relate two models of security protocols, namely the linear logic or multiset rewriting model, and the classical logic, Horn clause representation of protocols. More specifically, we show that the latter model is an abstraction of the former, in which ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

LICS '05: Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science

June 2005

459 pages

ISBN:0769522661

Publisher

IEEE Computer Society

United States

Publication History

Published: 26 June 2005

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

35
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Bauereiβ TPesenti Gritti APopescu ARaimondi F(2018)CoSMedJournal of Automated Reasoning10.1007/s10817-017-9443-361:1-4(113-139)Online publication date: 1-Jun-2018
https://dl.acm.org/doi/10.1007/s10817-017-9443-3
Chadha RSistla AViswanathan MAceto LIngólfsdóttir A(2017)Verification of randomized security protocolsProceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3329995.3330061(1-12)Online publication date: 20-Jun-2017
https://dl.acm.org/doi/10.5555/3329995.3330061
Basin DCremers CDreier JSasse R(2017)Symbolically analyzing security protocols using tamarinACM SIGLOG News10.1145/3157831.31578354:4(19-30)Online publication date: 3-Nov-2017
https://dl.acm.org/doi/10.1145/3157831.3157835
Kim JHolz RHu WJha S(2017)Automated Analysis of Secure Internet of Things ProtocolsProceedings of the 33rd Annual Computer Security Applications Conference10.1145/3134600.3134624(238-249)Online publication date: 4-Dec-2017
https://dl.acm.org/doi/10.1145/3134600.3134624
Chadha RCheval VCiobâcă ŞKremer S(2016)Automated Verification of Equivalence Properties of Cryptographic ProtocolsACM Transactions on Computational Logic10.1145/292671517:4(1-32)Online publication date: 20-Sep-2016
https://dl.acm.org/doi/10.1145/2926715
Chrétien RCortier VDelaune S(2015)From Security Protocols to Pushdown AutomataACM Transactions on Computational Logic10.1145/281126217:1(1-45)Online publication date: 23-Sep-2015
https://dl.acm.org/doi/10.1145/2811262
van den Broek FVerdult Rde Ruiter JRay ILi NKruegel C(2015)Defeating IMSI CatchersProceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security10.1145/2810103.2813615(340-351)Online publication date: 12-Oct-2015
https://dl.acm.org/doi/10.1145/2810103.2813615
Cortier V(2015)Formal verification of e-votingACM SIGLOG News10.1145/2728816.27288232:1(25-34)Online publication date: 28-Jan-2015
https://dl.acm.org/doi/10.1145/2728816.2728823
Cheval VCortier V(2015)Timing Attacks in Security ProtocolsProceedings of the 4th International Conference on Principles of Security and Trust - Volume 903610.1007/978-3-662-46666-7_15(280-299)Online publication date: 11-Apr-2015
https://dl.acm.org/doi/10.1007/978-3-662-46666-7_15
Cortier VKremer S(2014)Formal Models and Techniques for Analyzing Security ProtocolsFoundations and Trends in Programming Languages10.1561/25000000011:3(151-267)Online publication date: 13-Nov-2014
https://dl.acm.org/doi/10.1561/2500000001
Show More Cited By

Abstract

Cited By

Index Terms

Recommendations

Verification of security protocols with lists: From length one to unbounded length

Automatic verification of correspondences for security protocols

Security protocols: from linear to classical logic by abstract interpretation

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