The Insecurity Problem: Tackling Unbounded Data

In this talk 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 \emph{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.