Reduction of the Intruder Deduction Problem into Equational Elementary Deduction for Electronic Purse Protocols with Blind Signa

Abstract. The intruder deduction problem for an electronic purse protocol with blind signatures is considered. The algebraic properties of the protocol are modeled by an equational theory implemented as a convergent rewriting system which involves rules for addition, multiplication and exponentiation. The whole deductive power of the intruder is modeled as a sequent calculus that, modulo this rewriting system, deals with blind signatures. It is proved that the associative-commutative (AC) equality of the algebraic theory can be decided in polynomial time, provided a strategy to avoid distributivity law between the AC operators is adopted. Moreover, it is also shown that the intruder deduction problem can be reduced in polynomial time to the elementary deduction problem for this equational theory.

• Type: Conference
• Year: 2010
• Where: WOLLIC
• Authors: Daniele Nantes Sobrinho, Mauricio Ayala-Rincón
• Keywords: Artificial Intelligence, Blind Signatures, Equational Theory, Intruder Deduction Problem, WOLLIC 2010