Protocol analysis modulo exclusive-or theories: a case study in Maude-MPA

Abstract

[EN] Escobar of the Universitat Politècnica de València in collaboration with José Meseguer (University of Illinois at Urbana-Champaign, USA) and Catherine Meadows (Naval Research Lab, Washington, DC, USA). We focus on protocols using exclusive-or as the only cryptographic properties of symbols, apart of the standard cancellation of encryption and decryption. The protocols analyzed in this document are borrowed from the paper ”Reducing Protocol Analysis with XOR to the XOR- Free Case in the Horn Theory Based Approach” by Ralf Küesters and Tomasz Truderung published in Journal of Automated Reasoning, volume 46, pages 325-352, Springer 2011. These protocols are divided into two groups, those that can be specified in the Alice-Bob notation and those corresponding to an Application Programming Interface (API). We have proved the same security properties described in Küesters and Truderung paper, but we go beyond that paper in the sense that we have provided protocol specifications that meet all the requirements of the original protocols, whereas Küesters and Truderung paper use simplified versions of these protocols. The main problem that we have encountered is to specify API protocols in Maude-NPA, since this was the first time that this kind of protocols were specified in the tool. Another contribution of this thesis is to confirm that protocols with exclusive-or can be verified in Maude-NPA

[ES] El desarrollo de esta tesis final de máster tiene como objetivo verificar diversos protocolos de seguridad existentes utilizando una herramienta de verificación automatizada de protocolos, Maude- NPA, desarrollada por Santiago Escobar, de la Universitat Politècnica de València , en colaboración con José Meseguer (Universidad de Illinois en Urbana- Champaign, EE.UU.) y Catherine Meadows (Naval Research Lab , Washington , DC, EE.UU.). Nos centramos en el uso de protocolos con el operador orexclusivo como propiedad principal criptográfica de símbolos, así como la cancelación estándar de cifrado y descifrado. Los protocolos analizados en esta tesis los tomamos del artículo ”Reducing Protocol Analysis with XOR to the XOR- Free Case in the Horn Theory Based Approach” de Ralf Küesters y Tomasz Truderung publicado en el “Journal of Automated Reasoning”, volumen 46, páginas 325-352 en el 2011 en Springer. Estos protocolos se dividen en dos grupos, los que se pueden especificar en la notación Alice-Bob y los correspondientes a una interfaz de programación de aplicaciones (API) . Hemos probado las mismas propiedades de seguridad descritas en el artículo de Ralf Küesters y Tomasz Truderung , pero yendo más allá, en el sentido de que hemos proporcionado las especificaciones de los protocolos que cumplen con todos los requisitos de los protocolos originales , mientras que en el artículo de Ralf Küesters y Tomasz Truderung utilizan versiones simplificadas de estos protocolos. El principal problema que nos hemos encontrado al especificar los protocolos API, es que esta fue la primera vez que este tipo de protocolos se especificó en Maude-NPA. Otra aportación de esta tesis es la confirmación de que los “protocolos or-exclusivos” pueden ser verificados en Maude-NPA .