Perpustakaan Digital ITB

Protokol Mobile Payment System memegang peranan penting pada proses transaksi finansial dengan metoda pembayaran elektronik. Suatu protokol harus dapat menjamin terpenuhinya empat aspek pokok kriptografi, yaitu confidentiality, integrity, authentication, dan non-repudiability. Selain keempat hal diatas, protokol juga harus dapat menangani hambatan yang timbul dari sifat protokol sebagai sebuah Finite State Machine (FSM), yaitu livelock, deadlock, non-progress, dan assertion consistency. SPIN sebagai sebuah perangkat lunak analisis protokol menyediakan fitur pemodelan protokol, dan kemampuan untuk melakukan simulasi dan verifikasi dalam melakukan analisis protokol. Penelitian Tugas Akhir ini bertujuan untuk merancang sebuah protokol MPS yang aman, dan bebas dari adanya protocol failure. Model pada SPIN ditulis dalam bahasa PROMELA, dan dengan implementasi dari beberapa klaim, akan memberikan hasil berupa status verifikasi protokol.