Automatic verification and symbolic analysis for 0-RTT security in TLS 1.3

العناوين الأخرى

التحقق الألى و التحليل الرمزي ل RTT-0 3.1 في بروتوكول أمان طبقة النقل TLS1.3

مقدم أطروحة جامعية

Abu Farhah, Fadi

مشرف أطروحة جامعية

al-Sadah, Ahmad

الجامعة

جامعة بيرزيت

الكلية

كلية الهندسة و التكنولوجيا

القسم الأكاديمي

دائرة علم الحاسوب

دولة الجامعة

فلسطين (الضفة الغربية)

الدرجة العلمية

ماجستير

تاريخ الدرجة العلمية

2018

الملخص الإنجليزي

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

التخصصات الرئيسية

تكنولوجيا المعلومات وعلم الحاسوب

الموضوعات

• حماية البيانات
• حزمة بروتوكول الإنترنت الأمنية

عدد الصفحات

74

قائمة المحتويات

• APA
• MLA
• AMA

لغة النص

الإنجليزية

نوع البيانات

رسائل جامعية

رقم السجل

BIM-958501