In this talk, we will mention unification problem for special equational theories of interest. The motivation for our work mainly originates from the application of unification procedures to the analysis of cryptographic protocols, in particular blind signature schemes. A successful approach to formal verification of protocols is based on state space exploration. Attacks on protocols are analyzed using backward reachability analysis, i.e., checking the reachability from flawed states to start states. In this context, unification comes into play when solving equations of terms (corresponding to messages exchanged during protocol sessions) at each step with respect to some algebraic properties, for example associativity and commutativity.
Blind signatures are signature schemes that keep the content confidential and have applications in modern cryptography for electronic voting and digital cash schemes. They have been implemented based on well-known signature schemes such as RSA and El Gamal encryption.
We will present an algebraic property (axiom E) of blind RSA signatures. We will show that the equational theory defined by E has an undecidable unification. The undecidability result follows by reduction from the boundedness problem for Intercell Turing Machines. Furthermore, it appears that E is the simplest equational theory, to our knowledge, which has an undecidable unification problem.
Theories similar to E have decidable unification problems. We will briefly present other theories of blind signatures,
having decidable unification problems. The results we obtained will be useful to analyze the protocols with blinding schemes when they are integrated into protocol analysis tools.
Strada le Grazie 15
Partita IVA 01541040232
Codice Fiscale 93009870234
© 2020 | Università degli studi di Verona | Credits