BIBLIOS

Document type
Journal articles

Document subtype
Full paper

Title
An Equation-Based Classical Logic

Participants in the publication
Andreia Mordido (Author)
Dep. Informática
LASIGE
Carlos Caleiro (Author)

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.


Where published
Logic, Language, Information, and Computation,Lecture Notes in Computer Science

Publication Identifiers
ISSN - 0302-9743
eISSN - 1611-3349
ISBN - 9783662477083,9783662477090

Publisher
Springer Berlin Heidelberg



Document Identifiers
URL - http://dx.doi.org/10.1007/978-3-662-47709-0_4
DOI - https://doi.org/10.1007/978-3-662-47709-0_4

Rankings
SCOPUS Q3 (2014) - 0.325 - General Computer Science

Keywords
Completeness Equational logic Classical logic Decidability