Title

Secrecy For Bounded Security Protocols With Freshness Check Is Nexptime-Complete

Keywords

Complexity; Secrecy problem; Security protocol

Abstract

The secrecy problem for security protocols is the problem to decide whether or not a given security protocol has leaky runs. In this paper, the (initial) secrecy problem for bounded protocols with freshness check is shown to be NEXPTIME-complete. Relating the formalism in this paper to the multiset rewriting (MSR) formalism we obtain that the initial secrecy problem for protocols in restricted form, with bounded length messages, bounded existentials, with or without disequality tests, and an intruder with no existentials, is NEXPTIME-complete. If existentials for the intruder are allowed but disequality tests are not allowed, the initial secrecy problem still is NEXPTIME-complete. However, if both existentials for the intruder and disequality tests are allowed and the protocols are not well-founded (and, therefore, not in restricted form), then the problem is undecidable. These results also correct some wrong statements in Durgin et al., JCS 12 (2004), 247-311. © 2008 - IOS Press and the authors. All rights reserved.

Publication Date

1-1-2008

Publication Title

Journal of Computer Security

Volume

16

Issue

6

Number of Pages

689-712

Document Type

Article

Personal Identifier

scopus

DOI Link

https://doi.org/10.3233/JCS-2007-0306

Socpus ID

55849092558 (Scopus)

Source API URL

https://api.elsevier.com/content/abstract/scopus_id/55849092558

This document is currently not available here.

Share

COinS