{Protocol Specification and Verification by Using Computational Logic}