Abstract
Security protocols provide critical services for distributed communication infrastructures. However, it is a challenge to ensure the correct functioning of their implementations, particularly, in the presence of malicious parties. We study testing of message confidentiality – an essential security property. We formally model protocol systems with an intruder using Dolev-Yao model. We discuss both passive monitoring and active testing of message confidentiality. For adaptive testing, we apply a guided random walk that selects next input on-line based on transition coverage and intruder’s knowledge acquisition. For mutation testing, we investigate a class of monotonic security flaws, for which only a small number of mutants need to be tested for a complete checking. The well-known Needham-Schroeder-Lowe protocol is used to illustrate our approaches.
This work was supported in part by the U.S. National Science Foundation (NSF) under grant awards CNS-0403342, CNS-0548403, and by the U.S. Department of Defense under grant award N41756-06-C-5541.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Achilles Proxy, http://www.mavensecurity.com/achilles
Chen, S., Kalbarczyk, Z., Xu, J., Iyer, R.K.: A Data-Driven Finite State Machine Model for Analyzing Security Vulnerabilities. In: International Conference on Dependable Systems and Networks (DSN 2003), p. 605 (2003)
DeMillo, R., Lipton, R., Sayward, F.: Hints on Test. Data Selection: Help For The Practicing Programmer. IEEE Computer 11(4), 34–41 (1978)
Dolev, D., Yao, A.: On the security of public-key protocols. IEEE Transaction on Information Theory 29, 198–208 (1983)
Duale, A., Ümit Uyar, M.: A Method Enabling Feasible Conformance Test Sequence Generation for EFSM Models. IEEE Trans. Computers 53(5), 614–627 (2004)
Fabbri, S., Maldonado, J., Sugeta, T., Masiero, P.: Mutation testing applied to validate specifications based on statecharts. In: International Symposium on Software Reliability Systems (ISSRE), pp. 210–219 (1999)
Geer, D., Harthorne, J.: Penetration Testing: A Duet. In: Proceedings of the 18th Annual Computer Security Applications Conference (ACSAC), pp. 185–198 (2002)
Jaiswal, S., Iannaccone, G., Kurose, J., Towlsey, D.: Formal Analysis of Passive Measurement Inference Techniques. In: Proceedings of IEEE Infocom 2006 (to appear, 2006)
Jurjens, J., Wimmel, G.: Formally Testing Fail-Safety of Electronic Purse Protocols. IEEE International Conference on Automated Software Engineering, 408 (2001)
Lee, D., Chen, D., Hao, R., Miller, R.E., Wu, J., Yin, X.: A formal approach for passive testing of protocol data portions. Proceedings of ICNP, 122–131 (2002)
Lee, D., Sabnani, K.K., Kristol, D.M., Paul, S.: Conformance Testing of Protocols Specified as Communicating Finite State Machines - a Guided Random Walk Based Approach. IEEE Trans. on Communications 44(5), 631–640 (1996)
Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines - A survey. Proceedings of the IEEE, 1090–1123 (August 1996)
Lee, D., Yannakakis, M.: Online minimization of transition systems. In: Proceedings of STOC, pp. 264–274 (1992)
Lowe, G.: Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055. Springer, Heidelberg (1996)
Marick, B.: The Weak Mutation Hypothesis. In: Proceedings of The ACM SIGSOFT Symposium on. Testing, Analysis, and Verification (October 1991)
Meadows, C.: Applying formal methods to the analysis of a key management protocol. J. Comput. Security 1, 5–53 (1992)
Meadows, C.: Formal methods for cryptographic protocol analysis: emerging issues and trends. IEEE Journal on Selected Areas in Communications 21(1), 44–54 (2003)
Needham, R., Schroeder, M.: Using encryption for authentication in large networks of computers. Communications of the ACM 21(12), 993–999 (1978)
Schneider, S.: Security Properties and CSP. In: Proceedings of the 1996 IEEE Symposium on Security and Privacy, p. 174 (1996)
Sheyner, O., Haines, J., Jha, S., Lippmann, R., Wing, J.: Automated Generation and Analysis of Attack Graphs. IEEE Symposium on Security and Privacy (2002)
Shu, G., Lee, D.: Network Protocol System Fingerprinting – A Formal Approach. In: Proceedings of IEEE Infocom 2006 (to appear, 2006)
Thompson, H.: Application Penetration Testing. IEEE Security & Privacy 3(1), 66–69 (2005)
Thompson, H.: Why Security Testing Is Hard. IEEE Security and Privacy 1(4), 83–86 (2003)
Wimmel, G., Jürjens, J.: Specification-Based Test Generation for Security-Critical Systems Using Mutations. In: George, C.W., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, pp. 471–482. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 IFIP International Federation for Information Processing
About this paper
Cite this paper
Shu, G., Lee, D. (2006). Message Confidentiality Testing of Security Protocols – Passive Monitoring and Active Checking. In: Uyar, M.Ü., Duale, A.Y., Fecko, M.A. (eds) Testing of Communicating Systems. TestCom 2006. Lecture Notes in Computer Science, vol 3964. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11754008_23
Download citation
DOI: https://doi.org/10.1007/11754008_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-34184-0
Online ISBN: 978-3-540-34185-7
eBook Packages: Computer ScienceComputer Science (R0)