Skip to Main content Skip to Navigation

A resolution Strategy for Verifying Cryptographic Protocols with CBC Encryption and Blind Signatures

Véronique Cortier 1 Michaël Rusinowitch 1 Eugen Zalinescu 1
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Formal methods have proved to be very useful for analyzing cryptographic protocols. However, most existing techniques apply to the case of abstract encryption schemes and pairing. In this paper, we consider more complex, less studied cryptographic primitives like CBC encryption and blind signatures. This leads us to introduce a new fragment of Horn clauses. We show decidability of this fragment using a combination of several resolution strategies. As a consequence, we obtain a new decidability result for a class of cryptographic protocols (with an unbounded number of sessions and a bounded number of nonces) that may use for example CBC encryption and blind signatures. We apply this result to fix the Needham-Schroeder symmetric key authentication protocol, which is known to be flawed when CBC mode is used.
Keywords : verification cryptographic protocols horn clauses resolution strategies
Document type :
Conference papers
Complete list of metadatas
https://hal.inria.fr/inria-00000557
Contributor : Véronique Cortier <>
Submitted on : Wednesday, November 2, 2005 - 3:00:36 PM
Last modification on : Wednesday, January 8, 2020 - 2:16:59 PM

Identifiers

  • HAL Id : inria-00000557, version 1

Collections

INRIA | CNRS | UNIV-FCOMTE | UNIV-BM | FEMTO-ST | UNIV-BM-THESE | LORIA | UNIV-LORRAINE

Citation

Véronique Cortier, Michaël Rusinowitch, Eugen Zalinescu. A resolution Strategy for Verifying Cryptographic Protocols with CBC Encryption and Blind Signatures. 7th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming - PPDP'05, Jul 2005, Lisbonne/Portugal, pp.12-22. ⟨inria-00000557⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

306

 

Contact                    Legal Notice                    Personal Data