Selecting Theories and Nonce Generation for Recursive Protocols
K. O. Kürtz, R. Küsters, and Th. Wilke
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.