Dolev-Yao Saldırgan Modeli ve Sembolik Kriptografi

1983'te Danny Dolev ve Andrew Yao tarafından önerilen Dolev-Yao modeli, sembolik protokol analizi için standart saldırgan modelidir. Saldırgan tüm ağı denetler.

Dolev-Yao saldırganı şunları yapabilir: herhangi bir iletiyi yakalayabilir, iletileri saklayabilir, eski iletileri yeniden oynatabilir, bilinen bileşenlerden yeni iletiler üretebilir; ancak temel kriptografik yapıtaşlarını kıramaz.

Sembolik modellerde şifreleme kusursuz bir kara kutudur: saldırgan anahtar olmadan şifreyi çözemez, büyük sayıları çarpanlarına ayıramaz ve imzaları sahteleyemez. Bu, analizi basitleştirir ancak uygulama düzeyindeki saldırıların gözden kaçmasına neden olabilir.

İletiler terim olarak modellenir: enc(k, m), sig(sk, m), hash(m), pair(a, b). Saldırgan belirli terimleri bilir ve tanımlı kuralları (türetim kuralları) kullanarak yeni terimler türetir.

Saldırganın bilgisi türetim altında kapalıdır: saldırgan enc(k,m) ve k'yi biliyorsa m'yi türetebilir. pair(a,b)'yi biliyorsa a ve b'yi türetebilir. Başlangıç bilgisinin kapanışı = saldırganın öğrenebileceği her şey.

Protokol güvenliği şu şekilde ifade edilir: "erişilebilir herhangi bir durumda saldırganın bilgisi gizli s'yi hiçbir zaman içermez." Gizlilik = erişilebilirlik. Kimlik doğrulama = belirli kötü iz kalıplarının bulunmaması.

İki taraflı protokol: A→B: {Na, A}_{K_B}; B→A: {Na, Nb}_{K_A}; A→B: {Nb}_{K_B}. Terim cebirinde: Alice, enc(pubkey_B, pair(Na, A)) gönderir. Yürütme sonrasında yalnızca B'nin Na'yı bildiğini doğrularız.

Uygulamalı pi hesabı (Abadi & Fournet 2001), protokolleri modellemek için kullanılan bir süreç cebiridir. Süreçler kanallar üzerinden iletişim kurar; saldırgan herkese açık kanalları kontrol eder. ProVerif ve Tamarin bu biçimciliği kullanır.

Dolev-Yao modelinde güvenli olan bir protokol, kriptografik gerçekleştirim zayıfsa hesaplamalı açıdan yine de güvensiz olabilir. Hesaplamalı Sağlamlık teoremi (Cortier ve diğerleri), belirli ilkel sınıfları için bu boşluğu kapatır.

Dolev-Yao şunları modelleyemez: cebirsel özellikler (ör. XOR değişme özelliği), yan kanal saldırıları, uygulama hataları veya olasılıksal başarısızlıklar. Eşitliksel teori modeli gibi genişletmeler bazı cebirsel özellikleri ele alır.

Dolev-Yao saldırganının sahip olmadığı yetenek hangisidir (NOT)?

Dolev-Yao saldırgana ağ üzerinde tam denetim sağlar ancak kusursuz kriptografi varsayar. İletiler bir cebirdeki terimlerdir; güvenlik bir erişilebilirlik özelliğidir. Uygulamalı pi hesabı biçimsel dili sağlar. Sınırlamalar: cebirsel ilişkileri, yan kanalları veya uygulama hatalarını modelleyemez.