Secrecy types for a simulatable cryptographic library

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Secrecy types for a simulatable cryptographic library

Full text

Pdf (206 KB)

Source

Conference on Computer and Communications Security archive
Proceedings of the 12th ACM conference on Computer and communications security table of contents

Alexandria, VA, USA

SESSION: Formal analysis of crypto protocols table of contents

Pages: 26 - 35

Year of Publication: 2005

ISBN:1-59593-226-7

Author

Peeter Laud

Tartu University, Tartu, Estonia

Sponsors

SIGSAC: ACM Special Interest Group on Security, Audit, and Control
ACM: Association for Computing Machinery

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 16, Downloads (12 Months): 69, Citation Count: 5

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Review this Article Save this Article to a Binder Display Formats: BibTex EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1102120.1102126 What is a DOI?

ABSTRACT

We present a type system for checking secrecy of messages handled by protocols that use the Backes-Pfitzmann-Waidner library for cryptographic operations. A secure realization of this library exists, therefore we obtain for the first time a cryptographically sound analysis for a full language for expressing protocols, particularly handling symmetric encryption and unbounded number of sessions. The language is similar to the spi-calculus, but has a completely deterministic semantics. The type system is similar to the Abadi-Blanchet type system for asymmetric communication.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked 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 , Bruno Blanchet, Secrecy types for asymmetric communication, Theoretical Computer Science, v.298 n.3, p.387-415, 11 April 2003 [doi>10.1016/S0304-3975(02)00863-0]
	3	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]
	4	Martín Abadi , Andrew D. Gordon, A calculus for cryptographic protocols, Information and Computation, v.148 n.1, p.1-70, Jan. 10, 1999 [doi>10.1006/inco.1998.2740 ]
	5	Martín Abadi , Jan Jürjens, Formal Eavesdropping and Its Computational Interpretation, Proceedings of the 4th International Symposium on Theoretical Aspects of Computer Software, p.82-94, October 29-31, 2001
	6	Martín Abadi , Phillip Rogaway, Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption), Proceedings of the International Conference IFIP on Theoretical Computer Science, Exploring New Frontiers of Theoretical Informatics, p.3-22, August 17-19, 2000
	7	M. Backes. A Cryptographically Sound Dolev-Yao Style Security Proof of the Otway-Rees Protocol. In proc. of ESORICS 2004 (LNCS 3193) pages 89--108.
	8	M. Backes and B. Pfitzmann. A Cryptographically Sound Security Proof of the Needham-Schroeder-Lowe Public-Key Protocol. In proc. of FST TCS 2003 (LNCS 2914), pages 1--12.
	9	Michael Backes , Birgit Pfitzmann, Symmetric Encryption in a Simulatable Dolev-Yao Style Cryptographic Library, Proceedings of the 17th IEEE Computer Security Foundations Workshop (CSFW'04), p.204, June 28-30, 2004 [doi>10.1109/CSFW.2004.20]
	10	Michael Backes , Birgit Pfitzmann, Relating Symbolic and Cryptographic Secrecy, Proceedings of the 2005 IEEE Symposium on Security and Privacy, p.171-182, May 08-11, 2005 [doi>10.1109/SP.2005.17]
	11	M. Backes, B. Pfitzmann, and M. Waidner. Symmetric authentication within a simulatable cryptographic library. In proc. of ESORICS 2003 (LNCS 2808), pages 271--290.
	12	Michael Backes , Birgit Pfitzmann , Michael Waidner, A composable cryptographic library with nested operations, Proceedings of the 10th ACM conference on Computer and communications security, October 27-30, 2003, Washington D.C., USA [doi>10.1145/948109.948140]
	13	Mihir Bellare , Anand Desai , Eron Jokipii , Phillip Rogaway, A Concrete Security Treatment of Symmetric Encryption, Proceedings of the 38th Annual Symposium on Foundations of Computer Science (FOCS '97), p.394, October 19-22, 1997
	14	Mihir Bellare , Anand Desai , David Pointcheval , Phillip Rogaway, Relations Among Notions of Security for Public-Key Encryption Schemes, Proceedings of the 18th Annual International Cryptology Conference on Advances in Cryptology, p.26-45, August 23-27, 1998
	15	B. Blanchet. Automatic Proof of Strong Secrecy for Security Protocols. In proc. of IEEE S&P 2004, pages 86--100.
	16	R. Canetti, Universally Composable Security: A New Paradigm for Cryptographic Protocols, Proceedings of the 42nd IEEE symposium on Foundations of Computer Science, p.136, October 14-17, 2001
	17	Ran Canetti , Marc Fischlin, Universally Composable Commitments, Proceedings of the 21st Annual International Cryptology Conference on Advances in Cryptology, p.19-40, August 19-23, 2001
	18	R. Canetti and J. Herzog. Universally Composable Symbolic Analysis of Cryptographic Protocols (The case of encryption-based mutual authentication and key exchange). Cryptology ePrint Archive: Report 2004/334, 22 Feb. 2005.
	19	Ran Canetti , Hugo Krawczyk, Universally Composable Notions of Key Exchange and Secure Channels, Proceedings of the International Conference on the Theory and Applications of Cryptographic Techniques: Advances in Cryptology, p.337-351, May 02, 2002
	20	Ran Canetti , Yehuda Lindell , Rafail Ostrovsky , Amit Sahai, Universally composable two-party and multi-party secure computation, Proceedings of the thiry-fourth annual ACM symposium on Theory of computing, May 19-21, 2002, Montreal, Quebec, Canada [doi>10.1145/509907.509980]
	21	V. Cortier and B. Warinschi. Computationally Sound, Automated Proofs for Security Protocols. In proc. of ESOP 2005 (LNCS 3444), pages 157--171.
	22	D. Dolev and A. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, IT-29(12):198--208, Mar. 1983.
	23	Oded Goldreich, Foundations of Cryptography: Basic Tools, Cambridge University Press, New York, NY, 2000
	24	S. Goldwasser and S. Micali. Probabilistic Encryption. Journal of Computer and System Sciences, 28(2):270--299, Apr. 1984.
	25	Andrew D. Gordon , Alan Jeffrey, Authenticity by typing for security protocols, Journal of Computer Security, v.11 n.4, p.451-519, 01/01/2004
	26	Andrew D. Gordon , Alan Jeffrey, Typing correspondence assertions for communication protocols, Theoretical Computer Science, v.300 n.1-3, p.379-409, 07 May 2003 [doi>10.1016/S0304-3975(02)00333-X]
	27	A. D. Gordon and A. Jeffrey. Types and effects for asymmetric cryptographic protocols. Journal of Computer Security, 12(3-4):435--483, 2004.
	28	Joshua D. Guttman , F. Javier Thayer , Lenore D. Zuck, The faithfulness of abstract protocol analysis: message authentication, Proceedings of the 8th ACM conference on Computer and Communications Security, November 05-08, 2001, Philadelphia, PA, USA [doi>10.1145/501983.502009]
	29	J. Herzog, M. Liskov, and S. Micali. Plaintext Awareness via Key Registration. In proc. of CRYPTO 2003 (LNCS 2729), pages 548--564.
	30	R. Janvier, Y. Lakhnech, and L. Mazar'e. Completing the Picture: Soundness of Formal Encryption in the Presence of Active Adversaries. In proc. of ESOP 2005 (LNCS 3444), pages 172--185.
	31	R. Janvier, Y. Lakhnech, and L. Mazar'e. (De)Compositions of Cryptographic Schemes and their Applications to Protocols. Cryptology ePrint Archive, Report 2005/020, 1 Feb. 2005.
	32	P. Laud. Handling Encryption in Analyses for Secure Information Flow. In proc. of ESOP 2003 (LNCS 2618), pages 159--173.
	33	P. Laud. Symmetric encryption in automatic analyses for confidentiality against active adversaries. In proc. of IEEE S&P 2004, pages 71--85.
	34	P. Laud. Secrecy Types for a Simulatable Cryptographic Library. Research Report IT-LU-O-162-050823, Cybernetica, Aug. 2005.
	35	P. Laud and V. Vene. A Type System for Computationally Secure Information Flow. In proc. of FCT 2005 (LNCS 3623), pages 365--377.
	36	P. Lincoln , J. Mitchell , M. Mitchell , A. Scedrov, A probabilistic poly-time framework for protocol analysis, Proceedings of the 5th ACM conference on Computer and communications security, p.112-121, November 02-05, 1998, San Francisco, California, United States [doi>10.1145/288090.288117]
	37	Patrick Lincoln , John C. Mitchell , Mark Mitchell , Andre Scedrov, Probabilistic Polynomial-Time Equivalence and Security Analysis, Proceedings of the Wold Congress on Formal Methods in the Development of Computing Systems-Volume I, p.776-793, September 20-24, 1999
	38	Gavin Lowe, Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR, Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.147-166, March 27-29, 1996
	39	C. Meadows. Formal Methods for Cryptographic Protocol Analysis: Emerging Issues and Trends. IEEE Journal on Selected Areas in Communication, 21(1):44--54, Jan. 2003.
	40	D. Micciancio and S. Panjwani. Adaptive Security of Symbolic Encryption. In proc. of TCC 2005 (LNCS 3378), pages 169--187.
	41	D. Micciancio and B. Warinschi. Completeness theorems for the Abadi-Rogaway logic of encrypted expressions. In Workshop on Issues in the Theory of Security - WITS 2002, Portland, Oregon, Jan. 2002.
	42	D. Micciancio and B. Warinschi. Soundness of Formal Encryption in the Presence of Active Adversaries. In proc. TCC 2004 (LNCS 2951), pages 133-151.
	43	Roger M. Needham , Michael D. Schroeder, Using encryption for authentication in large networks of computers, Communications of the ACM, v.21 n.12, p.993-999, Dec. 1978 [doi>10.1145/359657.359659]
	44	Birgit Pfitzmann , Michael Waidner, A Model for Asynchronous Reactive Systems and its Application to Secure Message Transmission, Proceedings of the 2001 IEEE Symposium on Security and Privacy, p.184, May 14-16, 2001
	45	Charles Rackoff , Daniel R. Simon, Non-Interactive Zero-Knowledge Proof of Knowledge and Chosen Ciphertext Attack, Proceedings of the 11th Annual International Cryptology Conference on Advances in Cryptology, p.433-444, August 11-15, 1991
	46	A. Ramanathan, J. C. Mitchell, A. Scedrov, and V. Teague. Probabilistic Bisimulation and Equivalence for Security Analysis of Network Protocols. In proc. of FOSSACS 2004 (LNCS 2987), pages 468--483.
	47	A. Yao. Theory and applications of trapdoor functions (extended abstract). In proc. of FOCS '82, pages 80--91.
	48	R. Zunino and P. Degano. A Note on the Perfect Encryption Assumption in a Process Calculus. In proc. of FOSSACS 2004 (LNCS 2987), pages 514--528.

CITED BY 5

	Cédric Fournet , Tamara Rezk, Cryptographically sound implementations for typed information-flow security, ACM SIGPLAN Notices, v.43 n.1, January 2008
	Geoffrey Smith, Secure information flow with random assignment and encryption, Proceedings of the fourth ACM workshop on Formal methods in security, p.33-44, November 03-03, 2006, Alexandria, Virginia, USA
	B. Blanchet , A. D. Jaggard , A. Scedrov , J.-K. Tsay, Computationally sound mechanized proofs for basic and public-key Kerberos, Proceedings of the 2008 ACM symposium on Information, computer and communications security, March 18-20, 2008, Tokyo, Japan
	Tri Van Le , Mike Burmester , Breno de Medeiros, Universally composable and forward-secure RFID authentication and authenticated key exchange, Proceedings of the 2nd ACM symposium on Information, computer and communications security, March 20-22, 2007, Singapore
	Michael Backes , Peeter Laud, Computationally sound secrecy proofs by mechanized flow analysis, Proceedings of the 13th ACM conference on Computer and communications security, October 30-November 03, 2006, Alexandria, Virginia, USA