Sitem pembayaran elektronis yang sangat berperan dalam dunia bisnis sangat memperbesar beban kerja bank. Bank harus terlibat pada proses pemindahan uang yang terjadi saat transaksi, sehingga volume kerja bank menjadi luar biasa besar pada waktu-waktu tertentu. Untuk membuat beban kerja tersebut tidak terpusat pada satu waktu, sistem pembayaran internet menggunakan verifikasi off-line tanpa melakukan hubungan bank. Urusan selanjutnya dengan bank dapat digeser ke waktu lain. Sistem off-line diharapkan dapat tetap mempertahankan keamanan transaksi. Tanpa pengawasan on-line dari bank, masalah keamanan ini menjadi lebih kritis, khususnya bagi pihak penerima dan pihak bank. Selain itu juga dibutuhkan kerahasiaan data belanja seseorang terhadap orang lain (privasi). Dalam tugas akhir ini dilakukan studi pengembangan awal suatu desain protokol sistem pembayaran elektronis melalui internet dengan verifikasi off-line. Pengembangan protokol sistem ini memanfaatkan kosep-konsep matematis, seperti kriptografi dan operasi dalam teori bilangan. Untuk menganalisis keamanan protokol dengan cara yang lebih sistematis, dikembangkan kerangka analisis formal. Kerangka analisis tersebut kemudian diterapkan terhadap protokol. Hasisl analisis dapat membantu mengamai perubahan status yang terjadi pada saat protokol dijalankan. Analisis tersebut juga dapat memperlihatkan beberapa kelemahan pada desain.