Type-checking zero-knowledge

ABSTRACT

This paper presents the first type system for statically analyzing security protocols that are based on zero-knowledge proofs. We show how certain properties offered by zero-knowledge proofs can be characterized in terms of authorization policies and statically enforced by a type system. The analysis is modular and compositional, and provides security proofs for an unbounded number of protocol executions. We develop a new type-checker that conducts the analysis in a fully automated manner. We exemplify the applicability of our technique to real-world protocols by verifying the authenticity and secrecy properties of the Direct Anonymous Attestation (DAA) protocol. The analysis of DAA takes less than three seconds.

REFERENCES

• 1: Martín Abadi, Secrecy by typing in security protocols, Journal of the ACM (JACM), v.46 n.5, p.749-786, Sept. 1999 [doi>10.1145/324133.324266]
• 2: Martín Abadi, Logic in Access Control, Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science, p.228, June 22-25, 2003
• 3: Martín Abadi , Bruno Blanchet, Secrecy Types for Asymmetric Communication, Proceedings of the 4th International Conference on Foundations of Software Science and Computation Structures, p.25-41, April 02-06, 2001
• 4: Martín Abadi , Bruno Blanchet, Analyzing security protocols with secrecy types and logic programs, Journal of the ACM (JACM), v.52 n.1, p.102-146, January 2005 [doi>10.1145/1044731.1044735]
• 5: Bruno Blanchet , Cedric Fournet, Automated Verification of Selected Equivalences for Security Protocols, Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, p.331-340, June 26-29, 2005 [doi>10.1109/LICS.2005.8]
• 6: A. Acquisti. Receipt-free homomorphic elections and write-in ballots. Cryptology ePrint Archive, Report 2004/105, 2004. http://eprint.iacr.org/.
• 7: L. Bachmair and H. Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):217--247, 1994.
• 8: Michael Backes , Agostino Cortesi , Riccardo Focardi , Matteo Maffei, A calculus of challenges and responses, Proceedings of the 2007 ACM workshop on Formal methods in security engineering, p.51-60, November 02-02, 2007, Fairfax, Virginia, USA [doi>10.1145/1314436.1314444]
• 9: Michael Backes , Catalin Hritcu , Matteo Maffei, Automated Verification of Remote Electronic Voting Protocols in the Applied Pi-Calculus, Proceedings of the 2008 21st IEEE Computer Security Foundations Symposium, p.195-209, June 23-25, 2008 [doi>10.1109/CSF.2008.26]
• 10: Michael Backes , Cǎtǎlin Hritcu , Matteo Maffei, Type-checking zero-knowledge, Proceedings of the 15th ACM conference on Computer and communications security, October 27-31, 2008, Alexandria, Virginia, USA [doi>10.1145/1455770.1455816]
• 11: Michael Backes , Cǎtǎlin Hritcu , Matteo Maffei, Type-checking zero-knowledge, Proceedings of the 15th ACM conference on Computer and communications security, October 27-31, 2008, Alexandria, Virginia, USA [doi>10.1145/1455770.1455816]
• 12: Michael Backes , Matteo Maffei , Dominique Unruh, Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the Direct Anonymous Attestation Protocol, Proceedings of the 2008 IEEE Symposium on Security and Privacy (sp 2008), p.202-215, May 18-21, 2008 [doi>10.1109/SP.2008.23]
• 13: Michael Backes , Dominique Unruh, Computational Soundness of Symbolic Zero-Knowledge Proofs Against Active Attackers, Proceedings of the 2008 21st IEEE Computer Security Foundations Symposium, p.255-269, June 23-25, 2008 [doi>10.1109/CSF.2008.20]
• 14: Jesper Bengtson , Karthikeyan Bhargavan , Cédric Fournet , Andrew D. Gordon , Sergio Maffeis, Refinement Types for Secure Implementations, Proceedings of the 2008 21st IEEE Computer Security Foundations Symposium, p.17-32, June 23-25, 2008 [doi>10.1109/CSF.2008.27]
• 15: Bruno Blanchet, An Efficient Cryptographic Protocol Verifier Based on Prolog Rules, Proceedings of the 14th IEEE workshop on Computer Security Foundations, p.82, June 11-13, 2001
• 16: Daniel Bleichenbacher, Chosen Ciphertext Attacks Against Protocols Based on the RSA Encryption Standard PKCS #1, Proceedings of the 18th Annual International Cryptology Conference on Advances in Cryptology, p.1-12, August 23-27, 1998
• 17: Ernie Brickell , Jan Camenisch , Liqun Chen, Direct anonymous attestation, Proceedings of the 11th ACM conference on Computer and communications security, October 25-29, 2004, Washington DC, USA [doi>10.1145/1030083.1030103]
• 18: Michele Bugliesi , Riccardo Focardi , Matteo Maffei, Dynamic types for authentication, Journal of Computer Security, v.15 n.6, p.563-617, December 2007
• 19: Frederick Butler , Iliano Cervesato , Aaron D. Jaggard , Andre Scedrov , Christopher Walstad, Formal analysis of Kerberos 5, Theoretical Computer Science, v.367 n.1, p.57-87, 24 November 2006 [doi>10.1016/j.tcs.2006.08.040]
• 20: D. Chaum. Blind signatures for untraceable payments. In Advances in Cryptology: CRYPTO'82, pages 199--203, 1983.
• 21: Michael R. Clarkson , Stephen Chong , Andrew C. Myers, Civitas: Toward a Secure Voting System, Proceedings of the 2008 IEEE Symposium on Security and Privacy (sp 2008), p.354-368, May 18-21, 2008 [doi>10.1109/SP.2008.32]
• 22: Ricardo Corin , Pierre-Malo Denielou , Cedric Fournet , Karthikeyan Bhargavan , James Leifer, Secure Implementations for Typed Session Abstractions, Proceedings of the 20th IEEE Computer Security Foundations Symposium, p.170-186, July 06-08, 2007 [doi>10.1109/CSF.2007.29]
• 23: Stephanie Delaune , Steve Kremer , Mark Ryan, Coercion-Resistance and Receipt-Freeness in Electronic Voting, Proceedings of the 19th IEEE workshop on Computer Security Foundations, p.28-42, July 05-07, 2006 [doi>10.1109/CSFW.2006.8]
• 24: S. Delaune, M. Ryan, and B. Smyth. Automatic verification of privacy properties in the applied pi calculus. To appear in 2nd Joint iTrust and PST Conferences on Privacy, Trust Management and Security (IFIPTM'08), 2008.
• 25: Boris Dragovic , Evangelos Kotsovinos , Steven Hand , Peter R. Pietzuch, XenoTrust: Event-based distributed trust management, Proceedings of the 14th International Workshop on Database and Expert Systems Applications, p.410, September 01-05, 2003
• 26: D. Fisher. Millions of .Net Passport accounts put at risk. eWeek, May 2003. (Flaw detected by Muhammad Faisal Rauf Danka).
• 27: C. Fournet, A.D. Gordon, and S. Maffeis. A type discipline for authorization policies. In Proc. 14th European Symposium on Programming (ESOP), Lecture Notes in Computer Science, pages 141--156. Springer-Verlag, 2005.
• 28: Cedric Fournet , Andrew Gordon , Sergio Maffeis, A Type Discipline for Authorization in Distributed Systems, Proceedings of the 20th IEEE Computer Security Foundations Symposium, p.31-48, July 06-08, 2007 [doi>10.1109/CSF.2007.7]
• 29: Oded Goldreich, Foundations of Cryptography: Basic Tools, Cambridge University Press, New York, NY, 2000
• 30: Andrew D. Gordon , Alan Jeffrey, Authenticity by typing for security protocols, Journal of Computer Security, v.11 n.4, p.451-519, July 2003
• 31: Andrew D. Gordon , Alan Jeffrey, Types and effects for asymmetric cryptographic protocols, Journal of Computer Security, v.12 n.3,4, p.435-483, May 2004
• 32: Andrew D. Gordon , Alan Jeffrey, Secrecy despite compromise: types, cryptography, and the pi-calculus, CONCUR 2005 - Concurrency Theory, Springer-Verlag, London, 2005 [doi>10.1007/11539452_17]
• 33: Christian Haack , Alan Jeffrey, Timed spi-calculus with types for secrecy and authenticity, CONCUR 2005 - Concurrency Theory, Springer-Verlag, London, 2005 [doi>10.1007/11539452_18]
• 34: Christian Haack , Alan Jeffrey, Pattern-matching spi-calculus, Information and Computation, v.204 n.8, p.1195-1263, August 2006 [doi>10.1016/j.ic.2006.04.004]
• 35: Ari Juels , Dario Catalano , Markus Jakobsson, Coercion-resistant electronic elections, Proceedings of the 2005 ACM workshop on Privacy in the electronic society, November 07-07, 2005, Alexandria, VA, USA [doi>10.1145/1102199.1102213]
• 36: Sepandar D. Kamvar , Mario T. Schlosser , Hector Garcia-Molina, The Eigentrust algorithm for reputation management in P2P networks, Proceedings of the 12th international conference on World Wide Web, May 20-24, 2003, Budapest, Hungary [doi>10.1145/775152.775242]
• 37: L. Lu, J. Han, L. Hu, J. Huai, Y. Liu, and L.M. Ni. Pseudo trust: Zero-knowledge based authentication in anonymous peer-to-peer protocols. In Proc. 2007 IEEE International Parallel and Distributed Processing Symposium, page 94. IEEE Computer Society Press, 2007.
• 38: David Wagner , Bruce Schneier, Analysis of the SSL 3.0 protocol, Proceedings of the 2nd conference on Proceedings of the Second USENIX Workshop on Electronic Commerce, p.4-4, November 18-21, 1996, Oakland, California
• 39: Christoph Weidenbach , Renate A. Schmidt , Thomas Hillenbrand , Rostislav Rusev , Dalibor Topic, System Description: Spass Version 3.0, Proceedings of the 21st international conference on Automated Deduction: Automated Deduction, July 17-20, 2007, Bremen, Germany [doi>10.1007/978-3-540-73595-3_38]

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.2 Network Protocols
          Subjects: Protocol verification

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

General Terms:
Security, Theory, Verification

Keywords:
authorization policies, language-based security, type systems, zero-knowledge protocols