Title
Selecting theories and nonce generation for recursive protocols
Abstract
Truderung's selecting theory model is one of the few models of cryptographic protocols which allows to model iterative (recursive) computations of principals and, at the same time, an automatic analysis in the following sense: there exists a procedure that checks whether in all runs of a given protocol a certain message is not revealed to an intruder. A major drawback of Truderung's model is that it allows only a finite number of constants, that is, there is no mechanism by which a principal can generate an unbounded number of fresh tokens such as nonces or session keys. We extend Truderung's model by such a mechanism and show that the extended model still allows an automatic analysis. We also demonstrate that the extended model is more appropriate to model the Recursive Authentication Protocol. It is important to know that after publication of Truderung's result it became clear that his proof only works in a restricted setting. We show that there is no hope to find a remedy to this by proving that the secrecy problem in the unrestricted setting is undecidable. In light of this, the aforementioned result about extending Truderung's model is to be read as follows. Adding anonymous constants in the restricted setting leads to a model of cryptographic protocols where insecurity is decidable.
Year
DOI
Venue
2007
10.1145/1314436.1314445
FMSE
Keywords
Field
DocType
model iterative,extended model,finite number,selecting theory model,selecting theory,restricted setting,aforementioned result,recursive protocol,nonce generation,cryptographic protocol,unrestricted setting,automatic analysis,unbounded number,decidability,security protocol,security protocols,authentication protocol
Existential quantification,Cryptographic protocol,Computer science,Algorithm,Decidability,Theoretical computer science,Authentication protocol,Recursion,Cryptographic nonce,Universal composability,Undecidable problem
Conference
Citations 
PageRank 
References 
6
0.42
11
Authors
3
Name
Order
Citations
PageRank
Klaas Ole Kürtz160.42
Ralf Küsters2101469.62
Thomas Wilke31028.76