article

Mobile values, new names, and secure communication

Authors:

Cédric FournetAuthors Info & Claims

ACM SIGPLAN Notices, Volume 36, Issue 3

Pages 104 - 115

https://doi.org/10.1145/373243.360213

Published: 01 January 2001 Publication History

Abstract

We study the interaction of the "new" construct with a rich but common form of (first-order) communication. This interaction is crucial in security protocols, which are the main motivating examples for our work; it also appears in other programming-language contexts. Specifically, we introduce a simple, general extension of the pi calculus with value passing, primitive functions, and equations among terms. We develop semantics and proof techniques for this extended language and apply them in reasoning about some security protocols.

References

[1]

Marten Abadi. Protection in programming-language translations. In Kim G. Larsen, Sven Skyum, and Glynn Winskel, editors, Proceedings of the 25th International Colloquium on Automata, Languages and Programming, volume 1443 of Lecture Notes in Computer Science, pages 868-883. Springer, July 1998. Also Digital Equipment Corporation Systems Research Center report No. 154, April 1998.]]

Digital Library

[2]

Martin Abadi. Secrecy by typing in security protocols. Journal of the ACM, 46(5):749-786, September 1999.]]

Digital Library

[3]

Martin Abadi, Cedric Fournet, and Georges Gonthier. Secure implementation of channel abstractions. In Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science, pages 105-116, June 1998.]]

Digital Library

[4]

Martin Abadi, Cedric Fournet, and Georges Gonthier. Authentication primitives and their compilation. In Proceedings of the 27th ACM Symposium on Principles of Programming Languages, pages 302-315, January 2000.]]

Digital Library

[5]

Martpin Abadi and Andrew D. Gordon. A calculus for cryptographic protocols: The spi calculus. Information and Computation, 148(1):1-70, January 1999. An extended version appeared as Digital Equipment Corporation Systems Research Center report No. 149, January 1998.]]

Digital Library

[6]

Martin Abadi and Phillip Rogaway. Reconciling two views of cryptography (The computational soundness of formal encryption). In Proceedings of the First IFIP International Conference on Theoretical Computer Science, volume 1872 of Lecture Notes in Computer Science, pages 3-22. Springer-Verlag, August 2000.]]

Digital Library

[7]

Roberto M. Amadio and Denis Lugiez. On the reachability problem in cryptographic protocols. In Catuscia Palamidessi, editor, CONCUR 2000: Concurrency Theory (11th International Conference), volume 1877 of Lecture Notes in Computer Science, pages 380-394. Springer-Verlag, August 2000.]]

Digital Library

[8]

Mihir Bellare and Phillip Rogaway. Entity authentication and key distribution. In Advances in Cryptology CRYPTO '94, volume 773 of Lecture Notes in Computer Science, pages 232-249. Springer-Verlag, 1993.]]

[9]

Chiara Bodei. Security Issues in Process Calculi. PhD thesis, Universita di Pisa, January 2000.]]

[10]

Chiara Bodei, Pierpaolo Degano, Flemming Nielson, and Hanne Riis Nielson. Control ow analysis for the pi-calculus. In Davide Sangiorgi and Robert de Simone, editors, CONCUR '98: Concurrency Theory (9th International Conference), volume 1466 of Lecture Notes in Computer Science, pages 84-98. Springer, September 1998.]]

Digital Library

[11]

Chiara Bodei, Pierpaolo Degano, Flemming Nielson, and Hanne Riis Nielson. Static analysis of processes for no read-up and no write-down. In Wolfgang Thomas, editor, Proceedings of the Second International Conference on Foundations of Software Science and Computation Structures (FoSSaCS '99), volume 1578 of Lecture Notes in Computer Science, pages 120-134. Springer, 1999.]]

Digital Library

[12]

Michele Boreale, Rocco De Nicola, and Rosario Pugliese. Proof techniques for cryptographic processes. In Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science, pages 157-166, July 1999.]]

Digital Library

[13]

