Can secrecy in unbounded Dolev-Yao sessions be decided? Yes, if you accept bounded freshness, typing, and a cut-off.