Model-based mutation testing from security protocols in HLPSL

• Published in: Software testing, verification & reliability verification & reliability, 2015-08, Vol.25 (5-7), p.684-711
• Main Authors: Dadeau, Frédéric, Héam, Pierre-Cyrille, Kheddam, Rafik, Maatoug, Ghazi, Rusinowitch, Michael
• Format: Article
• Language: English
• Subjects: AVISPA; Computer information security; Computer Science; Cryptography and Security; HLPSL; Internet; Mathematical models; mutation testing; Mutations; Program verification (computers); Protocol (computers); Security; security protocols; Software Engineering; test generation
• ISSN: 0960-0833; 1099-1689
• DOI: 10.1002/stvr.1531

Summary In recent years, important efforts have been made for offering a dedicated language for modelling and verifying security protocols. Outcome of the European project AVISPA, the high‐level security protocol language (HLPSL) aims at providing a means for verifying usual security properties (such as data secrecy) in message exchanges between agents. However, verifying the security protocol model does not guarantee that the actual implementation of the protocol will fulfil these properties. This article presents a model‐based testing approach, relying on the mutation of HLPSL models to generate test cases. The proposed mutations aim at introducing leaks in the security protocols and represent real‐world implementation errors. The mutated models are then analysed by the automated validation of Internet security protocols and applications tool set, which produces, when the mutant protocol is declared unsafe, counterexample traces exploiting the security flaws and, thus, providing test cases. A dedicated framework is then used to concretize the attack traces, bridging the gap between the formal model level and the implementation level. This model‐based testing technique has been experimented on a wide range of security protocols, in order to evaluate the mutation operators. This process has also been fully tool‐supported, from the mutation of the HLPSL model to the concretization of the test cases into test scripts. It has been applied to a realistic case study of the Paypal payment protocol, which made it possible to discover a vulnerability in an implementation of an e‐commerce framework. Copyright © 2014 John Wiley & Sons, Ltd. This article proposes a model‐based mutation testing approach for security protocols written in HLPSL. Mutation operators for protocol models, expressing real‐world implementation choices or mistakes, are presented and evaluated on a large bench of real‐world protocols. Finally, it describes a framework that helps automating the execution of the generated test cases. Copyright © 2014 John Wiley & Sons, Ltd.