Luca Cardelli. Mobility and security. In F. L. Bauer and R. Steinbrueggen, editors, Foundations of Secure Computation, NATO Science Series, pages 3-37. IOS Press, 2000.]]

[14]

Sylvain Conchon and Fabrice Le Fessant. Jocaml: Mobile agents for Objective-Caml. In First International Symposium on Agent Systems and Applications (ASA'99)/Third International Symposium on Mobile Agents (MA'99), pages 22-29, October 1999.]]

Digital Library

[15]

Core SDI S.A. ssh insertion attack. Available at http://www.core-sdi.com/soft/ssh/attack.txt, July 1998.]]

[16]

Mads Dam. Proving trust in systems of secondorder processes. In Proceedings of the 31th Hawaii International Conference on System Sciences, volume VII, pages 255-264, 1998.]]

Digital Library

[17]

W. Diffie and M. Hellman. New directions in cryptography. IEEE Transactions on Information Theory, IT-22(6):644-654, November 1976.]]

Digital Library

[18]

Whitfield Diffie, Paul C. van Oorschot, and Michael J. Wiener. Authentication and authenticated key exchanges. Designs, Codes and Cryptography, 2:107-125, 1992.]]

Digital Library

[19]

Danny Dolev and Andrew C. Yao. On the security of public key protocols. IEEE Transactions on Information theory, IT-29(12):198-208, March 1983.]]

Digital Library

[20]

Cedric Fournet and Georges Gonthier. A hierarchy of equivalences for asynchronous calculi. In Kim G. Larsen, Sven Skyum, and Glynn Winskel, editors, Proceedings of the 25th International Colloquium on Automata, Languages and Programming, volume 1443 of Lecture Notes in Computer Science, pages 844-855. Springer, July 1998.]]

Digital Library

[21]

Alan O. Freier, Philip Karlton, and Paul C. Kocher. The SSL protocol: Version 3.0. Available at http:// home.netscape.com/eng/ssl3/draft302.txt, Novem-ber 1996.]]

[22]

Shafi Goldwasser and Mihir Bellare. Lecture notes on cryptography. Summer Course "Cryptography and Computer Security: at MIT, 1996-1999, August 1999.]]

[23]

Shafi Goldwasser and Silvio Micali. Probabilistic encryption. Journal of Computer and System Sciences, 28:270-299, April 1984.]]

[24]

Shafi Goldwasser, Silvio Micali, and Ronald Rivest. A digital signature scheme secure against adaptive chosen-message attack. SIAM Journal on Computing, 17:281-308, 1988.]]

Digital Library

[25]

R. Kemmerer, C. Meadows, and J. Millen. Three system for cryptographic protocol analysis. Journal of Cryptology, 7(2):79-130, Spring 1994.]]

Digital Library

[26]

Hugo Krawczyk. SKEME: A versatile secure key exchange mechanism for internet. In Proceedings of the Internet Society Symposium on Network and Distributed Systems Security, February 1996. Available at http://bilbo.isu.edu/sndss/sndss96.html.]]

Digital Library

[27]

Ben Liblit and Alexander Aiken. Type systems for distributed data structures. In Proceedings of the 27th ACM Symposium on Principles of Programming Languages, pages 199-213, January 2000.]]

Digital Library

[28]

P. Lincoln, J. Mitchell, M. Mitchell, and A. Scedrov. A probabilistic poly-time framework for protocol analysis. In Proceedings of the Fifth ACM Conference on Computer and Communications Security, pages 112- 121, 1998.]]

Digital Library

[29]

Gavin Lowe. Breaking and fixing the Needham- Schroeder public-key protocol using FDR. In Tools and Algorithms for the Construction and Analysis of Systems, volume 1055 of Lecture Notes in Computer Science, pages 147-166. Springer Verlag, 1996.]]

Digital Library

[30]

Alfred J. Menezes, Paul C. van Oorschot, and Scott A. Vanstone. Handbook of Applied Cryptography. CRC Press, 1996.]]

Digital Library

[31]

Robin Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989.]]

Digital Library

