| | |
| | |
Stat |
Members: 3643 Articles: 2'488'730 Articles rated: 2609
29 March 2024 |
|
| | | |
|
Article overview
| |
|
Deciding security properties for cryptographic protocols. Application to key cycle | Hubert Comon-Lundh
; Véronique Cortier
; Eugen Zalinescu
; | Date: |
27 Aug 2007 | Abstract: | There has been a growing interest in applying formal methods for validating
cryptographic protocols and many results have been obtained. In this paper, we
re-investigate and extend the NP-complete decision procedure for a bounded
number of sessions of Rusinowitch and Turuani. In this setting, constraint
systems are now a standard for modeling security protocols. We provide a
generic approach to decide general security properties by showing that any
constraint system can be transformed in (possibly several) much simpler
constraint systems that are called emph{solved forms}.
As a consequence, we prove that deciding the existence of key cycles is
NP-complete for a bounded number of sessions. Indeed, 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.
We show that our decision procedure can also be applied to reprove
decidability of authentication-like properties and decidability of a
significant existing fragment of protocols with timestamps. | Source: | arXiv, 0708.3564 | Services: | Forum | Review | PDF | Favorites |
|
|
No review found.
Did you like this article?
Note: answers to reviews or questions about the article must be posted in the forum section.
Authors are not allowed to review their own article. They can use the forum section.
browser claudebot
|
| |
|
|
|
| News, job offers and information for researchers and scientists:
| |