Perpustakaan Digital ITB

Pada penelitian sebelumnya yang telah dilakukan oleh saudara Mirza Azhari [11], telah terancang sebuah protokol mobile payment system yang terbukti memenuhi klaim atomicity, effectiveness, dan non-repudiation. Namun dalam prosesnya, protokol tersebut tidak memperhatikan keadaan network yang menjadi tempat berlangsungnya proses komunikasi pada protokol mobile payment system tersebut. Pada Tugas Akhir ini penulis menganalisis pengaruh faktor-faktor network seperti delay dan message lost pada protokol mobile payment system hasil penelitian sebelumnya [11]. Penulis kemudian mengembangkan protokol yang sudah ada tersebut dengan memasukkan unsur network dalam prosesnya. Protokol hasil pengembangan tersebut kemudian disimulasikan dan diverifikasi dengan menggunakan program SPIN model checker. Untuk bisa dijalankan pada program SPIN, model protokol dituliskan dahulu ke bahasa PROMELA (Process Meta Language). Bentuk bahasa PROMELA dari protokol kemudian dapat disimulasikan dan diverifikasi oleh SPIN. Hasil simulasi protokol dianalisis dengan menyesuaikan pada bentuk rancangan secara umum. Kemudian program SPIN memverifikasi Correctness properties dan Claim Transaction properties pada protokol yang bersangkutan. Dari hasil simulasi dan verifikasi, protokol yang telah dikembangkan terbukti memenuhi klaim atomicity dan non-repudiation.