article

Logical relation for encryption

Authors:

Benjamin C. PierceAuthors Info & Claims

Journal of Computer Security, Volume 11, Issue 4

Pages 521 - 554

Published: 01 July 2003 Publication History

Abstract

The theory of relational parametricity and its logical relations proof technique are powerful tools for reasoning about information hiding in the polymorphic λ-calculus. We investigate the application of these tools in the security domain by defining a cryptographic λ-calculus - an extension of the standard simply typed λ-calculus with primitives for encryption, decryption, and key generation - and introducing syntactic logical relations (in the style of Pitts and Birkedal-Harper) for this calculus that can be used to prove behavioral equivalences between programs that use encryption.We illustrate the framework by encoding some simple security protocols, including the Needham-Schroeder public-key protocol. We give a natural account of the well-known attack on the original protocol and a straightforward proof that the improved variant of the protocol is secure.

References

[1]

{1} M. Abadi, Secrecy by typing in security protocols, Journal of the ACM46(5) (1999), 749-786.]]

[2]

{2} M. Abadi and A.D. Gordon, A bisimulation method for cryptographic protocols, Nordic Journal of Computing5 (1998), 267-303.]]

[3]

{3} M. Abadi and A.D. Gordon, A calculus for cryptographic protocols: The spi calculus, Information and Computation, 148(1) (1999), 1-70. A preliminary version appeared in: Proceedings of the 4th ACM Conference on Computer and Communications Security, 1997, pp. 36-47.]]

Digital Library

[4]

{4} M. Abadi and C. Fournet, Mobile values, new names, and secure communication, in: Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2001, pp. 104-115.]]

[5]

{5} G.M. Bierman, A.M. Pitts and C.V. Russo, Operational properties of Lily, a polymorphic linear lambda calculus with recursion, in: Higher Order Operational Techniques in Semantics, Volume 41 of Electronic Notes in Theoretical Computer Science, Elsevier Science, 2000.]]

[6]

{6} L. Birkedal and R. Harper, Relational interpretations of recursive types in an operational setting, Information and Computation155(1-2) (1999), 3-63.]]

[7]

{7} M. Boreale, R. De Nicola and R. Pugliese, Proof techniques for cryptographic processes, 1999. ftp://rap.dsi.unifi.it/pub/papers/spi.ps.gz, An extended and revised version of the paper that appeared in 14th Annual IEEE Symposium on Logic in Computer Science, 1999, pp. 157-166.]]

[8]

{8} D. Dolev and A.C. Yao, On the security of public key protocols, IEEE Transactions on Information Theory29(2) (1983), 198-208.]]

[9]

{9} A. Durante, R. Focardi and R. Gorrieri, CVS: A compiler for the analysis of cryptographic protocols, in: 12th IEEE Computer Security Foundations Workshop, 1999, pp. 203-212.]]

[10]

{10} A. Durante, R. Focardi and R. Gorrieri, A compiler for analysing cryptographic protocols using noninterference, ACM Transactions on Software Engineering and Methodology9(4) (2000), 488-528.]]

Digital Library

[11]

{11} A.D. Gordon and A. Jeffrey, Authenticity by typing for security protocols, in: 14th IEEE Computer Security Foundations Workshop, 2001, pp. 145-159.]]

Digital Library

[12]

{12} J. Heather, G. Lowe and S. Schneider, How to prevent type flaw attacks on security protocols, in: 13th IEEE Computer Security Foundations Workshop, 2000, pp. 255-268.]]

[13]

{13} N. Heintze and E. Clarke, eds, Workshop on Formal Methods and Security Protocols, 1999. http://cm.bell-labs.com/cm/cs/who/nch/fmsp99/.]]

[14]

{14} N. Heintze and J.G. Riecke, The SLam calculus: Programming with secrecy and integrity, in: Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1998.]]

[15]

{15} M. Hennessy and J. Riely, Information flow vs. resource access in the asynchronous pi-calculus, in: Proceedings of the 27th International Colloquium on Automata, Languages and Programming, Volume 1853 of Lecture Notes in Computer Science, Springer-Verlag, 2000, pp. 415-427.]]

[16]

{16} K. Honda and N. Yoshida, A uniform framework for secure information flow, in: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2002, pp. 81-92.]]

[17]

{17} IEEE computer security foundations workshop, http://www2.csl.sri.com/csfw/index.html.]]

[18]

