Minimal backups of cryptographic protocol runs

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Minimal backups of cryptographic protocol runs

Full text

Pdf (470 KB)

Source

Conference on Computer and Communications Security archive
Proceedings of the 6th ACM workshop on Formal methods in security engineering table of contents

Alexandria, Virginia, USA

Pages 11-20

Year of Publication: 2008

ISBN:978-1-60558-288-7

Authors

Jay A. McCarthy	Brigham Young University, Provo, UT, USA
Shriram Krishnamurthi	Brown University, Providence, RI, USA

Sponsors

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

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 2, Downloads (12 Months): 46, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Request Permissions 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/1456396.1456398 What is a DOI?

ABSTRACT

As cryptographic protocols execute they accumulate information such as values and keys, and evidence of properties about this information. As execution proceeds, new information becomes relevant while some old information ceases to be of use. Identifying what information is necessary at each point in a protocol run is valuable for both analysis and deployment.

We formalize this necessary information as the minimal backup of a protocol. We present an analysis that determines the minimal backup at each point in a protocol run. We show that this minimal backup has many uses: it serves as a foundation for job-migration and other kinds of fault-tolerance, and also assists protocol designers understand the structure of protocols and identify potential flaws.

In a cryptographic context it is dangerous to reason informally. We have therefore formalized and verified this work using the Coq proof assistant. Additionally, Coq provides a certified implementation of our analysis. Concretely, our analysis and its implementation consume protocols written in a variant of the Cryptographic Protocol Programming Language, CPPL.

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	M. Burrows, M. Abadi, and R. Needham. A logic of authentication. Proceedings of the Royal Society, Series A, 426(1871):233--271, December 1989.
	2	Dorothy E. Denning , Giovanni Maria Sacco, Timestamps in key distribution protocols, Communications of the ACM, v.24 n.8, p.533-536, Aug. 1981 [doi>10.1145/358722.358740]
	3	D. Dolev and A. Yao. On the security of public-key protocols. IEEE Transactions on Information Theory, 29:198--208, 1983.
	4	Fred Douglis , John Ousterhout, Transparent process migration: design alternatives and the sprite implementation, Software—Practice & Experience, v.21 n.8, p.757-785, Aug. 1991 [doi>10.1002/spe.4380210802]
	5	L. Gong. Increasing availability and security of an authentication service. IEEE Journal on Selected Areas in Communications, 11(5):657--662, 1993.
	6	J. D. Guttman, J. C. Herzog, J. D. Ramsdell, and B. T. Sniffen. Programming cryptographic protocols. In Trust in Global Computing, 2005.
	7	Joshua D. Guttman , F. Javier Thayer, Authentication tests and the structure of bundles, Theoretical Computer Science, v.283 n.2, p.333-380, June 14, 2002 [doi>10.1016/S0304-3975(01)00139-6]
	8	J. D. Guttman, F. J. Thayer, J. A. Carlson, J. C. Herzog, J. D. Ramsdell, and B. T. Sniffen. Trust management in strand spaces: A rely-guarantee method. In European Symposium on Programming, 2004.
	9	Ping Ji , Zihui Ge , Jim Kurose , Don Towsley, A comparison of hard-state and soft-state signaling protocols, Proceedings of the 2003 conference on Applications, technologies, architectures, and protocols for computer communications, August 25-29, 2003, Karlsruhe, Germany [doi>10.1145/863955.863984]
	10	Gary A. Kildall, A unified approach to global program optimization, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.194-206, October 01-03, 1973, Boston, Massachusetts [doi>10.1145/512927.512945]
	11	Chung-Chi Jim Li , Elliot M. Stewart , W. Kent Fuchs, Compiler-assisted full checkpointing, Software—Practice & Experience, v.24 n.10, p.871-886, Oct. 1994 [doi>10.1002/spe.4380241002]
	12	Benjamin C. Ling , Emre Kiciman , Armando Fox, Session state: beyond soft state, Proceedings of the 1st conference on Symposium on Networked Systems Design and Implementation, p.22-22, March 29-31, 2004, San Francisco, California
	13	G. Lowe. A family of attacks upon authentication protocols. Department of Mathematics and Computer Science 5, University of Leicester, 1997.
	14	M. Marwah, S. Mishra, and C. Fetzer. Tcp server fault tolerance using connection migration to a backup server. In Dependable Systems and Networks, 2003.
	15	Project EVA. Security protocols open repository. http://www.lsv.ens-cachan.fr/spore/, 2007.
	16	Suchitra Raman , Steven McCanne, A model, analysis, and protocol framework for soft state-based communication, Proceedings of the conference on Applications, technologies, architectures, and protocols for computer communication, p.15-25, August 30-September 03, 1999, Cambridge, Massachusetts, United States
	17	Michael K. Reiter , Kenneth P. Birman, How to securely replicate services, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.986-1009, May 1994 [doi>10.1145/177492.177745]
	18	Michael K. Reiter , Kenneth P. Birman , Robbert van Renesse, A security architecture for fault-tolerant systems, ACM Transactions on Computer Systems (TOCS), v.12 n.4, p.340-371, Nov. 1994 [doi>10.1145/195792.195823]
	19	M. Satyanarayanan, Integrating security in a large distributed system, ACM Transactions on Computer Systems (TOCS), v.7 n.3, p.247-280, Aug. 1989 [doi>10.1145/65000.65002]
	20	Florin Sultan , Kiran Srinivasan , Deepa Iyer , Liviu Iftode, Migratory TCP: Connection Migration for Service Continuity in the Internet, Proceedings of the 22 nd International Conference on Distributed Computing Systems (ICDCS'02), p.469, July 02-05, 2002
	21	F. Javier Thayer Fábrega, Strand spaces: proving security protocols correct, Journal of Computer Security, v.7 n.2-3, p.191-230, Jan. 1999
	22	F. J. Thayer Fábrega, J. C. Herzog, and J. D. Guttman. Strand spaces: Why is a security protocol correct? In 1998 IEEE Symposium on Security and Privacy. IEEE Computer Society Press, May 1998.
	23	The Coq development team. The Coq proof assistant reference manual, 8.1 edition, 2007.
	24	D. Williams and H. Lutfiyya. Fault-tolerant authentication services. International Journal of Computers and Applications, 2007.