Article

Security analysis of network protocols: logical and computational methods

Author:

John C. MitchellAuthors Info & Claims

PPDP '05: Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming

Pages 151 - 152

https://doi.org/10.1145/1069774.1069788

Published: 11 July 2005 Publication History

Abstract

Security analysis of network protocols is a rich scientific area with two different foundations, one based on logic and symbolic computation, and one based on computational complexity theory. The symbolic approach has led to formal logics and automated tools that have been used successfully in a number of case studies. The computational approach yields more insight into the strength and vulnerabilities of protocols, but it involves explicit reasoning about probability and computational complexity. Ideally, we would like to combine the advantages of both and develop a simple, automatable method that captures intuitive high-level reasoning principles, yet accurately reflects the subtleties of probabilistic polynomial-time computation. This talk will summarize some of the main lines of prior work and discuss ways to bridge the gap between symbolic and computational analysis. A significant portion of the talk will focus on a high-level protocol logic whose provable statements are correct when regarded as assertions about probabilistic polynomial-time protocol execution in the face of probabilistic polynomial-time attack.

References

[1]

M. Abadi and P. Rogaway. Reconciling two views of cryptography (the computational soundness of formal encryption). Journal of Cryptology, 15(2):103--127, 2002.

Digital Library

[2]

P. Adão, G. Bana, and A. Scedrov. Computational and information-theoretic soundness and completeness of formal encryption. In Proceedings of 18th IEEE Computer Security Foundations Workshop. IEEE, 2005. To appear.

Digital Library

[3]

M. Backes, A. Datta, A. Derek, J. C. Mitchell, and M. Turuani. Compositional analysis of contract signing protocols. In Proceedings of 18th IEEE Computer Security Foundations Workshop. IEEE, 2005. To appear.

Digital Library

[4]

M. Backes, B. Pfitzmann, and M. Waidner. A universally composable cryptographic library. Cryptology ePrint Archive, Report 2003/015, 2003.

[5]

I. Cervesato, N. A. Durgin, P. D. Lincoln, J. C. Mitchell, and A. Scedrov. A meta-notation for protocol analysis. In P. Syverson, editor, Proceedings of the 12th IEEE Computer Security Foundations Workshop --- CSFW'99, pages 55--69, Mordano, Italy, June 1999. IEEE Computer Society Press.

Digital Library

[6]

