Mutation-Based Test Generation from Security Protocols in HLPSL

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...

Full description

Saved in:
Bibliographic Details
Main Authors: Dadeau, F, Héam, Pierre-Cyrille, Kheddam, R
Format: Conference Proceeding
Language:English
Subjects:
AVISPA
Encryption
HLPSL
mutation
Niobium
Protocols
Public key
security protocols
Servers
test generation
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2159-4848
2771-3091
DOI:10.1109/ICST.2011.42