Model Checking Timed Automata pada proses Authentikasi Security Protocol Pada Jaringan Berbasis Nirkabel

ABSTRAKSI: Protokol authentikasi EAP MD5 dan EAP TLS adalah protokol keamanan yang masih sering dijumpai pengunaannya saat ini. Protokol Keamanan tersebut menggunakan proses authentikasi pada jaringan nirkabel dengan menggunakan IEEE 802.1x sebagai media transmisinya. Terdapat 3 komponen yang berperan pada IEEE 802.1x yaitu suplican , authenticator dan authentication server. Ketiga komponen inilah yang akan dimodelkan dengan menggunakan timed automata untuk melihat kondisi yang terjadi jika dilakukan serangan dengan menggunakan man in the middle attack dan dilakukan penambahan aspek waktu pada protokol tersebut. Salah satu bentuk pengecekan terhadap model adalah dengan menggunakan timed automata. Timed Automata adalah finate automata klasik yang dapat memanipulasi waktu, berkembang terus menerus dan mensinkonisasikan dengan waktu mutlak[2]. Tugas akhir ini mengkhususkan diri pada proses memodelkan protokol authentikasi EAP MD5 dan EAP TLS dengan menggunakan Timed Automata dengan menambahkan kemungkinan retransmisi berdasarkan aspek waktu. Setelah model selesai maka berikutnya dilakukan pengecekan terhadap model berdasarkan aturan yang ada apakah dapat berjalan sesuai dengan aturan tersebut. Dari hasil verfikasi model tersebut dengan menggunakan alat UPPAAL maka dapat dilihat bahwasannya protokol authentikasi EAP MD5 dan EAP TLS dapat dimodelkan dengan menggunakan timed automata dan sesuai dengan aturan yang terdapat pada RFC protokol tersebut.Kata Kunci : EAP MD5, EAP TLS, Timed Automata, UPPAALABSTRACT: Authentication protocols EAP MD5 and EAP TLS are security protocols that are still frequently encountered use today. This Security Protocol using the process of authentication on a wireless network using the IEEE 802.1x as the transmission medium. There are three components that use a role in the IEEE 802.1x are suplican, authenticator and authentication server. These three components will be modeled using timed automata to see the condition that occurs when an attack carried out by using the man in the middle attack and carried out additional aspects of the time in the protocol. One form of model checking is use timed automata. Timed automata are classic finate automata that can manipulate time, developing continuously and synchronously with the absolute time [2]. This final project focuses on the modeling process authentication protocols EAP MD5 and EAP TLS using Timed Automata with the added possibility of retransmission based on the aspect of time. Once completed, the next model to be checked against an existing model based on whether the rules can be run in accordance with these rules. From the results verify the model using UPPAAL tool, it can be seen authentication protocols EAP MD5 and EAP TLS can be modeled using timed automata, and in accordance with the rules contained in the RFC protocol.Keyword: EAP MD5, EAP TLS, Timed Automata, UPPAA