Formal Analysis of the TLS Handshake Protocol

Hanane Houmani, Mourad Debbabi

2012

Abstract

Most applications in the Internet as e-banking, e-commerce, e-maling, etc., use the Secure Sockets Layer (SSL) or Transport Layer Security (TLS) protocol to protect the communication channel between the client and the server. That is why it is paramount to ensure the security objectives such as confidentiality, authentication and integrity of the SSL/TLS protocol. In this paper we prove the confidentiality (secrecy) property of the SSL/TLS handshake protocol which consititues the main core of the SSL/TLS protocol. To perform this analysis, we introduce a new funcion called DINEK function that safeltly estimates the security level of messages. More precisely, this function which shares a conceptual origin with the idea of a rank function, allows to estimate a security level of a message (including the unknown messages) according to the interaction between the protocol and the intruder. This function could not be used only to verify the TLS protocol as we will show in this paper, but also to verify the secrecy property for large class of protocols and in particular Key Agreement protocols. The verification using the DINEK function is proven in this paper for unbounded number of sessions and unbounded number of nouces.

Paper Citation

in Harvard Style

Houmani H. and Debbabi M. (2012). Formal Analysis of the TLS Handshake Protocol . In Proceedings of the International Conference on Security and Cryptography - Volume 1: SECRYPT, (ICETE 2012) ISBN 978-989-8565-24-2, pages 192-205. DOI: 10.5220/0004075101920205

in Bibtex Style

@conference{secrypt12,
author={Hanane Houmani and Mourad Debbabi},
title={Formal Analysis of the TLS Handshake Protocol},
booktitle={Proceedings of the International Conference on Security and Cryptography - Volume 1: SECRYPT, (ICETE 2012)},
year={2012},
pages={192-205},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0004075101920205},
isbn={978-989-8565-24-2},
}

in EndNote Style

TY - CONF
JO - Proceedings of the International Conference on Security and Cryptography - Volume 1: SECRYPT, (ICETE 2012)
TI - Formal Analysis of the TLS Handshake Protocol
SN - 978-989-8565-24-2
AU - Houmani H.
AU - Debbabi M.
PY - 2012
SP - 192
EP - 205
DO - 10.5220/0004075101920205