Deciding security properties for cryptographic protocols. Application to key cycles

Details Deciding security properties for cryptographic protocols. Application to key cycles Deciding security properties for cryptographic protocols. Application to key cycles

2007-08-27

arxiv.org/abs/0708.3564v2

Computer Science

Logic in Computer Science

revised version (corrected small mistakes, improved presentation); to be published in ACM Transactions on Computational Logic;

Scientific paper

There is a large amount of work dedicated to the formal verification of security protocols. In this paper, we revisit and extend the NP-complete decision procedure for a bounded number of sessions. We use a, now standard, deducibility constraints formalism for modeling security protocols. Our first contribution is to give a simple set of constraint simplification rules, that allows to reduce any deducibility constraint system to a set of solved forms, representing all solutions (within the bound on sessions). As a consequence, we prove that deciding the existence of key cycles is NP-complete for a bounded number of sessions. The problem of key-cycles has been put forward by recent works relating computational and symbolic models. The so-called soundness of the symbolic model requires indeed that no key cycle (e.g., enc(k,k)) ever occurs in the execution of the protocol. Otherwise, stronger security assumptions (such as KDM-security) are required. We show that our decision procedure can also be applied to prove again the decidability of authentication-like properties and the decidability of a significant fragment of protocols with timestamps.

Affiliated with

Also associated with

No associations

Rating

Deciding security properties for cryptographic protocols. Application to key cycles does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Deciding security properties for cryptographic protocols. Application to key cycles, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Deciding security properties for cryptographic protocols. Application to key cycles will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-126249