Automatic verification and symbolic analysis for 0-RTT security in TLS 1.3
Other Title(s)
التحقق الألى و التحليل الرمزي ل RTT-0 3.1 في بروتوكول أمان طبقة النقل TLS1.3
Dissertant
Thesis advisor
University
Birzeit University
Faculty
Faculty of Engineering and Technology
Department
Department of Computer Science
University Country
Palestine (West Bank)
Degree
Master
Degree Date
2018
English Abstract
Transport Layer Security (TLS) protocol is one of the most important and widely used cryptographic protocols that is introduced to provide secure communication over Internet.
However, over twenty years, attacks against TLS show weaknesses and pitfalls in the protocol design and implementation.
Therefore, Internet Engineering Task Force (IETF) is in continuous development to revamp the security of TLS by adding new security features to avoid the weakness of older protocol versions.
Many design goals were proposed in many fields of the TLS protocol to finally produce a new secure, reliable and fast version of this protocol, specifically, reducing the latency of the key exchange (KE) protocols while maintaining the security guarantees represented by forwarding secrecy.
To achieve this, zero round trip time (0-RTT) protocol is a candidate solution.
We explore a practical solution to protect the KE process and sends the early data in 0-RTT with full Perfect Forward Secrecy (PFS) and preventing the replay attack.
To this end, we analyze the 0-RTT handshake process using Diffie-Hellman and pre-shared keys in TLS1.3; by extending and updating a previous model of 0-RTT protocol in the TLS1.3 protocol specifications (RFC8446).
By studying related work which attempted to solve the PFS and replay attack using either puncture mechanism or Google Quick UDP Internet Connection (QUIC) protocol, we found that both solutions have significant performance drawbacks.
We present a new approach to implement 0-RTT based on TLS1.3 without sacrificing PFS.
We support the theoretical approach by practical tests using a Tamarin tool for symbolic modeling and analysis of TLS1.3 security protocols.
In the practical experiments, we simulate several attempts to break PFS using Tamarin component and we verify that the solution guarantees PFS.
Moreover, we deduce that attempting to solve the PFS problem by Diffie-Hellman using more than one key will require a fundamental change to the structure of Diffie-Hellman which ends up with a new protocol that need intensive reviews and studies
Main Subjects
Information Technology and Computer Science
Topics
No. of Pages
74
Table of Contents
Table of contents.
Abstract.
Abstract in Arabic.
Chapter One : Introduction.
Chapter Two : Transport layer security (TLS) foundation.
Chapter Three : Attacks on TLS.
Chapter Four : Tamarin prover for security protocols modeling.
Chapter Five : Modeling and analyzing of TLS 1.3 handshake modes.
Chapter Six : Conclusion.
References.
American Psychological Association (APA)
Abu Farhah, Fadi. (2018). Automatic verification and symbolic analysis for 0-RTT security in TLS 1.3. (Master's theses Theses and Dissertations Master). Birzeit University, Palestine (West Bank)
https://search.emarefa.net/detail/BIM-958501
Modern Language Association (MLA)
Abu Farhah, Fadi. Automatic verification and symbolic analysis for 0-RTT security in TLS 1.3. (Master's theses Theses and Dissertations Master). Birzeit University. (2018).
https://search.emarefa.net/detail/BIM-958501
American Medical Association (AMA)
Abu Farhah, Fadi. (2018). Automatic verification and symbolic analysis for 0-RTT security in TLS 1.3. (Master's theses Theses and Dissertations Master). Birzeit University, Palestine (West Bank)
https://search.emarefa.net/detail/BIM-958501
Language
English
Data Type
Arab Theses
Record ID
BIM-958501
