Stéphanie Delaune, Hai Lin, and \relax Christopher Lynch. Protocol verification via rigid\slashflexible resolution. In Proceedings of the 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'07), pp. 242–256, Lecture Notes in Artificial Intelligence 4790, Springer, Yerevan, Armenia, October 2007.
In this paper we propose a decision procedure, i.e., an inference system for clauses containing rigid and flexible variables. Rigid variables are only allowed to have one instantiation, whereas flexible variables are allowed as many instantiations as desired. We assume a set of clauses containing only rigid variables together with a set of clauses containing only flexible variables. When the flexible clauses fall into a particular class, we propose an inference system based on ordered resolution that is sound and complete and for which the inference procedure will halt.
An interest in this form of problem is for cryptographic protocol verification for a bounded number of protocol instances. Our class allows us to obtain a generic decidability result for a large class of cryptographic protocols that may use for instance CBC (Cipher Block Chaining) encryption and blind signature.
@inproceedings{DLL-lpar07,
abstract = {In this paper we propose a decision procedure, i.e.,
an~inference system for clauses containing rigid and
flexible variables. Rigid variables are only allowed
to have one instantiation, whereas flexible variables
are allowed as many instantiations as desired.
We~assume a set of clauses containing only rigid
variables together with a set of clauses containing
only flexible variables. When the flexible clauses
fall into a particular class, we propose an inference
system based on ordered resolution that is sound and
complete and for which the inference procedure will
halt.\par An interest in this form of problem is for
cryptographic protocol verification for a bounded
number of protocol instances. Our class allows us to
obtain a generic decidability result for a large
class of cryptographic protocols that may use for
instance~CBC (Cipher Block Chaining) encryption and
blind signature.},
address = {Yerevan, Armenia},
author = {Delaune, St{\'e}phanie and Lin, Hai and
Lynch, {\relax Ch}ristopher},
booktitle = {{P}roceedings of the 14th {I}nternational
{C}onference on {L}ogic for {P}rogramming,
{A}rtificial {I}ntelligence, and {R}easoning
({LPAR}'07)},
OPTDOI = {10.1007/978-3-540-75560-9_19},
editor = {Dershowitz, Nachum and Voronkov, Andrei},
month = oct,
pages = {242-256},
publisher = {Springer},
series = {Lecture Notes in Artificial Intelligence},
title = {Protocol verification via rigid{\slash}flexible
resolution},
volume = {4790},
year = {2007},
acronym = {{LPAR}'07},
nmonth = {10},
lsv-category = {intc},
wwwpublic = {public and ccsb},
}