Article

Probabilistic polynomial-time semantics for a protocol security logic

Authors:

John C. Mitchell,

Vitaly Shmatikov,

Mathieu TuruaniAuthors Info & Claims

ICALP'05: Proceedings of the 32nd international conference on Automata, Languages and Programming

Pages 16 - 29

https://doi.org/10.1007/11523468_2

Published: 11 July 2005 Publication History

Abstract

We describe a cryptographically sound formal logic for proving protocol security properties without explicitly reasoning about probability, asymptotic complexity, or the actions of a malicious attacker. The approach rests on a new probabilistic, polynomial-time semantics for an existing protocol security logic, replacing an earlier semantics that uses nondeterministic symbolic evaluation. While the basic form of the protocol logic remains unchanged from previous work, there are some interesting technical problems involving the difference between efficiently recognizing and efficiently producing a value, and involving a reinterpretation of standard logical connectives that seems necessary to support certain forms of reasoning.

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]

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

[3]

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

[4]

M. Bellare, A. Boldyreva, and S. Micali. Public-key encryption in a multi-user setting: Security proofs and improvements. In Advances in Cryptology - EUROCRYPT 2000, Proceedings, pages 259-274, 2000.

[5]

M. Bellare and P. Rogaway. Entity authentication and key distribution. In Proceedings of the 13th Annual International Cryptology Conference on Advances in Cryptology (CRYPTO '93), pages 232-249. Springer-Verlag, 1994.

Digital Library

[6]

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

[7]

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.

[8]

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

[9]

D. Dolev and A. Yao. On the security of public-key protocols. IEEE Transactions on Information Theory, 2(29):198-208, 1983.

Digital Library

[10]

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

[11]

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.

[12]

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

Digital Library

[13]

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

[14]

R. Janvier, L. Mazare, and Y. Lakhnech. Completing the picture: Soundness of formal encryption in the presence of active adversaries. In Proceedings of 14th European Symposium on Programming (ESOP'05), Lecture Notes in Computer Science, pages 172-185. Springer-Verlag, 2005.

Digital Library

[15]

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.

[16]

N. J. Nilsson. Probabilistic logic. Artificial Intelligence, 28(1):71-87, 1986.

Digital Library

[17]

V. Shoup. On formal models for secure key exchange (version 4). Technical Report RZ 3120, IBM Research, 1999.

[18]

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

Petcher AMorrisett G(2015)The Foundational Cryptography FrameworkProceedings of the 4th International Conference on Principles of Security and Trust - Volume 903610.1007/978-3-662-46666-7_4(53-72)Online publication date: 11-Apr-2015
https://dl.acm.org/doi/10.1007/978-3-662-46666-7_4
Zhang JMa JYang C(2015)Protocol Derivation System for the Needham-Schroeder familySecurity and Communication Networks10.1002/sec.5658:16(2687-2703)Online publication date: 10-Nov-2015
https://dl.acm.org/doi/10.1002/sec.565
Böhl FCortier VWarinschi BSadeghi AGligor VYung M(2013)Deduction soundnessProceedings of the 2013 ACM SIGSAC conference on Computer & communications security10.1145/2508859.2516711(1261-1272)Online publication date: 4-Nov-2013
https://dl.acm.org/doi/10.1145/2508859.2516711
Show More Cited By

Index Terms

Probabilistic polynomial-time semantics for a protocol security logic

Index terms have been assigned to the content through auto-classification.

Recommendations

Semantics and logic for security protocols

This paper presents a sound BAN-like logic for reasoning about security protocols with theorem prover support. The logic has formulas for sending and receiving messages (with nonces, public and private encryptions, etc.), and has both temporal and ...
Semantics for disjunctive logic programs
Topological semantics of justification logic
CSR'08: Proceedings of the 3rd international conference on Computer science: theory and applications

The Justification Logic is a family of logical systems obtained from epistemic logics by adding new type of formulas t:F which reads as t is a justification for F. The major epistemic modal logic S4 has a well-known Tarski topological interpretation ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

ICALP'05: Proceedings of the 32nd international conference on Automata, Languages and Programming

July 2005

1476 pages

ISBN:3540275800

Editors:
Luís Caires
CITI / Departamento de Informática, Universidade Nova de Lisboa, Portugal
,
Giuseppe F. Italiano
Dipartimento di Informatica, Sistemi e Produzione, Università di Roma "Tor Vergata", via del Politecnico 1, Roma, Italy
,
Luís Monteiro
Departamento de Informatica, Universidade Nova de Lisboa, via del Politecnico 1, Caparica, Portugal
,
Catuscia Palamidessi
Departamento de Informatica, Ecole Polytechnique, Rue de Saclay, Palaiseau Cedex, France
,
Moti Yung
Computer Science Department, Google Inc. and Columbia University, 1214 Amsterdam Avenue, New York, France

Sponsors

Fundacao para a Ciencia e Tecnologia
FCT: Foundation for Science and Technology
Centro de Lógica e Computação/IST/UTL: Centro de Lógica e Computação/IST/UTL

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 11 July 2005

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

29
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 26 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Petcher AMorrisett G(2015)The Foundational Cryptography FrameworkProceedings of the 4th International Conference on Principles of Security and Trust - Volume 903610.1007/978-3-662-46666-7_4(53-72)Online publication date: 11-Apr-2015
https://dl.acm.org/doi/10.1007/978-3-662-46666-7_4
Zhang JMa JYang C(2015)Protocol Derivation System for the Needham-Schroeder familySecurity and Communication Networks10.1002/sec.5658:16(2687-2703)Online publication date: 10-Nov-2015
https://dl.acm.org/doi/10.1002/sec.565
Böhl FCortier VWarinschi BSadeghi AGligor VYung M(2013)Deduction soundnessProceedings of the 2013 ACM SIGSAC conference on Computer & communications security10.1145/2508859.2516711(1261-1272)Online publication date: 4-Nov-2013
https://dl.acm.org/doi/10.1145/2508859.2516711
Bana GHasebe KOkada MSadeghi AGligor VYung M(2013)Computationally complete symbolic attacker and key exchangeProceedings of the 2013 ACM SIGSAC conference on Computer & communications security10.1145/2508859.2516710(1231-1246)Online publication date: 4-Nov-2013
https://dl.acm.org/doi/10.1145/2508859.2516710
Halpern J(2013)From Qualitative to Quantitative Proofs of Security Properties Using First-Order Conditional LogicProceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS.2013.66(2-3)Online publication date: 25-Jun-2013
https://dl.acm.org/doi/10.1109/LICS.2013.66
Blanchet B(2012)Security protocol verificationProceedings of the First international conference on Principles of Security and Trust10.1007/978-3-642-28641-4_2(3-29)Online publication date: 24-Mar-2012
https://dl.acm.org/doi/10.1007/978-3-642-28641-4_2
Bana GComon-Lundh H(2012)Towards unconditional soundnessProceedings of the First international conference on Principles of Security and Trust10.1007/978-3-642-28641-4_11(189-208)Online publication date: 24-Mar-2012
https://dl.acm.org/doi/10.1007/978-3-642-28641-4_11
Fournet CKohlweiss MStrub PChen YDanezis GShmatikov V(2011)Modular code-based cryptographic verificationProceedings of the 18th ACM conference on Computer and communications security10.1145/2046707.2046746(341-350)Online publication date: 17-Oct-2011
https://dl.acm.org/doi/10.1145/2046707.2046746
Brzuska CFischlin MWarinschi BWilliams SChen YDanezis GShmatikov V(2011)Composability of bellare-rogaway key exchange protocolsProceedings of the 18th ACM conference on Computer and communications security10.1145/2046707.2046716(51-62)Online publication date: 17-Oct-2011
https://dl.acm.org/doi/10.1145/2046707.2046716
Cortier VKremer SWarinschi B(2011)A Survey of Symbolic Methods in Computational Analysis of Cryptographic SystemsJournal of Automated Reasoning10.1007/s10817-010-9187-946:3-4(225-259)Online publication date: 1-Apr-2011
https://dl.acm.org/doi/10.1007/s10817-010-9187-9
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents