article

Private authentication

Authors:

Martín Abadi,

Cédric FournetAuthors Info & Claims

Theoretical Computer Science, Volume 322, Issue 3

Pages 427 - 476

https://doi.org/10.1016/j.tcs.2003.12.023

Published: 06 September 2004 Publication History

Abstract

Frequently, communication between two principals reveals their identities and presence to third parties. These privacy breaches can occur even if security protocols are in use; indeed, they may even be caused by security protocols. However, with some care, security protocols can provide authentication for principals that wish to communicate while protecting them from monitoring by third parties. We discuss the problem of private authentication and present two protocols for private authentication of mobile principals. Our protocols allow two mobile principals to communicate when they meet at a location if they wish to do so, without the danger of tracking by third parties. We also present the analysis of one of the protocols in the applied pi calculus. We establish authenticity and secrecy properties. Although such properties are fairly standard, their formulation in the applied pi calculus makes an original use of process equivalences. In addition, we treat identity-protection properties, thus exploring a formal model of privacy.

References

[1]

{1} M. Abadi, Private authentication, in: Proc. Workshop on Privacy Enhancing Technologies (PET 2002), Lecture Notes in Computer Science, vol. 2482, Springer, Berlin, 2003, pp. 27-40.]]

Digital Library

Google Scholar

[2]

{2} M. Abadi, C. Fournet, Mobile values, new names, and secure communication, in: Proc. 28th ACM Symp. on Principles of Programming Languages (POPL 2001), ACM, New York, January 2001, pp. 104-115.]]

Digital Library

Google Scholar

[3]

{3} M. Abadi, C. Fournet, G. Gonthier, Authentication primitives and their compilation, in: Proc. 27th ACM Symp. on Principles of Programming Languages (POPL 2000), ACM, New York, January 2000, pp. 302-315.]]

Digital Library

Google Scholar

[4]

{4} M. Abadi, C. Fournet, G. Gonthier, Secure implementation of channel abstractions, Inform. and Comput. 174 (1) (2002) 37-83.]]

Digital Library

Google Scholar

[5]

{5} M. Abadi, A.D. Gordon, A calculus for cryptographic protocols: the spi calculus, Inform. and Comput. 148 (1) (1999) 1-70, An extended version appeared as Digital Equipment Corporation Systems Research Center Report No. 149, January 1998.]]

Digital Library

Google Scholar

[6]

{6} M. Abadi, R. Needham, Prudent engineering practice for cryptographic protocols, IEEE Trans. Software Engng. 22 (1) (1996) 6-15.]]

Digital Library

Google Scholar

[7]

{7} M. Abadi, P. Rogaway, Reconciling two views of cryptography (The computational soundness of formal encryption), in: Proc. 1st IFIP Internat. Conf. on Theoretical Computer Science, Lecture Notes in Computer Science, vol. 1872, Springer, Berlin, August 2000, pp. 3-22.]]

Digital Library

Google Scholar

[8]

{8} W. Aiello, S.M. Bellovin, M. Blaze, R. Canetti, J. Ionnidis, A.D. Keromytis, O. Reingold, Efficient, DoS-resistant, secure key exchange for internet protocols, in: V. Atluri (Ed.), Proc. 9th ACM Conf. on Computer and Communications Security (CCS 2002), ACM, New York, November 2002, pp. 48-58.]]

Digital Library

Google Scholar

[9]

{9} G. Ateniese, A. Herzberg, H. Krawczyk, G. Tsudik, On traveling incognito, Comput. Networks 31 (8) (1999) 871-884.]]

Digital Library

Google Scholar

[10]

{10} M. Bellare, A. Boldyreva, A. Desai, D. Pointcheval, Key-privacy in public-key encryption, in: C. Boyd (Ed.), Advances in Cryptology-ASIACRYPT 2001, Lecture Notes in Computer Science, vol. 2248, Springer, Berlin, 2001, pp. 566-582.]]

Digital Library

Google Scholar

[11]

{11} V. Bharghavan, C.V. Ramamoorthy, Security issues in mobile communications, in: Proc. 2nd Internat. Symp. on Autonomous Decentralized Systems, 1995, pp. 19-24.]]

Digital Library

Google Scholar

[12]

{12} Specification of the Bluetooth system (core, v1.0b), On the Web at http://www.bluetooth.com, December 1999.]]

Google Scholar

[13]

{13} J. Camenisch, A. Lysyanskaya, An efficient system for non-transferable anonymous credentials with optional anonymity revocation, in: B. Pfitzmann (Ed.), Advances in Cryptology-EUROCRYPT 2001, Lecture Notes in Computer Science, vol. 2045, Springer, Berlin, 2001, pp. 93-118.]]

Digital Library

Google Scholar

[14]

{14} L. Cardelli, Mobility and security, in: F.L. Bauer, R. Steinbrueggen (Eds.), Foundations of Secure Computation, NATO Science Series, IOS Press, Amsterdam, 2000, pp. 1-37, Vol. for the 20th Internat. Summer School on Foundations of Secure Computation, Marktoberdorf, Germany, 1999.]]

Google Scholar

[15]

{15} D. Chaum, Untraceable electronic mail, return addresses, and digital pseudonyms, Comm. ACM 24 (2) (1981) 84-88.]]

Digital Library

Google Scholar

[16]

{16} D.E. Denning, G.M. Sacco, Timestamps in key distribution protocols, Comm. ACM 24 (7) (1981) 533-535.]]

Digital Library

Google Scholar

[17]

{17} C. Ellison, B. Frantz, B. Lampson, R. Rivest, B. Thomas, T. Ylonen, SPKI certificate theory, On the Web at http ://www.ietf.cnri.reston.va.us/rfc/rfc2693, txt, September 1999.]]

Google Scholar

[18]

{18} H. Federrath, A. Jerichow, A. Pfitzmann, MIXes in mobile communication systems: location management with privacy, in: R.J. Anderson (Ed.), Information Hiding: First Internat. Workshop, Lecture Notes in Computer Science, vol. 1174, Springer, Berlin, 1996, pp. 121-135.]]

Digital Library

Google Scholar

[19]

{19} C. Fournet, M. Abadi, Hiding names: private authentication in the applied pi calculus, in: Software Security--Theories and Systems. Mext-NSF-JSPS Internat. Symp. (ISSS'02), Lecture Notes in Computer Science, vol. 2609, Springer, Berlin, 2003, pp. 317-338.]]

Digital Library

Google Scholar

[20]

{20} A.O. Freier, P. Karlton, P.C. Kocher, The SSL protocol: Version 3.0. Available at http://wp. netscape.com/eng/ssl3/, March 1996.]]

Google Scholar

[21]

{21} S. Goldwasser, S. Micali, Probabilistic encryption, J. Comput. System Sci. 28 (1984) 270-299.]]

Crossref

Google Scholar

[22]

{22} D. Hughes, V. Shmatikov, Information hiding, anonymity, and privacy: a modular approach, J. Comput. Security (2003), to appear.]]

Digital Library

Google Scholar

[23]

{23} M. Jakobsson, Privacy vs. authenticity, Ph.D. Thesis, University of California, San Diego, 1997.]]

Digital Library

Google Scholar

[24]

{24} M. Jakobsson, K. Sako, R. Impagliazzo, Designated verifier proofs and their applications, in: U. Maurer (Ed.), Advances in Cryptology-EUROCRYPT 96, Lecture Notes in Computer Science, vol. 1070, Springer, Berlin, 1996, pp. 143-154.]]

Digital Library

Google Scholar

[25]

{25} M. Jakobsson, S. Wetzel, Security weaknesses in Bluetooth, in: Topics in Cryptology-CT-RSA 2001, Proc. Cryptographer's Track at RSA Conf. 2001, Lecture Notes in Computer Science, vol. 2020, Springer, Berlin, 2001, pp. 176-191.]]

Digital Library

Google Scholar

[26]

{26} H. Krawczyk, SKEME: a versatile secure key exchange mechanism for internet, in: Proc. Internet Society Symp. on Network and Distributed Systems Security, February 1996, Available at http://bilbo.isu.edu/sndss/sndss96.html.]]

Digital Library

Google Scholar

[27]

{27} B. Lampson, M. Abadi, M. Burrows, E. Wobber, Authentication in distributed systems: theory and practice, ACM Trans. Comput. Systems 10 (4) (1992) 265-310.]]

Digital Library

Google Scholar

[28]

{28} A.K. Lenstra, E.R. Verheul, The XTR public key system, in: M. Bellare (Ed.), Advances in Cryptology --CRYPTO 2000, Lecture Notes in Computer Science, vol. 1880, Springer, Berlin, 2000, pp. 1-19.]]

Digital Library

Google Scholar

[29]

{29} A.J. Menezes, P.C. van Oorschot, S.A. Vanstone, Handbook of Applied Cryptography, CRC Press, Boca Raton, FL, 1996.]]

Digital Library

Google Scholar

[30]

{30} R. Molva, D. Samfat, G. Tsudik, Authentication of mobile users, IEEE Network 8 (2) (1994) 26-35.]]

Digital Library

Google Scholar

[31]

{31} R.M. Needham, M.D. Schroeder, Using encryption for authentication in large networks of computers, Comm. ACM 21 (12) (1978) 993-999.]]

