Message confidentiality testing of security protocols - Passive monitoring and active checking

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 online 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. © IFIP International Federation for Information Processing 2006.