R. Chadha, J. C. Mitchell, A. Scedrov, and V. Shmatikov. Contract signing, optimism, and advantage. In 14th International Conference on Concurrency Theory (CONCUR '03), volume 2761 of Lecture Notes in Computer Science. Springer-Verlag, 2003.

[7]

V. Cortier and B. Warinschi. Computationally sound, automated proofs for security protocols. In Proceedings of 14th European Symposium on Programming (ESOP'05), Lecture Notes in Computer Science, pages 157--171. Springer-Verlag, 2005.

Digital Library

[8]

A. Datta, A. Derek, J. Mitchell, V. Shmatikov, and M. Turuani. Probabilistic polynomial-time semantics for a protocol security logic. In 32nd International Colloquium on Automata, Languages and Programming (ICALP '05), Lecture Notes in Computer Science. Springer-Verlag, 2005.

Digital Library

[9]

A. Datta, A. Derek, J. C. Mitchell, and D. Pavlovic. A derivation system for security protocols and its logical formalization. In Proceedings of 16th IEEE Computer Security Foundations Workshop, pages 109--125. IEEE, 2003.

[10]

A. Datta, A. Derek, J. C. Mitchell, and D. Pavlovic. Abstraction and refinement in protocol derivation. In Proceedings of 17th IEEE Computer Security Foundations Workshop, pages 30--45. IEEE, 2004.

Digital Library

[11]

A. Datta, A. Derek, J. C. Mitchell, and D. Pavlovic. A derivation system and compositional logic for security protocols. Journal of Computer Security, 2005. To appear.

Digital Library

[12]

A. Datta, R. Küsters, J. C. Mitchell, A. Ramanathan, and V. Shmatikov. Unifying equivalence-based definitions of protocol security. In ACM SIGPLAN and IFIP WG 1.7, 4th Workshop on Issues in the Theory of Security, April 2004.

[13]

N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov. Undecidability of bounded security protocols. Journal of Computer Security, 12(2):247, 2004.

Digital Library

[14]

N. Durgin, J. C. Mitchell, and D. Pavlovic. A compositional logic for proving security properties of protocols. Journal of Computer Security, 11:677--721, 2003.

Digital Library

[15]

C. He and J. Mitchell. Analysis of the 802.11i 4-way handshake. In ACM Workshop on Wireless Security (WiSe 2004). Philadelphia, October, 2004.

Digital Library

[16]

C. He and J. Mitchell. Security analysis and improvements for ieee 802.11i. In 11th Annual Network and Distributed System Security Symposium (NDSS '05). San Diego, February, 2005.

[17]

J. Herzog. The Diffie-Hellman key-agreement scheme in the strand-space model. In Proceedings of 16th IEEE Computer Security Foundations Workshop, pages 234--247, 2003.

[18]

J. Herzog. Computational Soundness for Standard Assumptions of Formal Cryptography. PhD thesis, MIT, 2004.

Digital Library

[19]

R. Impagliazzo and B. M. Kapron. Logics for reasoning about cryptographic constructions. In Proceedings of the 44th Annual IEEE Symposium on Foundations of Computer Science (FOCS '03), pages 372--383. IEEE, 2003.

Digital Library

[20]

D. Micciancio and B. Warinschi. Soundness of formal encryption in the presence of active adversaries. In Theory of Cryptography Conference - Proceedings of TCC 2004, volume 2951 of Lecture Notes in Computer Science, pages 133--151. Springer-Verlag, 2004.

[21]

J. Mitchell, V. Shmatikov, and U. Stern. Finite-state analysis of ssl 3.0. In Seventh USENIX Security Symposium, pages 201--216, 1998.

Digital Library

[22]

J. C. Mitchell, M. Mitchell, and U. Stern. Automated analysis of cryptographic protocols using Murφ. In Proc. IEEE Symposium on Research in Security and Privacy, pages 141--151. IEEE Computer Society Press, 1997.

Digital Library

[23]

A. Ramanathan, J. C. Mitchell, A. Scedrov, and V. Teague. Probabilistic bisimulation and equivalence for security analysis of network protocols. In FOSSACS 2004 - Foundations of Software Science and Computation Structures, March 2004. Summarizes results in {?}.

[24]

V. Shmatikov and J. C. Mitchell. Finite-state analysis of two contract signing protocols. Theoretical Computer Science, 283(2):419--450, 2002.

Digital Library

[25]

B. Warinschi. A computational analysis of the Needham-Schroeder(-Lowe) protocol. In Proceedings of 16th Computer Science Foundation Workshop, pages 248--262. ACM Press, 2003.

Cited By

Hu YPang LPei QWang X(2015)Instruction Clustering Analysis for Network Protocol's Abnormal BehaviorProceedings of the 2015 10th International Conference on P2P, Parallel, Grid, Cloud and Internet Computing (3PGCIC)10.1109/3PGCIC.2015.69(791-794)Online publication date: 4-Nov-2015
https://dl.acm.org/doi/10.1109/3PGCIC.2015.69
Gu QJones KZang WYu MLiu P(2012)Revealing Abuses of Channel Assignment Protocols in Multi-channel Wireless Networks: An Investigation Logic ApproachComputer Security – ESORICS 201210.1007/978-3-642-33167-1_17(289-306)Online publication date: 2012
https://doi.org/10.1007/978-3-642-33167-1_17
Kondakci SYilmaz GMakarevich OElçi AOrgun MHuss SBabenko LChefranov AVaradharajan V(2010)Implementation and performance evaluation of the RSEP protocol on ARM and intel platformsProceedings of the 3rd international conference on Security of information and networks10.1145/1854099.1854139(194-202)Online publication date: 7-Sep-2010
https://dl.acm.org/doi/10.1145/1854099.1854139
Show More Cited By

Index Terms

Security analysis of network protocols: logical and computational methods
1. Networks
  1. Network protocols
    1. Protocol correctness
      1. Protocol testing and verification

Recommendations

Security analysis of network protocols: compositional reasoning and complexity-theoretic foundations
A Model for Secure Protocols and Their Compositions

This paper develops a foundation for reasoning about protocol security. We adopt a model-based approach for defining protocol security properties. This allows us to describe security properties in greater detail and precision than previous frameworks. ...
Internet of Things Protocols Comparison, Architecture, Vulnerabilities and Security: State of the art
ICCWCS'17: Proceedings of the 2nd International Conference on Computing and Wireless Communication Systems

The internet of things is a topical subject, which consists in connecting the objects to each other in order to communicate via networks. This communication is managed by protocols to ensure the proper exchange of information and data while respecting ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PPDP '05: Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming

July 2005

260 pages

ISBN:1595930906

DOI:10.1145/1069774

General Chair:
Pedro Barahona
Universidade Nova de Lisboa, Portugal
,
Program Chair:
Amy Felty
University of Ottawa, Canada

Copyright © 2005 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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 July 2005

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

PPDP05

Sponsor:

PPDP05: Principles and Practice of Declarative Programming 2005

July 11 - 13, 2005

Lisbon, Portugal

Acceptance Rates

Overall Acceptance Rate 230 of 486 submissions, 47%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
630
Total Downloads

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

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Hu YPang LPei QWang X(2015)Instruction Clustering Analysis for Network Protocol's Abnormal BehaviorProceedings of the 2015 10th International Conference on P2P, Parallel, Grid, Cloud and Internet Computing (3PGCIC)10.1109/3PGCIC.2015.69(791-794)Online publication date: 4-Nov-2015
https://dl.acm.org/doi/10.1109/3PGCIC.2015.69
Gu QJones KZang WYu MLiu P(2012)Revealing Abuses of Channel Assignment Protocols in Multi-channel Wireless Networks: An Investigation Logic ApproachComputer Security – ESORICS 201210.1007/978-3-642-33167-1_17(289-306)Online publication date: 2012
https://doi.org/10.1007/978-3-642-33167-1_17
Kondakci SYilmaz GMakarevich OElçi AOrgun MHuss SBabenko LChefranov AVaradharajan V(2010)Implementation and performance evaluation of the RSEP protocol on ARM and intel platformsProceedings of the 3rd international conference on Security of information and networks10.1145/1854099.1854139(194-202)Online publication date: 7-Sep-2010
https://dl.acm.org/doi/10.1145/1854099.1854139
Sutcliffe G(2007)TPTP, TSTP, CASC, etc.Computer Science – Theory and Applications10.1007/978-3-540-74510-5_4(6-22)Online publication date: 2007
https://doi.org/10.1007/978-3-540-74510-5_4
Cervesato IDurgin NLincoln PMitchell JScedrov A(1999)A meta-notation for protocol analysisProceedings of the 12th IEEE Computer Security Foundations Workshop10.1109/CSFW.1999.779762(55-69)Online publication date: 1999
https://doi.org/10.1109/CSFW.1999.779762

View Options

Get Access

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