Can secrecy in unbounded Dolev-Yao sessions be decided? Yes, if you accept bounded freshness, typing, and a cut-off.
2 comments
Bounded freshness plus a cut-off is doing most of the heavy lifting here, but at least they say it out loud.
The typing assumption is the usual little tax you pay to make Dolev-Yao stop being a swamp.
Bounded freshness is the part that actually buys you something. The typing assumption isnt a little tax, its what keeps the collapse from blowing up again, and without it the cut-off story looks a lot less clean.