BIBLIOS

Tipo
Artigos em Revista

Tipo de Documento
Artigo Completo

Título
An Equation-Based Classical Logic

Participantes na publicação
Andreia Mordido (Author)
Dep. Informática
LASIGE
Carlos Caleiro (Author)

Resumo
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.


Suporte
Logic, Language, Information, and Computation,Lecture Notes in Computer Science

Identificadores da Publicação
ISSN - 0302-9743
eISSN - 1611-3349
ISBN - 9783662477083,9783662477090

Editora
Springer Berlin Heidelberg



Identificadores do Documento
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

Identificadores de Qualidade
SCOPUS Q3 (2014) - 0.325 - General Computer Science

Keywords
Completeness Equational logic Classical logic Decidability