Formal Analysis of EAP-TLS Protocol Based on Logic of Events

The Extensible Authentication Protocol–Transport Layer Security (EAP-TLS) is a critical authentication protocol for wireless networks and secure IoT communications. However, it faces significant challenges from man-in-the-middle attacks, including message tampering, replay, and certificate forgery. Although model checking techniques have been applied to verify its security properties, the complexity of the EAP-TLS handshake often prevents accurate formal modeling; existing studies rarely assess the communication overhead of protocol enhancements. Moreover, traditional Logic of Events Theory (LoET) struggles to handle transport-layer protocols like EAP-TLS due to their intricate interaction processes. This study proposes a novel formal analysis approach, extending LoET by expanding five event classes, formulating corresponding rules, and introducing new axioms. Formal verification reveals attack paths involving plaintext theft, message tampering, and entity impersonation. The research proposes an enhanced strategy to mitigate these vulnerabilities through hash merging, encryption, and signature methods, alongside analyzing their communication costs to ensure feasibility. Using the extended LoET, the improved protocol is rigorously proven to satisfy strong authentication, thereby enhancing practical security. The proposed method achieves a time complexity of O(n2) and demonstrates superior performance in resisting state explosion compared with related approaches, thus establishing a more efficient and robust framework for EAP-TLS security analysis.