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. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Delaune, S., Lin, H., & Lynch, C. (2007). Protocol verification via rigid/flexible resolution. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4790 LNAI, pp. 242–256). Springer Verlag. https://doi.org/10.1007/978-3-540-75560-9_19
Mendeley helps you to discover research relevant for your work.