This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Model for Secure Protocols and Their Compositions
January 1996 (vol. 22 no. 1)
pp. 16-30

Abstract—This paper develops a foundation for reasoning about protocol security. We adopt a model-based approach for defining protocol security properties. This allows us to describe security properties in greater detail and precision than previous frameworks. Our model allows us to reason about the security of protocols, and considers issues of beliefs of agents, time, and secrecy. We prove a composition theorem which allows us to state sufficient conditions on two secure protocols A and B such that they may be combined to form a new secure protocol C. Moreover, we give counter-examples to show that when the conditions are not met, the protocol C may not be secure.

[1] M. Abadi, "The power of temporal proofs," Proc. Second IEEE Symp. Logic in Computer Science, pp. 123-130, June 1987.
[2] M. Abadi and M. Tuttle, "A semantics for a logic of authentication," Proc. of ACM Symp. Principles of Distributed Computing, Aug. 1991.
[3] J. van Benthem, "Time, logic and computation," Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, eds., Springer-Verlag, pp. 1-49, June 1988.
[4] P. Bieber, "A logic of communication in hostile environment," Proc. IEEE Computer Security Foundations Workshop III, pp. 14-22,Los Alamitos, Calif., June 1990.
[5] R. Bird, I. Gobal, A. Herzberg, P.A. Janson, S. Kutten, R. Molva, and C.M. Yung, "Systematic design of a family of attack-resistant authentication protocols," J. Selected Areas in Comm., vol. 11, no. 5, pp. 679-693, June 1993.
[6] M. Blum and S. Goldwasser, "An efficient probabilistic public-key encryption scheme which hides all partial information," Advances in Cryptology: Proc. of CRYPTO'84, Springer-Verlag LNCS no. 196, 1984.
[7] J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang., "Symbolic model checking: 1020states and beyond," Information and Computation, vol. 98, no. 2, pp. 142-170, June 1992.
[8] E.M. Clarke and E.A. Emerson, "Synthesis of synchronization skeletons for branching time temporal logic," Logic of Programs: Workshop, Lecture notes in Computer Science. vol. 131. Yorktown Heights, N. Y.: Springer-Verlag, May 1981.
[9] E.M. Clarke, E.A. Emerson, and A.P. Sistla, "Automatic verification of finite-state concurrent systems using temporal logic specifications," ACM Trans. Programming Languages and Systems, vol. 8, no. 2, pp. 244-263, 1986.
[10] J. Burgess, "Basic tense logic," Handbook of Philosophical Logic, Volume II: Extensions of Classical Logic, E. Gabbay and F. Guenthner, eds., pp. 89-133. Kluwer Academic Publishers, 1986.
[11] M. Burrows, M. Abadi, and R. Needham, "A logic of authentication," ACM Trans. Computer Systems, vol. 8, no. 1, pp. 18-36, Feb. 1990. Also see Research Report no. 39, DEC SRC, 48 pp., 1989.
[12] D. Dolev and A. C. Yao, "On the security of public key protocols," IEEE Trans. Information Theory, vol. 29, no. 2, Mar. 1983. Also appears in the 22nd FOCS, 1981.
[13] S. Even and O. Goldreich, "On the security of multi-party ping-pong protocols," Proc. 24th IEEE Symp. Foundation of Computer Science, pp. 34-39, Oct. 1983.
[14] S. Goldwasser and S. Micali, "Probabilistic encryption and how to play mental poker keeping secret all private information," Proc. 14th ACM Symp. Theory of Computing, 1982.
[15] N. Heintze and J. Jaffar, "A decision procedure for a class of Herbrand set constraints," Proc. Fifth IEEE Symp. Logic in Computer Science, pp. 42-51, June 1990.
[16] T. Kasami, S. Yamamura, and K. Mori, "A key management scheme for end-to-end encryption and a formal verification of its security," Systems, Computers, Control, vol. 13, pp. 59-69, 1982.
[17] L. Lamport, "Time, clocks and the ordering of events in a distributed system," Comm. ACM, vol. 21, no. 7, pp. 558-565, July 1978.
[18] H.R. Lewis and C. Papadimitriou, Elements of the Theory of Computation. Prentice-Hall, 1981.
[19] C.A. Meadows, "Applying formal methods to the analysis of key management protocol," J. Computer Security, vol. 1, pp. 5-53, 1992.
[20] M.J. Merritt, "Cryptographic protocols," PhD thesis, Georgia Instit. of Tech nology, Feb. 1983.
[21] D. Otway and O. Rees, "Efficient and timely mutual authentication," Operating Systems Review, vol. 21, no. 1, pp. 8-10, Jan. 1987.
[22] P. Syverson and C. Meadows, "A logical language for specifying cryptographic protocol requirements," Proc. 1993 IEEE Symp. Research in Security and Privacy, May 1993.
[23] P. Syverson, "The use of logic in the analysis of cryptographic protocols," Proc. 1991 IEEE Symp. Research in Security and Privacy, May 1991.
[24] P. Syverson, "Adding time to a logic of authentication," Proc. First ACM Conf. Computer and Comm. Security,Fairfax, Va., Nov. 1993.

Index Terms:
Authentication, clocks, communication, composition, computer security, cryptography, formal methods, logic of authentication, model, model checking, protocol analysis, protocols, protocols-composition of, protocol analysis, security, time, timed models.
Citation:
Nevin Heintze, J.d. Tygar, "A Model for Secure Protocols and Their Compositions," IEEE Transactions on Software Engineering, vol. 22, no. 1, pp. 16-30, Jan. 1996, doi:10.1109/32.481514
Usage of this product signifies your acceptance of the Terms of Use.