Identity authentication and secrecy in the pi-calculus and Prolog