Skip to Main content Skip to Navigation
Conference papers

Compiling symbolic attacks to protocol implementation tests

Hatem Ghabri 1 Ghazi Maatoug 2, 1 Michael Rusinowitch 2
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : Recently efficient model-checking tools have been developed to find flaws in security protocols specifications. These flaws can be interpreted as potential attacks scenarios but the feasability of these scenarios need to be confirmed at the implementation level. However, bridging the gap between an abstract attack scenario derived from a specification and a penetration test on real implementations of a protocol is still an open issue. This work investigates an architecture for automatically generating abstract attacks and converting them to concrete tests on protocol implementations. In particular we aim to improve previously proposed blackbox testing methods in order to discover automatically new attacks and vulnerabilities. As a proof of concept we have experimented our proposed architecture to detect a renegotiation vulnerability on some implementations of SSL/TLS, a protocol widely used for securing electronic transactions.
Document type :
Conference papers
Complete list of metadatas
Contributor : Michaël Rusinowitch <>
Submitted on : Saturday, December 7, 2013 - 11:32:00 AM
Last modification on : Wednesday, September 16, 2020 - 10:43:31 AM

Links full text



Hatem Ghabri, Ghazi Maatoug, Michael Rusinowitch. Compiling symbolic attacks to protocol implementation tests. Fourth International Symposium on Symbolic Computation in Software Science, Adel Bouhoula and Tetsuo Ida and Fairouz Kamareddine, Dec 2012, Tunis, Tunisia. ⟨10.4204/EPTCS.122.4⟩. ⟨hal-00915320⟩