ABSTRAKSI: Perkembangan teknologi akses internet memasuki babak baru sejak adanya layanan akses wireless seperti hotspot. Dalam area ini, user dapat mengakses dengan perangkat yang mendukung teknologi wireless. Sejalan dengan perkembangan ini, berbagai protokol yang mendukung berbagai proses dalam teknologi ini dikembangkan dalam berbagai penelitian, proses autentikasi salah satunya, dan menghasilkan berbagai protokol, salah satunya EAP dan server autentikasi seperti RADIUS.
Walau demikian semakin meningkatnya teknologi protokol juga diimbangi dengan meningkatnya kemampuan para attacker dan software pendukungnya untuk menyerang protocol yang didesain untuk melindungi user yang terhubung pada server autentikasi.
Serangan man-in-the-middle adalah salah satu cara yang digunakan untuk menyadap data pribadi tersebut. Serangan ini berupa attacker akan berpura-pura sebagai authenticator (access point). Robustness sistem autentikasi berbasis EAP-MD5 pada jaringan wireless akan diuji dengan formal methods mengggunakan BAN Logic untuk membuktikan apakah serangan man-in-the-middle mampu mencari celah dalam protokol ini.Kata Kunci : EAP , BAN Logic , RADIUS , Man-in-the-Middle , Formal Methods.ABSTRACT: Internet access technology enters a new phase due to the rapid developments of wireless internet access, especially hotspots. Within this area, users can create connection and stay connected to the internet using hardware which supports wireless access from their devices. This popular service is also supported by various researchs over their process, including authentication process, which creates protocols such as EAP and authentication server like RADIUS.
Even then, the rapid development over protocol technology is balanced by attacker’s skill and advancement of their software support to break over the protocol designed to protect connected user.
Man-in-the-middle attack is one of the methods chosen to break over protocol. This attack consists of several attacking process, but ultimately attacker will be able to personificate the authenticator (access point). The robustness of EAP-MD5 based authentication system on wireless network will be tested using formal methods and BAN Logic to prove whether the attack could find its way around this protocol or not.
Keyword: EAP , BAN Logic , RADIUS , Man-in-the-Middle , Formal Methods.