An Equation-Based Classical Logic?

Abstract. We propose and study a logic able to state and reason about equational constraints, by combining aspects of classical propositional logic, equational logic, and quantifiers. The logic has a classical struc-ture over an algebraic base, and a form of universal quantification distin-guishing between local and global validity of equational constraints. We present a sound and complete axiomatization for the logic, parameter-ized by an equational specification of the algebraic base. We also show (by reduction to SAT) that the logic is decidable, under the assumption that its algebraic base is given by a convergent rewriting system, thus covering an interesting range of examples. As an application, we analyze offline guessing attacks to security protocols, where the equational base specifies the algebraic properties of the cryptographic primitives. Key words: classical logic, equational logic, completeness, decidability.