Navy Research Laboratory (NRL) Protocol Analyzer

Posted by Ae89 on Sabtu, 08 Mei 2010 | 0 komentar

index1.php
Protokol kriptografi merupakan protokol komunikasi yang menggunakan fungsi enkripsi dengan tujuan untuk distribusi kunci kriptografi, autentikasi pihak-pihak yang saling berkomunikasi dalam sebuah jaringan yang rawan terhadap berbagai kemungkinan serangan yang berusaha untuk menggagalkan tujuan dari suatu protokol. Sebagai contoh adalah kerawanan terhadap usaha pencurian session key yang akan digunakan untuk komunikasi. Namun, tidak selamanya suatu protokol selalu aman. Setiap protokol pastilah mempunyai kekurangannya masing-masing. Karena berbagai kekurangan yang dapat terjadi itu, maka biasanya protokol-protokol autentikasi tersebut biasanya mengikuti standar dari ISO yang menyarankan penggunaan public key cryptosystem di dalamnya. Dengan penggunaan public key ini setiap orang bisa mengirimkan pesan rahasianya dengan enkripsi menggunakan public key dan setiap penerima pesan bisa melakukan dekripsi menggunakan private key-nya, juga termasuk untuk proses signing pesan menggunakan private key pengirim pesan, yang nantinya akan diverifikasi oleh receiver menggunakan public key sender.
Jikalau analisis IKE pernah dilaksanakan oleh R. Canetti dan H. Krawczyk dengan berbasis matematis untuk pertama kalinya, Zhou berbasis non-matematis, maka Meadows menggunakan Navy Research Labs (NRL) protocol analyzer yang merupakan sebuah sistem yang handal untuk menganalisis protokol keamanan yang ditulisnya dalam sebuah prolog. Lebih jelasnya, NRL protocol analyzer ini merupakan merupakan suatu prototipe tool yang bertujuan untuk melakukan fungsi verifikasi. IKE dianalisis untuk suatu prinsip kerahasiaan, autentikasi maupun perfect forward secrecy (PFS), dalam hal ini adalah pada segi keamanan saat distribusi kunci di dalam jaringan. Dari sini dapat ditemukan beberapa permasalahan yang menjadi sumber serangan bagi IKE. Dengan memperhatikan pada sumber dan usaha yang dilakukan, kesimpulan yang dapat diambil dari analisis ini berdampak pada evolusi IKE menjadi IKEv2.
NRL Protocol Analyzer telah diterapkan di antara Quintus Prolog dan SWIProlog serta pada titik ini terdiri dari sekitar 4.000 baris kode. Terlebih dulu, para Analyzer tidak lebih dari memberikan penjelasan lengkap mengenai semua state yang bisa segera mendahului state tertentu. Versi Analyzer ini digunakan untuk memverifikasi beberapa protokol sederhana. Sementara Analyzer dalam hal ini, beberapa prosedur umum untuk membuktikan state  yang tidak terjangkau untuk dikembangkan.
Meskipun Analyzer masih agak rumit untuk digunakan, kita dapat menemukan cacat yang tidak bisa diketahui sebelumnya dalam dua protokol seperti: Simmons broadcast selective protocol dan Burns Mitchell resource sharing protocol.
Biasanya beberapa tantangan bisa muncul saat kita menerapkan model checking terhadap analisis protokol kriptografi. Oleh karena itu, NRL Protocol Analyzer didesain dengan tujuan untuk mengimbangi tantangan-tantangan tersebut. NRL Protocol Analyzer bisa digunakan untuk membuktikan properti keamanan dari protokol kriptografi juga menentukan letak-letak lubang keamanan. Dalam keadaan tertentu, digunakan untuk menemukan cacat yang belum diketahui dalam Simons Selective Broadcast Protocol dan Burns Mitchell Resource Sharing Protocol dan cacat dari sebuah implementasi terpisah yang tidak diketahui dalam protokol reauthentication Neuman Stubblebine.
Protokol NRL Protocol Analyzer ini berdasarkan atas sebuah versi pada bagian yang pernah ditulis kembali oleh Dolev dan Yao, dimana diasumsikan seorang intruder mampu membaca semua lalu lintas pesan, memodifikasi maupun merusak message traffic dan juga melakukan operasi seperti layaknya user yang sah di dalam protokol. Namun bagaimanapun tetap ada beberapa kata/ secret word (kunci enkripsi) yang mana intruder belum mengetahuinya dan mencoba untuk menemukannya. Namun meskipun NRL Protocol Analyzer ini berbasiskan Dolev dan Yao, ada perbedaan pada pembuktian properti keamanan protokolnya.