Sciweavers

FSTTCS
2003
Springer

Tagging Makes Secrecy Decidable with Unbounded Nonces as Well

13 years 8 months ago
Tagging Makes Secrecy Decidable with Unbounded Nonces as Well
Tagging schemes have been used in security protocols to ensure that the analysis of such protocols can work with messages of bounded length. When the set of nonces is bounded, this leads to decidability of secrecy. In this paper, we show that tagging schemes can be used to obtain decidability of secrecy even in the presence of unboundedly many nonces. 1 Background Security protocols are specifications of communication patterns which are intended to let agents share secrets over a public network. They are required to perform correctly even in the presence of malicious intruders who listen to the message exchanges that happen over the network and also manipulate the system (by blocking or forging messages, for instance). An obvious correctness requirement is that of secrecy: an intruder cannot read the contents of a message intended for others. The presence of intruders necessitates the use of encrypted communication. It has been widely acknowledged that even if perfect cryptographic to...
Ramaswamy Ramanujam, S. P. Suresh
Added 06 Jul 2010
Updated 06 Jul 2010
Type Conference
Year 2003
Where FSTTCS
Authors Ramaswamy Ramanujam, S. P. Suresh
Comments (0)