Protocol Specification and Verification by Using Computational Logic