Stéphanie Delaune, Hai Lin, and Christopher Lynch. Protocol verification via rigid\slashflexible resolution. In Proceedings of the Workshop on Automated Deduction: Decidability, Complexity, Tractability (ADDCT'07), pp. 2–16, Bremen, Germany, July 2007.
(unavailable)
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-addct07,
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 = {Bremen, Germany},
author = {Delaune, St{\'e}phanie and Lin, Hai and
Lynch, {Ch}ristopher},
booktitle = {{P}roceedings of the {W}orkshop on {A}utomated
{D}eduction: {D}ecidability, {C}omplexity,
{T}ractability ({ADDCT}'07)},
editor = {Ghilardi, Silvio and Sattler, Ulrike and
Sofronie-Stokkermans, Viorica and Tiwari, Ashish},
month = jul,
pages = {2-16},
title = {Protocol verification via rigid{\slash}flexible
resolution},
year = {2007},
acronym = {{ADDCT}'07},
nmonth = {7},
lsv-category = {autc},
wwwpublic = {perso},
}