TY - GEN
T1 - Cryptographic protocol verification using tractable classes of horn clauses
AU - Seidl, Helmut
AU - Verma, Kumar Neeraj
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 one-variable 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 one-variable 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.
UR - http://www.scopus.com/inward/record.url?scp=39149130363&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-71322-7_5
DO - 10.1007/978-3-540-71322-7_5
M3 - Conference contribution
AN - SCOPUS:39149130363
SN - 9783540713159
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 97
EP - 119
BT - Program Analysis and Compilation, Theory and Practice - Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday
PB - Springer Verlag
T2 - Symposium on Program Analysis and Compilation, Theory and Practice. Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday
Y2 - 9 June 2006 through 10 June 2006
ER -