Transformation techniques for constraint logic programs with applications to protocol verification