Model‐based mutation testing from security protocols in HLPSL. (29th April 2014)

• Record Type: Journal Article
• Authors: Dadeau, Frédéric; Héam, Pierre‐Cyrille; Kheddam, Rafik; Maatoug, Ghazi; Rusinowitch, Michael
• Other Names: Jia Yue guestEditor.; Merayo Mercedes guestEditor.; Harman Mark guestEditor.
• Is Part Of: Software testing, verification & reliability. Volume 25:Number 5/7(2015)
• Page Start: 684
• Page End: 711
• Publication Date: 2014-04-29
• Subjects: mutation testing -- security protocols -- HLPSL -- AVISPA -- test generation; Computer software -- Testing -- Periodicals; Computer software -- Verification -- Periodicals; Computer software -- Reliability -- Periodicals; 005.14
• DOI: 10.1002/stvr.1531
• Languages: English
• ISSNs: 0960-0833

Abstract

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 abstract 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 abstract 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 abstract 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. Abstract : 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.