Model Penyerang Dolev-Yao & Kripto Simbolis

Diusulkan oleh Danny Dolev dan Andrew Yao pada 1983, model Dolev-Yao adalah model musuh standar untuk analisis protokol simbolik. Penyerang mengendalikan seluruh jaringan.

Penyerang Dolev-Yao dapat: mencegat pesan apa pun, menyimpan pesan, memutar ulang pesan lama, memalsukan pesan baru dari komponen yang diketahui, tetapi tidak dapat memecahkan primitif kriptografi yang mendasarinya.

Dalam model simbolis, enkripsi adalah kotak hitam yang sempurna: penyerang tidak dapat mendekripsi tanpa kunci, tidak dapat memfaktorkan bilangan besar, dan tidak dapat memalsukan tanda tangan. Hal ini menyederhanakan analisis, tetapi mungkin tidak mendeteksi serangan pada tingkat implementasi.

Pesan dimodelkan sebagai suku: enc(k, m), sig(sk, m), hash(m), pair(a, b). Penyerang mengetahui suku tertentu dan menurunkan suku baru menggunakan aturan yang telah ditentukan (aturan deduksi).

Pengetahuan penyerang tertutup terhadap deduksi: jika mereka mengetahui enc(k,m) dan k, mereka dapat menurunkan m. Jika mereka mengetahui pair(a,b), mereka dapat menurunkan a dan b. Penutupan pengetahuan awal = segala sesuatu yang dapat dipelajari penyerang.

Keamanan protokol dinyatakan sebagai berikut: "pengetahuan penyerang tidak pernah memuat rahasia s dalam keadaan apa pun yang dapat dicapai." Kerahasiaan = keterjangkauan. Autentikasi = tidak adanya pola jejak buruk tertentu.

Protokol dua pihak: A→B: {Na, A}_{K_B}; B→A: {Na, Nb}_{K_A}; A→B: {Nb}_{K_B}. Dalam aljabar suku: Alice mengirim enc(pubkey_B, pair(Na, A)). Kami memverifikasi bahwa setelah eksekusi, hanya B yang mengetahui Na.

Kalkulus pi terapan (Abadi & Fournet 2001) adalah aljabar proses untuk memodelkan protokol. Proses berkomunikasi melalui saluran; penyerang mengendalikan saluran publik. ProVerif dan Tamarin menggunakan formalisme ini.

Protokol yang aman dalam model Dolev-Yao mungkin tetap tidak aman secara komputasional jika instansiasi kriptografinya lemah. Teorema Keterandalan Komputasional (Cortier dkk.) menjembatani kesenjangan tersebut untuk kelas primitif tertentu.

Dolev-Yao tidak dapat memodelkan: sifat aljabar (misalnya, komutativitas XOR), serangan kanal samping, bug implementasi, atau kegagalan probabilistik. Ekstensi seperti model teori persamaan menangani beberapa sifat aljabar.

Kemampuan apa yang TIDAK dimiliki penyerang Dolev-Yao?

Dolev-Yao memberi penyerang kendali penuh atas jaringan, tetapi mengasumsikan kriptografi yang sempurna. Pesan adalah suku dalam suatu aljabar; keamanan adalah properti keterjangkauan. Kalkulus pi terapan menyediakan bahasa formalnya. Keterbatasan: tidak dapat memodelkan hubungan aljabar, kanal samping, atau bug implementasi.