[32]

Robin Milner. Communicating and Mobile Systems: the -Calculus. Cambridge University Press, 1999.]]

Digital Library

[33]

John C. Mitchell. Foundations for Programming Languages. MIT Press, 1996.]]

Digital Library

[34]

John C. Mitchell, Mark Mitchell, and Ulrich Stern. Automated analysis of cryptographic protocols using Mur. In Proceedings of the 1997 IEEE Symposium on Security and Privacy, pages 141-151, 1997.]]

Digital Library

[35]

Lawrence C. Paulson. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 6(1-2):85-128, 1998.]]

[36]

Birgit Pfitzmann, Matthias Schunter, and Michael Waidner. Cryptographic security of reactive systems (extended abstract). Electronic Notes in Theoretical Computer Science, 32, April 2000.]]

[37]

Benjamin C. Pierce and David N. Turner. Pict: A programming language based on the pi-calculus. In Gordon Plotkin, Colin Stirling, and Mads Tofte, editors, Proof, Language and Interaction: Essays in Honour of Robin Milner, Foundations of Computing. MIT Press, May 2000.]]

Digital Library

[38]

D. Sangiorgi. On the bisimulation proof method. Journal of Mathematical Structures in Computer Science, 8:447-479, 1998.]]

Digital Library

[39]

Steve Schneider. Security properties and CSP. In Proceedings of the 1996 IEEE Symposium on Security and Privacy, pages 174-187, 1996.]]

Digital Library

[40]

Bruce Schneier. Applied Cryptography: Protocols, Algorithms, and Source Code in C. John Wiley & Sons, Inc., second edition, 1996.]]

Digital Library

[41]

Stuart G. Stubblebine and Virgil D. Gligor. On message integrity in cryptographic protocols. In Proceedings of the 1992 IEEE Symposium on Research in Security and Privacy, pages 85-104, 1992.]]

Digital Library

[42]

F. Javier Thayer Fabrega, Jonathan C. Herzog, and Joshua D. Guttman. Strand spaces: Why is a security protocol correct? In Proceedings of the 1998 IEEE Symposium on Security and Privacy, pages 160-171, May 1998.]]

[43]

Bjorn Victor. The Fusion Calculus: Expressiveness and Symmetry in Mobile Processes. PhD thesis, Dept. of Computer Systems, Uppsala University, Sweden, June 1998.]]

[44]

Andrew C. Yao. Theory and applications of trapdoor functions. In Proceedings of the 23rd Annual Symposium on Foundations of Computer Science (FOCS 82), pages 80-91, 1982.]]

Digital Library

Cited By

Dansarie M(2024)Security Issues in Special-Purpose Digital Radio Communication Systems: A Systematic ReviewIEEE Access10.1109/ACCESS.2024.342009112(91101-91126)Online publication date: 2024
https://doi.org/10.1109/ACCESS.2024.3420091
Mohammed BAl-Shareeda MManickam SAl-Mekhlafi ZAlayba ASallam A(2023)ANAA-Fog: A Novel Anonymous Authentication Scheme for 5G-Enabled Vehicular Fog ComputingMathematics10.3390/math1106144611:6(1446)Online publication date: 16-Mar-2023
https://doi.org/10.3390/math11061446
Wu TMeng QYang LKumari SPirouz M(2023)Amassing the Security: An Enhanced Authentication and Key Agreement Protocol for Remote Surgery in Healthcare EnvironmentComputer Modeling in Engineering & Sciences10.32604/cmes.2022.019595134:1(317-341)Online publication date: 2023
https://doi.org/10.32604/cmes.2022.019595
Show More Cited By

Recommendations

Mobile values, new names, and secure communication
POPL '01: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

We study the interaction of the "new" construct with a rich but common form of (first-order) communication. This interaction is crucial in security protocols, which are the main motivating examples for our work; it also appears in other programming-...
Pure Modal Logic of Names and Tableau Systems

