On the Automated Correction of Protocols with Improper Message Encoding

Dieter Hutter, Raul Monroy

In: Luca Vigano , Pierpaolo Degano (editor). Proceedings of the Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security. Workshop on Automated Reasoning for Security Protocol Analysis (ARSPA) located at Affiliated with ETAPS 2009 March 28-29 York United Kingdom Lectures Notes in Computer Science (LNCS) Springer Verlag 2009.


Security protocols are crucial to achieve trusted computing. Since designing security protocols is error-prone, security protocols are typically faulty and have to be fixed. Continuing previous work we present first steps to automate this repair process especially for protocols that are susceptible to type-flaw attacks. To this end, we extend the notion of strand spaces by introducing an implementation layer for messages and extending the capabilities of a penetrator to swap messages that share the same implementation. Based on this framework we are able to track type flaw attacks to incompatibilities between the way messages are implemented and the design of concrete security protocols. Heuristics are given to either change the implementation or the protocol to avoid these situations.

German Research Center for Artificial Intelligence
Deutsches Forschungszentrum für Künstliche Intelligenz