FORMAL VALIDATION OF SECURITY PROPERTIES OF AMT’S THREE-WAY HANDSHAKE