By a pure modal logic of names (PMLN) we mean a quantifier-free formulation of such a logic which includes not only traditional categorical, but also modal categorical sentences with modalities de re and which is an extension of Propositional Logic. For ...
Perfectly Reliable and Secure Communication Tolerating Static and Mobile Mixed Adversary
ICITS '08: Proceedings of the 3rd international conference on Information Theoretic Security

In this paper, we study the problem of perfectly reliable message transmission(PRMT) and perfectly secure message transmission(PSMT) between a sender Sand a receiver Rin an undirected synchronous network, tolerating a mixed adversary, where the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 36, Issue 3

March 2001

303 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/373243

Editors:
Cindy Norris
Appalachian State Univ., Boone, NC
,
James B. Fenwick
Appalachian State Univ., Boone, NC

Issue’s Table of Contents

POPL '01: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2001
304 pages
ISBN:1581133367
DOI:10.1145/360204
Chairmen:
Chris Hankin
Imperial College, London, U. K.
,
Dave Schmidt
Kansas State Univ., Manhattan

Copyright © 2001 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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 2001

Published in SIGPLAN Volume 36, Issue 3

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

669
Total Citations
View Citations
1,688
Total Downloads

Downloads (Last 12 months)35
Downloads (Last 6 weeks)7

Reflects downloads up to 17 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Dansarie M(2024)Security Issues in Special-Purpose Digital Radio Communication Systems: A Systematic ReviewIEEE Access10.1109/ACCESS.2024.342009112(91101-91126)Online publication date: 2024
https://doi.org/10.1109/ACCESS.2024.3420091
Mohammed BAl-Shareeda MManickam SAl-Mekhlafi ZAlayba ASallam A(2023)ANAA-Fog: A Novel Anonymous Authentication Scheme for 5G-Enabled Vehicular Fog ComputingMathematics10.3390/math1106144611:6(1446)Online publication date: 16-Mar-2023
https://doi.org/10.3390/math11061446
Wu TMeng QYang LKumari SPirouz M(2023)Amassing the Security: An Enhanced Authentication and Key Agreement Protocol for Remote Surgery in Healthcare EnvironmentComputer Modeling in Engineering & Sciences10.32604/cmes.2022.019595134:1(317-341)Online publication date: 2023
https://doi.org/10.32604/cmes.2022.019595
Wu TMeng QKumari SZhang P(2022)Rotating behind Security: A Lightweight Authentication Protocol Based on IoT-Enabled Cloud Computing EnvironmentsSensors10.3390/s2210385822:10(3858)Online publication date: 19-May-2022
https://doi.org/10.3390/s22103858
周鑫(2022)An Efficient Remote User Authentication Protocol Based on Elliptic CurveAdvances in Applied Mathematics10.12677/AAM.2022.111290211:12(8550-8566)Online publication date: 2022
https://doi.org/10.12677/AAM.2022.1112902
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
Horne RMauw SYurkov S(2022)Unlinkability of an Improved Key Agreement Protocol for EMV 2nd Gen Payments2022 IEEE 35th Computer Security Foundations Symposium (CSF)10.1109/CSF54842.2022.9919666(364-379)Online publication date: Aug-2022
https://doi.org/10.1109/CSF54842.2022.9919666
Rakeei MGiustolisi RLenzini G(2022)Secure Internet Exams Despite CoercionData Privacy Management, Cryptocurrencies and Blockchain Technology10.1007/978-3-031-25734-6_6(85-100)Online publication date: 26-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-25734-6_6
Delaune SLallemand J(2022)One Vote Is Enough for Analysing PrivacyComputer Security – ESORICS 202210.1007/978-3-031-17140-6_9(173-194)Online publication date: 25-Sep-2022
https://doi.org/10.1007/978-3-031-17140-6_9
Yang LChen YWu T(2021)Provably Secure Client-Server Key Management Scheme in 5G NetworksWireless Communications & Mobile Computing10.1155/2021/40831992021Online publication date: 1-Jan-2021
https://dl.acm.org/doi/10.1155/2021/4083199
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 Issue’s Table of Contents