Abstract
With the explosive growth of the Internet and the distributed applications it supports, there is a pressing need for secure group communications — the ability of a group of agents to communicate securely with each other while allowing members to join or leave the group. Prompted by the success of other researchers in applying finite-state model-checking tools to the verification of small security protocols, we decided to attempt a larger security protocol: a recently published protocol for secure group communication. Not surprisingly, creating an ad hoc abstract model suitable for model-checking required cleverness, and state explosion was always a threat. Nevertheless, with minimal effort, the model checking tool discovered two flaws in the protocol, one of which has not been reported previously. We conclude our paper with a discussion of possible fixes to the protocol, as well as suggested verification tool improvements that would have simplified our task.
Chapter PDF
References
J.-M. Chang and N. F. Maxemchuk. Reliable broadcast protocols. ACM Transactions on Computer Systems, 2 (3): 251–273, August 1984.
E. Clarke, K. McMillan, S. Campos, and V. Hartonas-Garmhausen. Symbolic model checking. In R. Alur and T. A. Henzinger, editors, Computer-Aided Verification: Eighth International Conference, pages 419–422. Springer-Verlag, July 1996. Lecture Notes in Computer Science Number 1102.
E. W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM, 18 (8): 453–457, August 1975.
D. L. Dill, A. J. Drexler, A. J. Hu, and C. H. Yang. Protocol verification as a hardware design aid. In International Conference on Computer Design. IEEE, October 1992.
G. J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, 1991.
A. J. Hu and D. L. Dill. Reducing BDD size by exploiting functional dependencies. In 30’ Design Automation Conference, pages 266–271. ACM/IEEE, 1993.
C. N. Ip and D. L. Dill. Efficient verification of symmetric concurrent systems. In International Conference on Computer Design, pages 230–234. IEEE, October 1993.
G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In Tools and Algorithms for the Construction and Analysis of Systems, pages 147–166. Springer-Verlag, 1996. Also published in Software Concepts and Tools Volume 17, pp. 93–102.
J. C. Mitchell, M. Mitchell, and U. Stern. Automated analysis of cryptographic protocols using Murphi. In Symposium on Security and Privacy, pages 141–151. IEEE, 1997.
S. Mittra. Iolus: A framework for scalable secure multicasting. In SIGCOMM. ACM, 1997.
V. Shmatikov and U. Stern. Efficient finite-state analysis for large security protocols. In 11 “ Computer Security Foundations Workshop, pages 106–115. IEEE, 1998.
P. Wolper, U. Stem, D. Leroy, and D. Dill. Reliable probabilistic verification using hash compaction. Submitted for publication. A draft is available from http://sprout.Stanford.EDU/uli/publications.html.
C. K. Wong, M. Gouda, and S. S. Lam. Secure group communications using key graphs. In SIGCOMM. ACM, 1998.
W. D. Young, W. E. Boebert, and R. Y. Kain, Proving a Computer System Secure, The Scientific Honeyweller, vol 6, no 2 (July 1985), pp. 18–27. Reprinted in Computer and Network Security, M. D. Abrams and H. J. Podell, eds., IEEE Computer Society Press, 1986.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Hu, A.J., Li, R., Shi, X., Vuong, S. (1999). Model-Checking a Secure Group Communication Protocol: A Case Study. In: Wu, J., Chanson, S.T., Gao, Q. (eds) Formal Methods for Protocol Engineering and Distributed Systems. PSTV FORTE 1999 1999. IFIP Advances in Information and Communication Technology, vol 28. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35578-8_27
Download citation
DOI: https://doi.org/10.1007/978-0-387-35578-8_27
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5270-0
Online ISBN: 978-0-387-35578-8
eBook Packages: Springer Book Archive