The Insecurity Problem: Tackling Unbounded Data

In this paper we focus on tackling the insecurity problem of security protocols in the presence of an unbounded number of data such as nonces or session keys. First, we pinpoint four open problems in this category. The first two problems concern protocols with natural restrictions that any "realistic\´ protocol should satisfy while the second two concern protocols with disequality constraints. For protocols with disequality constraints we will prove: (1) Insecurity is decidable in NEXPTIME when bounding the size of messages and not requiring data to be freshly generated. (2) Insecurity is NEXPTIME-complete when bounding the size of messages and the number of freshly generated data used in honest sessions. This shows that unbounded data can be tackled in settings which do not trivially reduce to the case of bounded data. The second result is in contrast with a recently published proof, which appears to prove the same problem undecidable. We will point out why this proof cannot be considered to be valid.