DocumentCode :
3641164
Title :
Mutation-Based Test Generation from Security Protocols in HLPSL
Author :
Frédéric Dadeau;Pierre-Cyrille Héam;Rafik Kheddam
Author_Institution :
LIFC, Univ. de Franche-Comte, Besancon, France
fYear :
2011
fDate :
3/1/2011 12:00:00 AM
Firstpage :
240
Lastpage :
248
Abstract :
In the 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. Nevertheless, verifying the security protocol model does not guarantee that the actual implementation of the protocol will fulfil these properties. We propose in this paper a testing technique that makes it possible to validate an implementation of a security protocol, based on a HLPSL model. We introduce a set of mutation operators for HLPSL models that aim at introducing leaks in the security protocols. The mutated models are then analysed by the AVISPA tool set that will produce counter-example traces leading to the leaks, thus providing the test cases. We report an experiment of our mutation technique on a wide range of security protocols and discuss the relevance of the proposed mutation operators.
Keywords :
"Protocols","Servers","Public key","Encryption","Niobium"
Publisher :
ieee
Conference_Titel :
Software Testing, Verification and Validation (ICST), 2011 IEEE Fourth International Conference on
ISSN :
2159-4848
Print_ISBN :
978-1-61284-174-8
Type :
conf
DOI :
10.1109/ICST.2011.42
Filename :
5770613
Link To Document :
بازگشت