Proof Theory, Transformations, and Logic Programming for Debugging Security Protocols