{18} G. Lowe, An attack on the Needham-Schroeder public-key authentication protocol, Information Processing Letters56(3) (1995), 131-133.]]

[19]

{19} C. Meadows, Formal verification of cryptographic protocols: A survey, in: Advances in Cryptology - Asiacrypt '94, Volume 917 of Lecture Notes in Computer Science, Springer-Verlag, 1995, pp. 133-150.]]

Digital Library

[20]

{20} C. Meadows, Open issues in formal methods for cryptographic protocol analysis, in: DARPA Information Survivability Conference and Exposition, IEEE Computer Society, 2000, pp. 237-250.]]

[21]

{21} J.K. Millen, A necessarily parallel attack, in: Workshop on Formal Methods and Security Protocols, 1999. http://www.cs.bell-labs.com/who/nch/fmsp99/program.html.]]

[22]

{22} J.C. Mitchell, Foundations for Programming Languages, MIT Press, 1996.]]

[23]

{23} J.H. Morris, Jr. Protection in programming languages, Communications of the ACM16(1) (1973) 15-21.]]

Digital Library

[24]

{24} R. Needham and M. Schroeder, Using encryption for authentication in large networks of computers, Communications of the ACM21(12) (1978) 993-999.]]

Digital Library

[25]

{25} B. Pierce and D. Sangiorgi, Typing and subtyping for mobile processes, in: Eighth Annual IEEE Symposium on Logic in Computer Science, 1993, pp. 376-385. Full version in Mathematical Structures in Computer Science6(5) (1996) 409-453.]]

[26]

{26} B. Pierce and E. Sumii, Relating cryptography and polymolphism, 2000. Manuscript: http://www.yl.is.s.u-tokyo.ac.jp/~sumii/pub/infohide.ps.gz.]]

[27]

{27} A.M. Pitts, Existential types: Logical relations and operational equivalence, in: Proceedings of the 25th International Colloquium on Automata, Languages and Programming, Volume 1443 of Lecture Notes in Computer Science, Springer-Verlag, 1998, pp. 309-326.]]

[28]

{28} A.M. Pitts, Parametric polymorphism and operational equivalence, Mathematical Structures in Computer Science10 (2000) 321-359. A preliminary version appeared in HOOTS II Second Workshop on Higher-Order Operational Techniques in Semantics, Electronic Notes in Theoretical Computer Science, Vol. 10, 1998.]]

[29]

{29} A.M. Pitts and J.R.X. Ross, Process calculus based upon evaluation to committed form, Theoretical Computer Science195 (1998), 155-182. A preliminary version appeared in: CONCUR '96: Concurrency Theory, Lecture Notes in Computer Science, Springer-Verlag, Vol. 1119, 1996, pp. 18-33.]]

[30]

{30} A.M. Pitts and I. Stark, Operational reasoning for functions with local state, in: Higher Order Operational Techniques in Semantics, Cambridge University Press, 1998, pp. 227-273.]]

Digital Library

[31]

{31} F. Pottier, A simple view of type-secure information flow in the π-calculus, in: 15th IEEE Computer Security Foundations Workshop, 2002, pp 320-330.]]

[32]

{32} F. Pottier and V. Simonet, Information flow inference for ML, in: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2002, pp. 319-330.]]

Digital Library

[33]

{33} J.C. Reynolds, Types, abstraction and parametric polymorphism, in: Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, 1983, pp. 513-523.]]

[34]

{34} P.Y.A. Ryan and S.A. Schneider, Process algebra and non-interference, in: 12th IEEE Computer Security Foundations Workshop, 1999, pp. 214-227.]]

[35]

{35} G. Smith and D. Volpano, Secure information flow in a multi-threaded imperative language, in: Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1998, pp. 355-364.]]

[36]

{36} I. Stark, Names and higher-order functions, PhD thesis, University of Cambridge, 1994. http://www.dcs.ed.ac.uk/home/stark/publications/thesis.html.]]

[37]

{37} D.N. Turner, The polymorphic pi-calculus: theory and implementation, PhD thesis, University of Edinburgh, 1995.]]

[38]

{38} D. Volpano, Formalization and proof of secrecy properties, in: 12th IEEE Computer Security Foundations Workshop, 1999, pp. 92-95.]]

[39]

{39} P. Wadler, Theorems for free! in: Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture, ACM, 1989, pp, 347-359.]]

Cited By

