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

https://hal.inria.fr/hal-00915320
Contributor : Michaël Rusinowitch <>
Submitted on : Saturday, December 7, 2013 - 11:32:00 AM
Last modification on : Tuesday, December 18, 2018 - 4:38:25 PM

Links full text

Identifiers

Citation

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⟩

Share

Metrics

Record views

233