Modello di attacco Dolev-Yao e crittografia simbolica

Proposto da Danny Dolev e Andrew Yao nel 1983, il modello Dolev-Yao è il modello standard dell'avversario per l'analisi simbolica dei protocolli. L'attaccante controlla l'intera rete.

L'attaccante Dolev-Yao può: intercettare qualsiasi messaggio, memorizzare i messaggi, riprodurre vecchi messaggi, falsificare nuovi messaggi a partire da componenti conosciuti, ma non può compromettere le primitive crittografiche sottostanti.

Nei modelli simbolici, la crittografia è una scatola nera perfetta: l'attaccante non può decifrare senza la chiave, non può fattorizzare numeri grandi né falsificare firme. Questo semplifica l'analisi, ma può non rilevare attacchi a livello di implementazione.

I messaggi sono modellati come termini: enc(k, m), sig(sk, m), hash(m), pair(a, b). L'attaccante conosce determinati termini e ne ricava di nuovi utilizzando regole definite (regole di deduzione).

La conoscenza dell'attaccante è chiusa rispetto alla deduzione: se conosce enc(k,m) e k, può ricavare m. Se conosce pair(a,b), può ricavare a e b. La chiusura della conoscenza iniziale = tutto ciò che l'attaccante può apprendere.

La sicurezza del protocollo si esprime così: "la conoscenza dell'attaccante non contiene mai il segreto s in alcuno stato raggiungibile". Segretezza = raggiungibilità. Autenticazione = assenza di determinati schemi di tracce dannose.

Protocollo tra due parti: A→B: {Na, A}_{K_B}; B→A: {Na, Nb}_{K_A}; A→B: {Nb}_{K_B}. Nell'algebra dei termini: Alice invia enc(pubkey_B, pair(Na, A)). Verifichiamo che, dopo l'esecuzione, solo B conosca Na.

Il calcolo pi applicato (Abadi & Fournet 2001) è un'algebra dei processi per modellare i protocolli. I processi comunicano attraverso canali; l'attaccante controlla i canali pubblici. ProVerif e Tamarin utilizzano questo formalismo.

Un protocollo sicuro nel modello Dolev-Yao può essere comunque insicuro dal punto di vista computazionale se l'istanza crittografica è debole. Il teorema di solidità computazionale (Cortier et al.) colma il divario per specifiche classi di primitive.

Dolev-Yao non è in grado di modellare: proprietà algebriche (ad esempio, la commutatività di XOR), attacchi a canale laterale, bug di implementazione o errori probabilistici. Le estensioni come il modello della teoria equazionale gestiscono alcune proprietà algebriche.

Quale capacità NON possiede l'attaccante Dolev-Yao?

Dolev-Yao dà all'attaccante il controllo completo della rete, ma presume una crittografia perfetta. I messaggi sono termini di un'algebra; la sicurezza è una proprietà di raggiungibilità. Il calcolo pi applicato fornisce il linguaggio formale. Limitazioni: non può modellare relazioni algebriche, attacchi a canale laterale o bug di implementazione.