Digital Library

Google Scholar

[32]

{32} A. Pfitzmann, M. Waidner, Networks without user observability, Comput. Security 6 (2) (1987) 158-166.]]

Digital Library

Google Scholar

[33]

{33} C. Rackoff, D.R. Simon, Cryptographic defense against traffic analysis, in: Proc. 25th Annu. ACM Symp. on the Theory of Computing, 1993, pp. 672-681.]]

Digital Library

Google Scholar

[34]

{34} M.G. Reed, P.F. Syverson, D.M. Goldschlag, Protocols using anonymous connections: mobile applications, in: B. Christianson, B. Crispo, M. Lomas, M. Roe (Eds.), Security Protocols: 5th Internat. Workshop, Lecture Notes in Computer Science, vol. 1361, Springer, Berlin, 1997, pp. 13-23.]]

Digital Library

Google Scholar

[35]

{35} R.L. Rivest, A. Shamir, Y. Tauman, How to leak a secret, in: C. Boyd (Ed.), Advances in Cryptology-ASIACRYPT 2001, Lecture Notes in Computer Science, vol. 2248, Springer, Berlin, 2001, pp. 552-565.]]

Digital Library

Google Scholar

[36]

{36} D. Samfat, R. Molva, N. Asokan, Untraceability in mobile networks, in: Proc. 1st Annu. Internat. Conf. on Mobile Computing and Networking (MobiCom 1995), 1995, pp. 26-36.]]

Digital Library

Google Scholar

[37]

{37} A. Shamir, Identity-based cryptosystems and signature schemes, in: G.R. Blakley, D. Chaum (Eds.), Advances in Cryptology--CRYPTO 84, Lecture Notes in Computer Science, vol. 196, Springer, Berlin, 1984, pp. 47-53.]]

Digital Library

Google Scholar

[38]

{38} V. Shmatikov, D. Hughes, Defining anonymity and privacy (extended abstract), in: Workshop on Issues in the Theory of Security (WITS' 02), January 2002.]]

Google Scholar

[39]

{39} A.C. Snoeren, H. Balakrishnan, An end-to-end approach to host mobility, in: Proc. 6th Annu. Internat. Conf. on Mobile Computing and Networking (MobiCom 2000), 2000, pp. 155-166.]]

Digital Library

Google Scholar

[40]

{40} Y. Zhang, W. Lee, Intrusion detection in wireless ad-hoc networks, in: Proc. 6th Annu. ACM/IEEE Internat. Conf. on Mobile Computing and Networking (MobiCom 2000), 2000, pp. 275-283.]]

Digital Library

Google Scholar

Cited By

View all

Horne RMauw SYurkov S(2023)When privacy fails, a formula describes an attackTheoretical Computer Science10.1016/j.tcs.2023.113842959:COnline publication date: 30-May-2023
https://dl.acm.org/doi/10.1016/j.tcs.2023.113842
Zhou QPandey OYe F(2022)An Approach for Multi-Level Visibility Scoping of IoT Services in Enterprise EnvironmentsIEEE Transactions on Mobile Computing10.1109/TMC.2020.301287521:2(408-420)Online publication date: 1-Feb-2022
https://dl.acm.org/doi/10.1109/TMC.2020.3012875
Mödersheim S(2022)Rewriting PrivacyRewriting Logic and Its Applications10.1007/978-3-031-12441-9_2(22-41)Online publication date: 2-Apr-2022
https://dl.acm.org/doi/10.1007/978-3-031-12441-9_2
Show More Cited By

Recommendations

Private authentication
PET'02: Proceedings of the 2nd international conference on Privacy enhancing technologies

Frequently, communication between two principals reveals their identities and presence to third parties. These privacy breaches can occur even if security protocols are in use; indeed, they may even be caused by security protocols. However, with some ...
Unconditionally secure disjointness tests for private datasets

We present two unconditional secure protocols for private set disjointness tests. In order to provide intuition of our protocols, we give a naive example that applies Sylvester matrices. Unfortunately, this simple construction is insecure as it reveals ...
Authentication for paranoids: multi-party secret handshakes
ACNS'06: Proceedings of the 4th international conference on Applied Cryptography and Network Security

In a society increasingly concerned with the steady assault on electronic privacy, the need for privacy-preserving techniques is both natural and justified. This need extends to traditional security tools such as authentication and key distribution ...

Reviews

Reviewer: Adrian Constantin Atanasiu

