Deciding key cycles for security protocols

Deciding key cycles for security protocols. V. Cortier and E. Zalinescu. In Proceedings of the 13th Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'06), pp. 317–331, Lecture Notes in Artificial Intelligence 4246, Springer, Phnom Penh, Cambodia, November 2006.

Download

[PDF] [HTML]

Abstract

Many recent results are concerned with interpreting proofs of security done in symbolic models in the more detailed models of computational cryptography. In the case of symmetric encryption, these results stringently demand that no key cycle (e.g. k k ) can be produced during the execution of protocols. While security properties like secrecy or authentication have been proved decidable for many interesting classes of protocols, the automatic detection of key cycles has not been studied so far.
In this paper, we prove that deciding the existence of key-cycles is NP-complete for a bounded number of sessions. Next, we observe that the techniques that we use are of more general interest and apply them to reprove the decidability of a significant existing fragment of protocols with timestamps.

BibTeX

@InProceedings{EugenLPAR06,
  author = 	 {V. Cortier and E. Zalinescu},
  title = 	 {Deciding key cycles for security protocols},
  booktitle = {Proceedings of the 13th Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'06)},
  pages = 	 {317-331},
  year = 	 {2006},
  volume = 	 {4246},
  series = 	 {Lecture Notes in Artificial Intelligence},
  address = 	 {Phnom Penh, Cambodia},
  month = 	 {November},
  abstract = {Many recent results are concerned with interpreting proofs of security 
done in symbolic models in the more detailed models of computational cryptography. 
In the case of symmetric encryption, these results stringently demand that no key 
cycle (e.g. {k} k ) can be produced during the execution of protocols. While security 
properties like secrecy or authentication have been proved decidable for many 
interesting classes of protocols, the automatic detection of key cycles has not been 
studied so far.
\par
In this paper, we prove that deciding the existence of key-cycles is NP-complete for 
a bounded number of sessions. Next, we observe that the techniques that we use are of
 more general interest and apply them to reprove the decidability of a significant 
existing fragment of protocols with timestamps.},
  publisher = {Springer},
  doi = {10.1007/11916277_22},
}