Automatic SAT-Compilation of Protocol Insecurity Problems via Reduction to Planning