zbMATH — the first resource for mathematics

An equation-based classical logic. (English) Zbl 06484967
Paiva, Valeria (ed.) et al., Logic, language, information, and computation. 22nd international workshop, WoLLIC 2015, Bloomington, IN, USA, July 20–23, 2015. Proceedings. Berlin: Springer (ISBN 978-3-662-47708-3/pbk; 978-3-662-47709-0/ebook). Lecture Notes in Computer Science 9160, 38-52 (2015).
Summary: 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 structure over an algebraic base, and a form of universal quantification distinguishing between local and global validity of equational constraints. We present a sound and complete axiomatization for the logic, parameterized 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.
For the entire collection see [Zbl 1319.03010].

03B70 Logic in computer science
Full Text: DOI