Book chapter
Cryptographic Protocol Verification Using Tractable Classes of Horn Clauses
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 \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$\mathcal{S^{+}}$\end{document}.
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.
Language: | English |
---|---|
Publisher: | Springer Berlin Heidelberg |
Year: | 2007 |
Pages: | 97-119 |
ISBN: | 1280940697 , 3540713158 , 3540713220 , 9781280940699 , 9783540713159 and 9783540713227 |
Types: | Book chapter |
DOI: | 10.1007/978-3-540-71322-7_5 |