Patrignani MKünnemann RWahby RCecchetti E(2024)Universal Composability Is Robust CompilationACM Transactions on Programming Languages and Systems10.1145/369823446:4(1-64)Online publication date: 31-Dec-2024
https://dl.acm.org/doi/10.1145/3698234
Devriese DPatrignani MPiessens F(2022)Two Parametricities Versus Three Universal TypesACM Transactions on Programming Languages and Systems10.1145/353965744:4(1-43)Online publication date: 21-Sep-2022
https://dl.acm.org/doi/10.1145/3539657
Backes MHriţcu CMaffei M(2014)Union, intersection and refinement types and reasoning about type disjointness for secure protocol implementationsJournal of Computer Security10.5555/2595841.259584522:2(301-353)Online publication date: 1-Mar-2014
https://dl.acm.org/doi/10.5555/2595841.2595845
Show More Cited By

Recommendations

Asynchronous Probabilistic Couplings in Higher-Order Separation Logic

Probabilistic couplings are the foundation for many probabilistic relational program logics and arise when relating random sampling statements across two programs. In relational program logics, this manifests as dedicated coupling rules that, e.g., say ...
Conditional Contextual Refinement

Much work in formal verification of low-level systems is based on one of two approaches: refinement or separation logic. These two approaches have complementary benefits: refinement supports the use of programs as specifications, as well as transitive ...

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 11, Issue 4

Special issue on CSFW14

July 2003

271 pages

ISSN:0926-227X

Issue’s Table of Contents

Publisher

IOS Press

Netherlands

Publication History

Published: 01 July 2003

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

21
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 03 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Patrignani MKünnemann RWahby RCecchetti E(2024)Universal Composability Is Robust CompilationACM Transactions on Programming Languages and Systems10.1145/369823446:4(1-64)Online publication date: 31-Dec-2024
https://dl.acm.org/doi/10.1145/3698234
Devriese DPatrignani MPiessens F(2022)Two Parametricities Versus Three Universal TypesACM Transactions on Programming Languages and Systems10.1145/353965744:4(1-43)Online publication date: 21-Sep-2022
https://dl.acm.org/doi/10.1145/3539657
Backes MHriţcu CMaffei M(2014)Union, intersection and refinement types and reasoning about type disjointness for secure protocol implementationsJournal of Computer Security10.5555/2595841.259584522:2(301-353)Online publication date: 1-Mar-2014
https://dl.acm.org/doi/10.5555/2595841.2595845
Jeffrey AMight MVan Horn DGiacobazzi RAbel ASheard T(2013)Causality for free!Proceedings of the 7th workshop on Programming languages meets program verification10.1145/2428116.2428127(57-68)Online publication date: 22-Jan-2013
https://dl.acm.org/doi/10.1145/2428116.2428127
Sangiorgi DKobayashi NSumii E(2011)Environmental bisimulations for higher-order languagesACM Transactions on Programming Languages and Systems10.1145/1889997.189000233:1(1-69)Online publication date: 25-Jan-2011
https://dl.acm.org/doi/10.1145/1889997.1890002
Neis GDreyer DRossberg A(2011)Non-parametric parametricityJournal of Functional Programming10.1017/S095679681100016521:4-5(497-562)Online publication date: 1-Sep-2011
https://dl.acm.org/doi/10.1017/S0956796811000165
Neis GDreyer DRossberg A(2009)Non-parametric parametricityACM SIGPLAN Notices10.1145/1631687.159657244:9(135-148)Online publication date: 31-Aug-2009
https://dl.acm.org/doi/10.1145/1631687.1596572
Neis GDreyer DRossberg AHutton GTolmach A(2009)Non-parametric parametricityProceedings of the 14th ACM SIGPLAN international conference on Functional programming10.1145/1596550.1596572(135-148)Online publication date: 31-Aug-2009
https://dl.acm.org/doi/10.1145/1596550.1596572
Matthews JFindler R(2009)Operational semantics for multi-language programsACM Transactions on Programming Languages and Systems10.1145/1498926.149893031:3(1-44)Online publication date: 21-Apr-2009
https://dl.acm.org/doi/10.1145/1498926.1498930
Matthews JAhmed A(2008)Parametric polymorphism through run-time sealing or, theorems for low, low prices!Proceedings of the Theory and practice of software, 17th European conference on Programming languages and systems10.5555/1792878.1792881(16-31)Online publication date: 29-Mar-2008
https://dl.acm.org/doi/10.5555/1792878.1792881
Show More Cited By

View Options

View options

Figures

Tables

Media

View Issue’s Table of Contents