Model-based mutation testing from security protocols in HLPSL

Abstract : 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.
Type de document :
Article dans une revue
Journal of Software Testing, Verification, and Reliability, John Wiley & Sons, 2015, pp.30. 〈10.1002/stvr.1531〉
Liste complète des métadonnées
Contributeur : Michaël Rusinowitch <>
Soumis le : jeudi 4 décembre 2014 - 12:15:47
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10

Lien texte intégral



Frédéric Dadeau, Pierre-Cyrille Héam, Rafik Kheddam, Ghazi Maatoug, Michaël Rusinowitch. Model-based mutation testing from security protocols in HLPSL. Journal of Software Testing, Verification, and Reliability, John Wiley & Sons, 2015, pp.30. 〈10.1002/stvr.1531〉. 〈hal-01090881〉



Consultations de la notice