Búsqueda avanzada

El autor Santiago Escobar ha publicado 6 artículo(s):

1 - Variant-based Equational Unification under Constructor Symbols

Equational unification of two terms consists of finding a substitution that, when applied to both terms, makes them equal modulo some equational properties. A narrowing-based equational unification algorithm relying on the concept of the variants of a term is available in the most recent version of Maude, version 3.0, which provides quite sophisticated unification features. A variant of a term t is a pair consisting of a substitution σ and the canonical form of tσ. Variant-based unification is decidable when the equational theory satisfies the finite variant property. However, this unification procedure does not take into account constructor symbols and, thus, may compute many more unifiers than the necessary or may not be able to stop immediately. In [1], we integrate the notion of constructor symbol into the variant-based unification algorithm. Our experiments on positive and negative unification problems show an impressive speedup.

Autores: Damián Aparicio-Sánchez / Santiago Escobar / Julia Sapiña / 
Palabras Clave: equational unification - Maude - Variants

2 - An Optimizing Protocol Transformation for Constructor Finite Variant Theories in Maude-NPA

Maude-NPA is an analysis tool for cryptographic security protocols that takes into account the algebraic properties of the cryptosystem. Maude-NPA can reason about a wide range of cryptographic properties. However, some alge- braic properties, and protocols using them, have been beyond Maude-NPA capabilities, either because the cryptographic properties cannot be expressed using its equational unification features or because the state space is unman- ageable. In [1], we provide a protocol transformation that can safely get rid of cryptographic properties under some conditions. We also provide, for the first time, an encoding of the theory of bilinear pairing into Maude-NPA that goes beyond the encoding of bilinear pairing available in the Tamarin tool.

Autores: Damián Aparicio-Sánchez / Santiago Escobar / Raúl Gutiérrez / Julia Sapiña / 
Palabras Clave: Bilinear pairing - Crypto protocol analysis - Diffie-Hellman Exponentiation - Protocol transformation

4 - Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA

We perform an automated analysis of two devices developed by Yubico: YubiKey, designed to authenticate a user to network-based services, and YubiHSM, Yubico’s hardware security module. Both are analyzed using the Maude-NPA cryptographic protocol analyzer. Although previous work has been done applying formal tools to these devices, there has not been any completely automated analysis. This is not surprising, because both YubiKey and YubiHSM, which make use of cryptographic APIs, involve a number of complex features: (i) discrete time in the form of Lamport clocks, (ii) a mutable memory for storing previously seen keys or nonces, (iii) event-based properties that require an analysis of sequences of actions, and (iv) reasoning modulo exclusive-or. Maude-NPA has provided support for exclusive-or for years but has not provided support for the other three features, which we show can also be supported by using constraints on natural numbers, protocol composition and reasoning modulo associativity. In this work, we have been able to automatically prove security properties of YubiKey and find the known attacks on the YubiHSM, in both cases beyond the capabilities of previous work using the Tamarin Prover due to the need of auxiliary user-defined lemmas and limited support for exclusive-or. Tamarin has recently been endowed with exclusive-or and we have rewritten the original specification of YubiHSM in Tamarin to use exclusive-or, confirming that both attacks on YubiHSM can be carried out by this recent version of Tamarin.

Autores: Antonio Gonzalez-Burgueño / Damian Aparicio / Santiago Escobar / Catherine Meadows / Jose Meseguer / 
Palabras Clave: equational unification - narrowing - protocol analysis - Rewriting Logic - security

6 - Associative Unification and Symbolic Reasoning Modulo Associativity in Maude

We have added support for associative unification to Maude 2.7.1. Associative unification is infinitary, i.e., there are unifica- tion problems u =? v such that there is an infinite minimal set of unifiers, whereas associative-commutative unification is finitary. A unique feature of the associative unification algorithm implemented in Maude is that it is guaranteed to terminate with a finite and complete set of associative unifiers for a fairly large class of unification problems occurring in prac- tice. For any problems outside this class, the algorithm returns a finite set of unifiers together with a warning that such set may be incom- plete. This paper describes this associative unification algorithm imple- mented in Maude and also how other symbolic reasoning Maude features such as (i) variant generation; (ii) variant unification; and (iii) narrow- ing based symbolic reachability analysis have been extended to deal with associativity.

Autores: Francisco Durán / Steven Eker / Santiago Escobar / Narciso Marti-Oliet / Jose Meseguer / Carolyn Talcott / 
Palabras Clave: associativity - narrowing - Rewriting Logic - unification