Mengapa Pembuktian Informal Tidak Cukup

Perancang protokol secara rutin menghasilkan argumen keamanan informal — penalaran dalam bentuk prosa tentang alasan penyerang tidak dapat berhasil. Sejarah menunjukkan bahwa argumen ini sering kali keliru, bahkan pada protokol yang dirancang oleh para ahli.

Needham-Schroeder (1978) dirancang untuk autentikasi timbal balik. Pada 1995, Gavin Lowe menemukan serangan perantara menggunakan verifikasi otomatis — 17 tahun setelah publikasi. Pembuktian informal tersebut melewatkan pemutaran ulang yang sulit dideteksi.

WEP disetujui oleh IEEE pada 1997 dengan klaim keamanan informal. Pada 2001, peneliti menemukan penggunaan ulang aliran kunci RC4, kolisi IV, dan ketiadaan integritas — sehingga WEP dapat ditembus dalam hitungan menit. Penalaran informal melewatkan semuanya.

Keamanan protokol bergantung pada interaksi antara banyak sesi serentak, penyerang aktif, dan asumsi kriptografis. Penalaran manusia kesulitan menghadapi ledakan jumlah status dan eksekusi serentak yang saling tersisip.

Metode formal memodelkan protokol secara matematis dan membuktikan — atau menyangkal — properti keamanan (kerahasiaan, autentikasi, kerahasiaan berkelanjutan) untuk semua strategi penyerang yang mungkin, bukan hanya strategi yang dipertimbangkan oleh perancang.

Simbolik (Dolev-Yao): kriptografi adalah kotak hitam sempurna; fokus pada logika protokol. Komputasional: permainan keamanan probabilistik nyata; lebih dekat dengan jaminan dunia nyata. Keduanya dapat menemukan bug nyata.

POODLE (2014) mengeksploitasi oracle padding dalam CBC SSL 3.0. Kerentanan tersebut merupakan cacat desain tingkat protokol, bukan bug implementasi. Analisis formal terhadap spesifikasi SSL 3.0 semestinya telah menandai oracle tersebut sebelum penerapan.

TLS 1.3 (RFC 8446) dirancang bersamaan dengan analisis formal menggunakan ProVerif dan miTLS. Spesifikasi tersebut diiterasi berdasarkan temuan formal — sebuah tonggak dalam penerapan metode formal oleh badan standardisasi.

Alat formal memverifikasi model protokol, bukan implementasinya. Protokol yang diverifikasi secara formal tetap dapat memiliki implementasi yang tidak aman. F* / HACL* memperluas verifikasi hingga kode kriptografis itu sendiri.

Verifikasi formal mahal: pemodelan protokol memerlukan waktu berminggu-minggu dan keahlian khusus. Namun, untuk sasaran bernilai tinggi (TLS, SSH, Signal), biayanya sepadan — satu cacat protokol dapat berdampak pada miliaran pengguna.

Apa yang membuat penemuan Lowe pada 1995 tentang serangan Needham-Schroeder menjadi penting?

Pembuktian informal gagal karena penalaran manusia melewatkan interaksi antarsesi serentak dan strategi penyerang. Needham-Schroeder, WEP, dan POODLE semuanya memiliki argumen keamanan informal. TLS 1.3 memasukkan analisis formal selama perancangannya. Alat formal menemukan bug tingkat protokol sebelum penerapan.