Verification of the SSL/TLS Protocol Using a Model Checkable Logic of Belief and Time .