A Model-Based Testing Approach for Security Protocols

This talk presents results recently published in Software Testing, Verification and Reliability. In recent years, important efforts have been made for offering a dedicated language for modelling and verifying/proving security protocols. However, verifying the security protocol model does not guarantee that the actual implementation of the protocol will fulfil these properties. In this talk we present a model-based testing approach, relying on the mutation of HLPSL - the specification language of the AVISPA tool - models to generate abstract test cases. The proposed mutations aim at introducing leaks in the security protocols and represent real-world implementation errors.