Cryptographic protocol verification using tractable classes of horn clauses

Helmut Seidl; Kumar Neeraj Verma

doi:10.1007/978-3-540-71322-7_5

Cryptographic protocol verification using tractable classes of horn clauses

Helmut Seidl
, Kumar Neeraj Verma

Research output: Contribution to journal › Conference article › Research › peer-review

Abstract

We consider secrecy problems for cryptographic protocols modeled using Horn clauses and present general classes of Horn clauses which can be efficiently decided. Besides simplifying the methods for the class of flat and onevariable clauses introduced for modeling of protocols with single blind copying [7,25], we also generalize this class by considering k-variable clauses instead of one-variable clauses with suitable restrictions similar to those for the class S(+). This class allows to conveniently model protocols with joint blind copying. We show that for a fixed k, our new class can be decided in DEXPTIME, as in the case of one variable.

Original language	English
Book series	Lecture Notes in Computer Science
Volume	4444
Pages (from-to)	97-119
ISSN	0302-9743
DOIs	https://doi.org/10.1007/978-3-540-71322-7_5
Publication status	Published - 2007
Event	Symposium on Program Analysis and Compilation, Theory and Practice: Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday - Schloss Dagstuhl, Germany Duration: 9 Jun 2006 → 10 Jun 2006

Conference

Conference	Symposium on Program Analysis and Compilation, Theory and Practice
Country/Territory	Germany
City	Schloss Dagstuhl
Period	09/06/2006 → 10/06/2006

Bibliographical note

ISBN: 978-3-540-71315-9 (Book in journal series)

Access to Document

10.1007/978-3-540-71322-7_5

OpenUrl availability

Check availability in DTU Findit

Cite this

@inproceedings{a0c82a2ebccc4595bb46cb45ac06939d,

title = "Cryptographic protocol verification using tractable classes of horn clauses",

abstract = "We consider secrecy problems for cryptographic protocols modeled using Horn clauses and present general classes of Horn clauses which can be efficiently decided. Besides simplifying the methods for the class of flat and onevariable clauses introduced for modeling of protocols with single blind copying [7,25], we also generalize this class by considering k-variable clauses instead of one-variable clauses with suitable restrictions similar to those for the class S(+). This class allows to conveniently model protocols with joint blind copying. We show that for a fixed k, our new class can be decided in DEXPTIME, as in the case of one variable.",

author = "Helmut Seidl and \{Neeraj Verma\}, Kumar",

note = "ISBN: 978-3-540-71315-9 (Book in journal series); Symposium on Program Analysis and Compilation, Theory and Practice : Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday ; Conference date: 09-06-2006 Through 10-06-2006",

year = "2007",

doi = "10.1007/978-3-540-71322-7\_5",

language = "English",

volume = "4444",

pages = "97--119",

journal = "Lecture Notes in Computer Science",

issn = "0302-9743",

publisher = "Springer Science and Business Media Deutschland GmbH",

}

TY - GEN

T1 - Cryptographic protocol verification using tractable classes of horn clauses

AU - Seidl, Helmut

AU - Neeraj Verma, Kumar

N1 - ISBN: 978-3-540-71315-9 (Book in journal series)

PY - 2007

Y1 - 2007

N2 - We consider secrecy problems for cryptographic protocols modeled using Horn clauses and present general classes of Horn clauses which can be efficiently decided. Besides simplifying the methods for the class of flat and onevariable clauses introduced for modeling of protocols with single blind copying [7,25], we also generalize this class by considering k-variable clauses instead of one-variable clauses with suitable restrictions similar to those for the class S(+). This class allows to conveniently model protocols with joint blind copying. We show that for a fixed k, our new class can be decided in DEXPTIME, as in the case of one variable.

AB - We consider secrecy problems for cryptographic protocols modeled using Horn clauses and present general classes of Horn clauses which can be efficiently decided. Besides simplifying the methods for the class of flat and onevariable clauses introduced for modeling of protocols with single blind copying [7,25], we also generalize this class by considering k-variable clauses instead of one-variable clauses with suitable restrictions similar to those for the class S(+). This class allows to conveniently model protocols with joint blind copying. We show that for a fixed k, our new class can be decided in DEXPTIME, as in the case of one variable.

U2 - 10.1007/978-3-540-71322-7_5

DO - 10.1007/978-3-540-71322-7_5

M3 - Conference article

SN - 0302-9743

VL - 4444

SP - 97

EP - 119

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

T2 - Symposium on Program Analysis and Compilation, Theory and Practice

Y2 - 9 June 2006 through 10 June 2006

ER -

Cryptographic protocol verification using tractable classes of horn clauses

Abstract

Conference

Bibliographical note

Access to Document

OpenUrl availability

Fingerprint

Cite this