This paper focuses on the privacy of communication between two or more mobile interlocutors (principals), and protecting their messages and their identities from third parties (a situation that can arise in mobile telephony and mobile computing). The protection is considered to be against an active adversary (as in security described by Needham-Schroder protocols). Abadi and Fournet provide a definition of a privacy property (first informally, then in a process calculus). This property implies that each principal may reveal and prove its identity to certain other principals, and hide it from the rest. The main contribution of the paper consists of the construction of two protocols that allow the principals to authenticate with chosen interlocutors, while hiding their identities from others. The paper spans 50 pages. The first section is a general overview of the subject. Section 2 defines and discusses the privacy properties defined by the authors. Section 3 presents the general assumptions on which the protocols rely. Section 4 develops two protocols, and some optimizations and extensions. The first protocol uses digital signatures, and requires that principals have loosely synchronized clocks. It is based on the Denning-Sacco public key protocol [1], and its corrected version [2]. The second protocol uses only encryption, and avoids the synchronization requirements, at the cost of an extra message. Section 5 explains the applied pi calculus (an extension of pi calculus), and gives some examples. Section 6 constructs a formal model of the second protocol using the applied pi calculus. Section 7 addresses (in two theorems) the authenticity and secrecy properties of this model of the second protocol. In section 8, the theoretical analysis is concentrated on privacy properties. The results show that the standard authenticity, secrecy, and privacy (identity protection) properties are covered by the protocol. Some applications of this identity protection are developed in subsection 8.3. Section 9 discusses some related problems and related work (including, in particular, work on message untraceability). Section 10 concludes the paper. An appendix contains proofs for the main claims of sections 7 and 8. The paper is considered by the authors to be a contribution to the formal study of security protocols and of their properties. Online Computing Reviews Service

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Publisher

Elsevier Science Publishers Ltd.

United Kingdom

Publication History

Published: 06 September 2004

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

45
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

View all

Horne RMauw SYurkov S(2023)When privacy fails, a formula describes an attackTheoretical Computer Science10.1016/j.tcs.2023.113842959:COnline publication date: 30-May-2023
https://dl.acm.org/doi/10.1016/j.tcs.2023.113842
Zhou QPandey OYe F(2022)An Approach for Multi-Level Visibility Scoping of IoT Services in Enterprise EnvironmentsIEEE Transactions on Mobile Computing10.1109/TMC.2020.301287521:2(408-420)Online publication date: 1-Feb-2022
https://dl.acm.org/doi/10.1109/TMC.2020.3012875
Mödersheim S(2022)Rewriting PrivacyRewriting Logic and Its Applications10.1007/978-3-031-12441-9_2(22-41)Online publication date: 2-Apr-2022
https://dl.acm.org/doi/10.1007/978-3-031-12441-9_2
Fernet LMödersheim S(2021)Deciding a Fragment of -PrivacySecurity and Trust Management10.1007/978-3-030-91859-0_7(122-142)Online publication date: 8-Oct-2021
https://dl.acm.org/doi/10.1007/978-3-030-91859-0_7
Horne RMauw SYurkov S(2021)Compositional Analysis of Protocol Equivalence in the Applied -Calculus Using Quasi-open BisimilarityTheoretical Aspects of Computing – ICTAC 202110.1007/978-3-030-85315-0_14(235-255)Online publication date: 6-Sep-2021
https://dl.acm.org/doi/10.1007/978-3-030-85315-0_14
Babel KCheval VKremer S(2020)On the semantics of communications when verifying equivalence propertiesJournal of Computer Security10.3233/JCS-19136628:1(71-127)Online publication date: 1-Jan-2020
https://dl.acm.org/doi/10.3233/JCS-191366
Mödersheim SViganò L(2019)Alpha-Beta PrivacyACM Transactions on Privacy and Security10.1145/328925522:1(1-35)Online publication date: 22-Jan-2019
https://dl.acm.org/doi/10.1145/3289255
Horne RAhn KLin STiu A(2018)Quasi-Open Bisimilarity with Mismatch is IntuitionisticProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3209108.3209125(26-35)Online publication date: 9-Jul-2018
https://dl.acm.org/doi/10.1145/3209108.3209125
Baelde DDelaune SHirschi L(2018)POR for Security Protocol EquivalencesComputer Security10.1007/978-3-319-99073-6_19(385-405)Online publication date: 3-Sep-2018
https://dl.acm.org/doi/10.1007/978-3-319-99073-6_19
Cortier VGrimm NLallemand JMaffei MThuraisingham BEvans DMalkin TXu D(2017)A Type System for Privacy PropertiesProceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security10.1145/3133956.3133998(409-423)Online publication date: 30-Oct-2017
https://dl.acm.org/doi/10.1145/3133956.3133998
Show More Cited By

View Options

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.

Cited By

Index Terms

Recommendations