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

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.

Date of Publication

2015

2015

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

Volume

9160

9160

Number of pages

14

14

Starting page

38

38

Last page

52

52

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

APA

Andreia Mordido, Carlos Caleiro, (2015). An Equation-Based Classical Logic. Logic, Language, Information, and Computation,Lecture Notes in Computer Science, 9160, 38-52. ISSN 0302-9743. eISSN 1611-3349. http://dx.doi.org/10.1007/978-3-662-47709-0_4

IEEE

Andreia Mordido, Carlos Caleiro, "An Equation-Based Classical Logic" in Logic, Language, Information, and Computation,Lecture Notes in Computer Science, vol. 9160, pp. 38-52, 2015. 10.1007/978-3-662-47709-0_4

BIBTEX

@article{35844, author = {Andreia Mordido and Carlos Caleiro}, title = {An Equation-Based Classical Logic}, journal = {Logic, Language, Information, and Computation,Lecture Notes in Computer Science}, year = 2015, pages = {38-52}, volume = 9160 }

Andreia Mordido, Carlos Caleiro, (2015). An Equation-Based Classical Logic. Logic, Language, Information, and Computation,Lecture Notes in Computer Science, 9160, 38-52. ISSN 0302-9743. eISSN 1611-3349. http://dx.doi.org/10.1007/978-3-662-47709-0_4

IEEE

Andreia Mordido, Carlos Caleiro, "An Equation-Based Classical Logic" in Logic, Language, Information, and Computation,Lecture Notes in Computer Science, vol. 9160, pp. 38-52, 2015. 10.1007/978-3-662-47709-0_4

BIBTEX

@article{35844, author = {Andreia Mordido and Carlos Caleiro}, title = {An Equation-Based Classical Logic}, journal = {Logic, Language, Information, and Computation,Lecture Notes in Computer Science}, year = 2015, pages = {38-52}, volume = 9160 }