Pada tesis ini, pengecekan model (model checking) dengan menggunakan NuSMV (New Symbolic Model Verifier ) dilakukan terhadap protokol pembayaran mikro Horn-Preneel. Pengecekan terfokus pada tahap pembayaran aktual, sedangkan tahap inisialisasi berupa otentikasi antara user dan vasp (value added service provider) diasumsikan sudah berjalan dengan baik dan benar. Pada akhir tahap pembayaran, terdapat broker yang berperan dalam pemberian credit kepada vasp atas pembayaran yang terverifikasi. Spesifikasi protokol yang diverifikasi adalah sifat liveness dan safety. Sifat liveness menunjukkan bahwa jika user sekali melakukan pembayaran maka pada suatu waktu pasti semua pembayaran selesai dilakukan. Sedangkan safety diartikan bahwa credit yang diberikan broker untuk vasp tidak melebihi jumlah yang dibayarkan oleh user. Langkah pertama yang dilakukan adalah memodelkan protokol menjadi sistem transisi yang digambarkan sebagai state diagram, kemudian diterjemahkan ke dalam bahasa pengecek model (model checker) NuSMV. Kemudian, spesifikasinya dimodelkan dalam bentuk formula LTL (Linear-time Temporal Logic). Parameter-parameter inisialisasi pembayaran terlebih dahulu didefinisikan dalam NuSMV dengan menggunakan fasilitas preprocessor m4. Selanjutnya, NuSMV secara otomatis melakukan verifikasi terhadap input model dan formula LTL tersebut. Output yang dikeluarkan oleh NuSMV menunjukkan bahwa model protokol memenuhi spesifikasi liveness dan safety. Pada uji coba yang dilakukan, waktu yang digunakan NuSMV untuk mengeluarkan output tersebut hanya selama 8 menit untuk sifat safety, sedangkan untuk sifat liveness selama 3 jam. vi + 59 hlm.; 15 gbr.; Daftar Pustaka: 15 (1996-2008)