The Transport Layer Security protocol (TLS) provides privacy for transmissions between two communicating applications. This protocol standardizes a revision of the Secure Socket Layer 3.0 protocol (SSL) by the Internet Engineering Task Force (IETF) Network Working Group. TLS supports a selection of cryptographic algorithms pertaining to key exchange, encryption, hashing, and digital signatures. A set of cipher-suites defines the different combinations of algorithms allowed within one session while a subprotocol implements the selected cipher-suite. TLS is based on previous versions of the SSL protocol developed by Netscape. Much of the current consumer commerce performed on the Internet utilizes the SSL protocol. Despite the widespread use, formal analysis of these protocols has been scant. Paulson's method was more powerful in that it allowed optional messages and fields within a single protocol. The scope of the formal analysis was limited to examination of individual sub-protocols and, consequently, the analysis is blind to attacks that interleave two sub-protocols. The TLS protocol is partitioned into two layers, labeled the TLS Record Protocol and the TLS Handshake Protocol. The TLS Record Protocol provides the encryption and message authentication for each message. The TLS Handshake Protocol operates on top of the TLS Record Protocol. A TLS handshake supplies the authentication and key exchange operations for the TLS protocol. The security state agreed upon in the handshake is then used by the TLS Record Protocol to provide session security. Typical security protocols have a single sequence of messages that are sent between the two principals. In TLS, the principals are referred to as the client (C) and the server (S). The client and the server must choose from a set of cipher-suites that can require different sequences of actions and messages within the protocol. For example, Diffie-Helman key agreement requires both principals to exchange public values that are used to compose a private session key, while RSA public key exchange relies on the client alone to choose, encrypt and deliver an appropriate private session key. The cipher-suite defines multiple characteristics such as the key exchange algorithm, the hashing method, and the digital signatures to be used in the handshake. Each characteristic requires different actions within the protocol depending upon which method is chosen. The TLS protocol offers a choice of several possible protocol characteristics. The Diffie-Helman and RSA key exchange methods comprise the TLS secure key exchange methods. Other characteristics of key exchange include the use of smaller encryption keys for export versions, and a choice between fixed or ephemeral keys. Two signature methods, DSS and RSA can be used with Diffie-Helman key exchange while only RSA signatures are used with RSA key exchange. In addition, key exchange may be anonymous with the use of Diffie-Hellman. The authentication of the client and server is also flexible. This means that in a TLS session there may be no authentication with certificates, only the server is provided a certificate, or that both the server and the client are provided certificates. For hashing requirements, MD5 or SHA may be chosen. In addition to the full handshake, by including an acceptable old session identifier, a session may be resumed quickly by using the previously agreed upon security values. The cipher-suite message also specifies the type of encryption to be used for the session once the handshake is completed.