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