INTRODUCTION
With the rapid development of network technology and Web technology, Internet
has a strong influence on all kinds of aspects in society. Many transactions
have been processed through web-based applications. In order to protect the
web-based applications against passive and active attacks, TLS protocol (http://tools.ietf.org/html/rfc5246)
is widely deployed. The latest version is TLS 1.2. The objective of TLS 1.2
protocol is to provide confidentiality and authentication between two communicating
parts. So, people have paid a close attention to analysis and verification of
its security properties and want to get more confidence on it.
For the sake of analyzing and proving the security properties of security protocols
and strengthening the confidence of the people, two approaches have been proposed
form the beginning of the 1980s (Meng, 2011). One is
symbolic model which is also called Dolev-Yao model and in which cryptographic
primitives are abstracted as perfect black boxes. Until now lots of mechanized
tools in this model have been developed, for example, Casper, Isabelle, ProVerif
and Scyther. In 2005 Ogata and Futatsugi (2005) formally
analyzed in symbolic model TLS protocol with CafeOBJ method based on equational
reasoning. But the results of proof based on symbolic model are not quite clear.
The other approach is computational model based on complexity and probability.
The attacker in computational model is modeled as a probabilistic polynomial-time
machine. The computation model is more realistic but it is difficult to mechanized
proof until the introduction of mechanized tool Crypto verif (Blanchet,
2008) which is the first mechanized tool with computational model. In 2012,
(Jager et al., 2012) firstly analyzed by hand
TLS protocol where Cipher suite is ephemeral Diffie-Hellman key exchange protocol
in standard model. In 2013, (Fournet et al., 2013)
used F7 refinement typechecker to verify security properties of TLS protocol
implementation.
According to the related references, analysis of security of TLS 1.2 protocol
where Cipher Suite is RSA encryption with mechanized tool in computational model
is not found.
Owning to the previous analysis of TLS 1.2 protocol is not quite clear, in
this study, Blanchet calculus is used to analyze TLS 1.2 protocol where Cipher
suite is RSA encryption with mechanized tool Crypto verif.
CONTRIBUTION AND OVERVIEW
During the past several years TLS protocol bas been implemented and widely
deployed in many web-based applications. For the sake of verifying the security
properties of security protocols and improving the confidence on its security,
symbolic model and computational model have been developed. Symbolic model is
also called Dolev-Yao model; computational model is based on complexity and
probability. The later model is more realistic owning to that the attacker is
modeled as a probabilistic polynomial-time machine. According to the related
references, until now it is not existence that security analysis of TLS 1.2
protocol where Cipher suite is RSA encryption with mechanized tool in computational
model.
So analysis of security properties of TLS 1.2 protocol where Cipher suite is
RSA encryption with mechanized tool in computational model plays an important
role in security protocol field and is a significant work. Hence in this study,
Blanchet calculus is used to analyze TLS 1.2 protocol where Cipher suite is
RSA encryption with mechanized tool.
The main contributions of this study are summarized as follows:
| • |
The status of analysis in TLS1.2 protocol including in symbolic
model and in computational model is presented. Until now it is not existence
that analysis security of TLS 1.2 protocol where Cipher suite is RSA encryption
with mechanized tool in computational model |
| • |
Applying Blanchet calculus in computational model with active adversary
for mechanized verification of TLS 1.2 protocol where Cipher suite is RSA
encryption. Authentication is expressed by non-injective or injective correspondence.
Figure 1 shows the model of mechanized verification of
TLS 1.2 protocol where Cipher suite is RSA encryption |
| • |
The result shows that TLS 1.2 protocol where cipher suite is RSA encryption
has confidentiality of pre master key and authentication from server to
client. The first mechanized verification on TLS 1.2 protocol where cipher
suite is RSA encryption in computational model of in active adversary is
implemented in this study |
RELATED WORK
In this part the status quo of the proof in TLS protocol and its implementation
based on symbolic model and on computational model is presented. Until now there
does not exist that analysis of TLS 1.2 protocol with mechanized tool in computational
model.
In 1996, Wagner and Schneier (1996) analyzed Secure
Sockets Layer (SSL) 3.0 which is the former version of TLS protocol with informal
method. They found some active attacks which mainly include change cipher spec-dropping,
Key exchange algorithm spoofing and version roll-back attack.
In symbolic model (Paulson, 1999) uses Isabelle to
automatically analyze TLS protocol and proves its security claimed in TLS specification;
in 2005 (Ogata and Futatsugi, 2005) formally analyzed
TLS protocol with CafeOBJ method based on equational reasoning. The results
are that TLS protocol has the security properties with the condition pre-master
secrets cannot be leaked.
In computational model (Jonsson and Kaliski, 2002)
present an analysis of a variant of TLS hand shake protocol where Cipher suite
is RSA by hand. They argue that TLS should use Tagged Key-Encapsulation Mechanism
(TKEM) 1 rather than TKEM2; In 2008, (Morrissey et al.,
2008) analyzed TLS hand shake protocol in random model by hand. They firstly
proposed a security model for key agreement protocol and then analyzed TLS hand
shake protocol with the condition that Message Authentication Code (MAC) value
is send in the plaintext and showed that TLS key agreement protocol is secure.
|
| Fig. 1: |
Model of mechanized verification of TLS 1.2 protocol where
Cipher suite is RSA encryption |
However the version of TLS protocol with Diffie-Hellman Key Exchange is not
analyzed; In 2011 (Paterson et al., 2011) presented
the scheme of length-hiding authenticated encryption to analyze security of
TLS Record Protocol by hand. They found a new distinguishing attack against
TLS where variable length padding and short MACs are used; in 2012 Jager
et al. (2012) firstly analyzed by hand TLS protocol where Cipher
suite is ephemeral Diffie-Hellman key exchange in the standard model. They introduced
the authenticated and confidential channel establishment security model and
showed that the combination of the TLS hand shake protocol with the TLS Record
Layer can be proven secure.
Here the aspect of security properties of implementation of TLS protocol is
discussed. In 2009 Chaki and Datta (2009) presented
the first framework to automatically analyze authentication and secrecy of the
hand shake in Open SSL. In 2012, (Bhargavan et al.,
2012) firstly implemented TLS protocol 1.0 with language F#. And then they
designed a model extraction method to extract the abstract model. Finally, they
used Crypto verif to analyze security properties of TLS implementation in F#.
In 2013 (Fournet et al., 2013) developed a new,
verified, reference implementation of TLS protocol 1.2 with functional language
F#. And then they used the F7 refinement type checker to verify its security
properties and find a few new attacks.
REVIEW OF BLANCHET CALCULUS AND MECHANIZED PROOF TOOL CRYPTO VERIF
In this section there is a brief overview of Blanchet calculus (Blanchet,
2008) and the mechanized prover Crypto verif, formalize TLS 1.2 protocol
using it (http://www.Cryptoverif.ens.fr).
Blanchet calculus is a probabilistic polynomial calculus and has been developed
for the automated proof security protocols. In this calculus, messages are bitstrings
and cryptographic primitives are functions operating on bitstrings. Blanchet
calculus includes terms and processes.
The mechanized prover Crypto verif can directly prove security properties of
cryptographic protocols in the computational model in which the cryptographic
primitives are functions on bit-strings and the adversary is a polynomial-time
Turing machine. It also can prove secrecy properties and events that can be
executed only with negligible probability.
Crypto verif can works in two modes: A fully automatic and an interactive mode.
The interactive mode, requires a Crypto verif user to provide commands that
indicate the main game transformations. Crypto verif is sound about the security
properties it shows in a proof but properties it cannot prove are not necessarily
invalid.
REVIEW OF TLS 1.2 HAND SHAKE PROTOCOL
TLS 1.2 protocol mainly consists of hand shake protocol and Record protocol
which play a very important role in TLS protocol. TLS Record Protocol is a layered
protocol and accepts messages from higher level layer to be transmitted and
partitions the data into blocks and transmits the result. Received data is processed
inversely and then delivered to higher level clients. TLS 1.2 hand shake Protocol
is one of the defined higher-level clients of TLS 1.2 Record protocol and is
used to establish a secure session between server and client. In other words
TLS 1.2 hand shake protocol can provide the authentication from server to client
and confidentiality of pre master key. Figure 2 describes
the messages exchanged between server and client in the simplification of TLS
1.2 hand shake protocol.
In TLS 1.2 hand shake protocol there are two communicating parties involved.
One is client, the other is server. Client and server use TLS 1.2 hand shake
protocol to share a common key and server use TLS 1.2 hand shake protocol to
authenticate identity of client. The simplification of TLS 1.2 hand shake protocol
contains seven messages which are client hello, Server hello, Server certificate,
Server hello done, client key exchange, Client finished and Server finished:
When a client wants to connect to a server, TLS 1.2 hand shake protocol requires
client to send the Client hello message. Client hello mainly includes client_version,
client_random, session_id, cipher_suites, compression_methods and extensions.
Client_version parameter describes the version of the TLS protocol through which
the client wants to communicate with server during this session. Client_random
parameter describes the structure generated by client who is used to prevent
against replay attacks and to compute the master key. Session_id parameter is
an important parameter in client hello message.
|
| Fig. 2: |
TLS 1.2 hand shake protocol |
It describes the Identity (ID) of a session that the client wants to use for
this connection. Cipher_suites parameter describes that a list of the cryptographic
options supported by the client. Compression_methods parameter describes the
compression methods supported by the client. Extensions parameter describes
some extended functions need to be supported by server. The client generates
Client hello message and sends it to server:
When the server receives the Client hello message, it then constructs the Server
hello message. Server hello message mainly includes server _version, server_random,
session_id, cipher_suites, compression_methods and extensions. Server generates
message Server hello according to the message Client hello. Server_version parameter
is generated with the condition that the lower of that required by the client
in client_version in message Client hello and the highest supported by the server.
Server_random parameter describes the structure generated by server which is
used to prevent against replay attacks and to calculate the master key. Session_id
parameter describes that the server finds the session id from the cache according
to the session id from the Session_id in message Client hello. Cipher_suites
parameter is from the cipher_suites in Client hello message. Here the value
of Cipher_suites is RSA public encryption. Compression_methods parameter is
from the compression_methods in Client hello message. Extensions parameter is
from the extensions in Client hello message. After the server constructs message
server hello, it sends it to the client.
After the server sends the message server hello to the client, he constructs
the message Server certificate to the client. The message Server certificate
is used to tell the public key of the server to the client. The message Server
certificate mainly contains version, serial Number, algorithm identifier, issuer,
utcTime, server_subject_name, server_subject_key_info and signature. Here the
server_subject_name and server_subject_key_info parameters are mainly introduced.
Server_subject_name parameter is the name of server which is the owner of certificate.
|
| Fig. 3: |
Cryptographic assumptions |
Server_subject_key_info parameter mainly includes the public key of the server
and the related information on the public key:
Server hello done: = Server hello done |
(4) |
After the server sends the message server certificate, he constructs the message
server hello done and sends it to the client. The server hello done message
is sent by the server to show that the end of the server hello and associated
messages. After sending server hello done message, the server will wait for
a client response:
Client key exchange: = Client key exchange
||Encrypted pre master secret
|
(5) |
After it receives the server hello done message, client key exchage message
is sent by the client. Client key exchage message is the key message in TLS
1.2 hand shake protocol which is used to tell the pre Master key to the client
in a secure way. Client key exchage message mainly includes key exchange algorithm
and encrypted pre master secret parameters. With this message, the pre master
key confidentiality is implemented by transmission of the RSA-encrypted pre
Master key used here. Key exchange algorithm parameter describes the key exchange
algorithm. The value of key exchange algorithm is RSA. Encrypted pre Master
secret parameter describes the structure of pre Master key confidentiality.
Pre_master_secret is generated by the client and is used to generate the master
secret:
Client finish: = Client finish |
(6) |
Client finished message is always sent immediately to the server when the verification
of the key exchange and authentication processes were successful. The server
must verify that the contents are correct. Once the client has sent client finished
message and received and validated the Server finished message from the server,
the client may begin to send and receive application data over the connection:
Server finished: = Server finished |
(7) |
A Server finished message is always sent immediately to the client when the
verification of the key exchange and authentication processes were successful.
The client must verify that the contents are correct. Once the server has sent
server finished message and received and validated the client finished message
from the client, the server may begin to send and receive application data over
the connection.
FORMALIZING TLS 1.2 HAND SHAKE PROTOCOL IN BLANCHET CALCULUS
When TLS 1.2 hand shake protocol is formalized it assumes that public-key encryption
is indistinguishability under adaptive chosen ciphertext attacks. Public key
signature is unforgeable against chosen-message attack. Symmetric encryption
is indistinguishability under chosen-plaintext attacks and probabilistic symmetric
encryption. Hash function including hash functions defined by us according to
the requirements is collision resistant and unforgeability against adaptive
chosen messages attacks. Figure 3 describes the cryptographic
assumptions in our analysis of TLS 1.2 hand shake protocol.
|
| Fig. 4: |
Query events and secret |
|
| Fig. 5: |
TLS 1.2 hand shake protocol process |
Here non-injective correspondences and injective correspondences are used to
model authentication from server to client. Firstly non-injective correspondences
are used: Event server(x) =>inj: client(x) is used to authenticate client
by server. Then injective correspondences are used: Event inj: event server(x)
=> inj: client(x) is used to authenticate client by server. Figure
4 describes the events and correspondence. Query secret pre master secret
is used to query the secrecy of pre master secret.
The complete formal model of TLS 1.2 hand shake protocol where Cipher suite
is RSA encryption in Blanchet calculus is given in Figure. Figure
5-8 reports the basic processes include initator process,
client process and server process in authentication and secrecy forming the
model of TLS 1.2 protocol. The process TLS 1.2 process in Fig.
5 is assumed to run in interaction with an adversary which also models the
network.
Initator process generates server’s
public key pkeyrsa and private key signp key for encryption in RSA scheme and
public key signs key and private key signs key, for digital signature in RSA
cryptosystem. Finally, it sends signp key hash by the public channel c.
In detail initator process in Fig. 6 firstly generates server’s
public key rsaky seed in the following procedure: Initator process receives
a null message on channel start, sent by the adversary. Then, it chooses randomly
with uniform probability a bitstring seed one in the type rsakey seed, by the
construction new seed one: Rasaky seed. A type T, such as raskeyseed, aims at
denoting a set of bitstrings. Then, initator process generates the server’s
public key pkeyrsa corresponding to the coins seed one, by calling the public-key
generation algorithm rsapkgen (seed one). Similarly, initator proccess generates
the secret key skeyrsa by calling rsaskgen(seed one).
After that initator process generates the server’s
public key signp key and private key signs key for digital signature in RSA
scheme in the following procedure: Initator process chooses randomly with uniform
probability a bitstring seed two in the type by the construction new seed two:
Key seed. Then, initator process generates the server’s
public key signp key corresponding to the coinsseed two, by calling the public-key
generation algorithm pkgen (seed two). Similarly, initator process generates
the secret key signs key by calling skgen (seed two). At the same time it produces
the hash key key hash in type hash key by the construct new key hash: Hash key.
Finally, it sends pkeyrsa, signp key, hash by the public channel c. After sending
this message, the control passes to the receiving process which is part of the
adversary. Several processes are available, which represent the roles of client
and server process. (|(!n1client process)|(!n2server
process)) is the parallel composition of client process |!n1client
process, server process |!n1Server process. It makes simultaneously
available the processes.
Client process is modeled as client process in Blanchet calculus in Fig.
7. Client process generates the client-version Client version in type version
by the construct new client version: Version, client-random client random in
type by the construct new client random: random and cipher-suites client Cipher
suitesin type cipher_suites by the construct new client cipher suites: Cipher_suites.
And then it produces Client Hello message message one in type message using
the function concat A (client version, client random, null, client cipher suites)
by the construct let message one: Message = concat A (client version, client
random, null, client phersuites) in. Finally, it sends message one, one message
on by the public channel through the construct 
⟨one, message one⟩.
After that client process receives the message two, message two_s in type message
from the public channel c2 through the construct c2 (= two, message two_s: Message).
And then it gets the version agreement_version in type version, server_random
in type random, sessionid_s in type session_id and cipher_suites suites_s in
type cipher_suites through the function concat A (Agreement_version: Version,
server_random: random, sessionid_s: Session_id, suites_s: Cipher_suites) by
the construct let concat A (Agreement_version: Version, server_random: Random,
sessionid_s: Session_id, suites_s: Cipher_suites) = message two _s in. Client
process sends the message = three, message three_s: Message, sign one_s: Signature
in the public channel c3 by the construct ******.
And then client process gets the digital signature sign one_s: Signature of
message message three_s: message through the public channel c3 by the construct
c3 = (= three, message three_s: message, signone_s: signature. It uses the function
check () to verify the digital signature signone_s: signature of messag emessage
three_s: message. If the verification is successful, then it gets certificate
version certify version: Certificate version, server subject name name_s: subject
name and certificate certify_info: Certificate using the construct let concat
B (Certify version: Certificate version, name_s: subject name, certify_info:
Certificate) = message three_s: in. Then it gets the public key pkeyrsa_s: rsapkey
of the server and the algorithm name_algorithm: algorithm name from certificatecertify_info:
Certificate using the construct let concatinfo (pkeyrsa_s: rsapkey, name_algorithm:
algorithm name) = certify_info.
After that client process receives the message message our_s: message through
the public channel c4 by the constructc4 (= four, message our_s: Message). If
the message message our_s: Message is server hello Done then it creates the
pre master key pre master secret in type using the construct new pre Master
secret: kay and uses the RSA encryption one() to encrypt it with public key
pkeyrsa_s by the construct let message five: Message = one (key toclear text
(pre Master secret), pkeyrsa_s, s2 and gets the message message five in type
message.
Finally, it sends message message five by the public channel c5 using the
construct 
⟨ #= three, message three_s: message, sign one_s: Signature⟩.
Client process uses the function concatprf() to compute the hash input_s_random_c:
Input of message client random, server_random by the construct let c_s_random_c:
Input = concatprf (client random, server_random) in. And then it uses the function
cocat hash one () to calculate the hash input cocathashone of message message
one, message five by the construct let hash message_s: Hash input = cocat hash
one (message one, message five) in. Client process gets the master key master
secret_c: Key and uses the PRF function f() to generate the master key master
secret_keyc: Key by the construct let key to output (message secret_c: Key)
= f (pre master secret, master secret, c_s_random_c in. Also it use the PRF
function f() to compute by the construct let verify data: Output = f(master
secret_c, client finished, hash (key, hash, hash message_c)). Finally, it executes
the event event client (verify data) and send it through the public channel
c6 by the construct 
⟨six, verify data⟩.
Server process is modeled as server process in Blanchet calculus in Fig.
8. Server process receives the message one, message one_c: Message from
the public channel c7 through the construct c7 (= one, message one_c: Message).
And then it uses the function concat A to parse the message nessage one_c and
gets client versionclient version: Version, client random client_random: Random,
session id id: Session_id and cipher suite cipher suites: Cipher_suites by the
construct let concat A(client_version: Version, client_random: random, id, cipher_suites)-message
one_c in Server process checks id whether it defined and is equal to sessionid
or not by the construct find I<=N such that defined (session id [i] &&
(session id [i] = id). If the result is ok, then it stores id into id_store:
Session_id using the construct let id_store: Session_id = id in. If is null,
then server process generates a new session id in type session_id by the construct
new session id: session_id and stores it into id_store by the construct let
id_store = session id. At the same time if client_version is equal to agreement
version, then it creates a random number server random by the construct new
server random: random and use the function cancat A () to compute the message
message two: Message by the construct let message two: message two: Message
= concat A (Agreement version, server random, id_store, suites in. Server process
sends message message two by the public channel c8 through the construct 
.
Server process generates the subject name name: Subject name of certificate
by the construct new name: Subject name and the subject algorithm of certificate
subject algorithm: Algorithm name by the construct new subject algorithm: Algorithm
name. At the same time it uses function concatinfo () to generate certificate
information certificate info: Certificate by the construct let certificate info:
Certificate = concatinfo (pkeyrsa, subject algorithm in and uses the function
concat B() to compute the message message three: Message by the construct let
message three: Message = concat B (certify name, certificate info) in. And then
it generates the digital signature sign one: signature of the message message
three: Message using the digital signature function sign () by the construct
let sign one: Signature = sign (message three, signs key, r1) in. It also sends
message three, sign one through the public channel c9 by the construct 
⟨three, message three, sign one⟩ and sends four, server Hello Done
through the public channel c10 by the construct 
.
Server process receives the message message five_c: Message from the public
channel c11 by the construct c11 (= five, message five_c: message). It uses
the RSA decryption dec() to decrypt message five: Message and gets the pre master
key pre master_secret: key by the construct let injbot (key to clear text (pre
master_secret: key)) = dec (message five_c, skeyrsa) in.
After that server process receives the messageverify data_fc: Output from the
public channel c12 with the constructc12 (= six, verify data_fc: Output). It
uses the function concatprf to compute the c_s_random_s by the construct let
c_s_random_s: input = concatprf (client_random, server random) in and uses the
PRF function to calculate the master key master secret_s: key by the construct
let key to output (master secret_s: key) = f(pre master_secret, master secret,
c_s_random_s) in. At the same time it computes the hash input hash message_fc
by the function cocat hash one() through the construct let hash message_fc:
Hash point = cocat hash one (message one_c, message five_c) in. If verify data_fc
is equal to output of the function f(master secret_s, client finished, hash
(key hashm hash message_fc)), then it uses the function cocat hash two () to
compute the hash input hash message: hash input by the construct let hash messageL
hash input = cocat hash two (message two, message three, server hello, done)
in. Finally, it executes the event event server (verify data_fc) and sends the
message f(master secret_s, server finished, hash(key hash, hash message)) by
the public channel c13 by the construct 
(seven, f(master secret_s, server finished, hash (key hash, hash message))).
MECHANIZED VERIFICATION OF SECRECY AND AUTHENTICATION IN TLS 1.2 HAND SHAKE
PROTOCOL WITH CRYPTO VERIF
The inputs of Crypto verif have two formats. One is channels Front-end. The
other is oracles Front-end. In both cases, the output of Crypto verif is same.
The main difference between the two inputs is that the oracle front-end is based
on oracles and the channel front-end is based on channels.
In this study, channel Front-end is used as the input of Crypto verif. Hence
formal model of TLS 1.2 hand shake protocol where Cipher suite is RSA encryption
must transform into the syntax of Crypto verif and generate the Crypto verif
inputs in the form of channels Front-end.
Here non-injective correspondences and injective correspondences in Table
1 are used to model the authentication from server to client. First non-injective
correspondences are used: event event server(x) ==> client(x) authenticate
client by server. And then Injective correspondences are then used: event inj:
event server(x) ==>inj client(x) authenticate client by server.
From Fig. 9-11, the inputs of verification
of authentication and secrecy in Crypto verif are presented. The analysis was
executed by Crypto verif and succeeded.
| Table 1: |
Correspondences in TLS1.2 protocol |
 |
|
| Fig. 9: |
Inputs of TLS1.2 protocol in cryp to verif |
|
|
|
| Fig. 10: |
Inputs of TLS1.2 protocol in cryp to verif |
|
|
|
| Fig. 11: |
Inputs of TLS1.2 protocol in crypto verif |
|
| Fig. 12: |
Authentication of TLS 1.2 protocol in crypto verif |
|
| Fig. 13: |
Secrecy of TLS 1.2 protocol in crypto verif |
The results show in Fig. 12 and 13. TLS
1.2 protocol where Cipher Suite is RSA encryption is proved to guarantee authentication
from server to client and the secrecy of pre master key in computation model.
CONCLUSION
During the past several years TLS protocol bas been implemented and deployed
widely in many web-based applications. According to the related references,
until now it is not found that security analysis of TLS 1.2 protocol where Cipher
suite is RSA encryption with mechanized tool in computational model. Hence,
in this study, Blanchet calculus in computational model is used to analyze TLS
1.2 protocol where Cipher suite is RSA encryption with mechanized tool. The
result shows that it has confidentiality of pre master key and authentication
from server to client. The first mechanized verification on TLS 1.2 protocol
where Cipher suite is RSA encryption in computational model of in active adversary
is executed.
In the near future the verification of the Java implementation of TLS 1.2 protocol
in computational model is very interesting.
ACKNOWLEDGMENT
This study was supported in part by Natural Science Foundation of The state
Ethnic Affairs Commission of PRC under the Grants No: 12ZNZ008, titled “Automatic
Verification of Cryptographic Security in Security Protocol Java Code”,
conducted in Wuhan, China from 1/1/2013 to 30/12/2013.
