Modellazione e verifica di protocolli di sicurezza con il Calcolo Pi applicato e ProVerif

Titolo originale:

Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif

Contenuto del libro:

La verifica dei protocolli di sicurezza è un'area di ricerca attiva fin dagli anni Novanta. Questo argomento è interessante per diversi motivi.

I protocolli di sicurezza sono onnipresenti: sono utilizzati per il commercio elettronico, le reti wireless, le carte di credito, il voto elettronico, ecc. La progettazione di protocolli di sicurezza è notoriamente soggetta a errori. Questi errori possono anche avere gravi conseguenze.

Per questo motivo, la verifica formale o la prova dei protocolli è particolarmente auspicabile.

Questa ricerca si concentra sulla verifica delle specifiche dei protocolli nel modello simbolico. Anche se è piuttosto astratto, questo livello di verifica è rilevante nella pratica, poiché consente di scoprire molti attacchi.

ProVerif è un verificatore automatico di protocolli simbolici. Supporta un'ampia gamma di primitive crittografiche, definite da regole di riscrittura o da equazioni. È in grado di dimostrare varie proprietà di sicurezza: segretezza, autenticazione ed equivalenza dei processi, per uno spazio di messaggi non limitato e un numero non limitato di sessioni.

Prende in input una descrizione del protocollo da verificare in un dialetto del calcolo pi greco applicato, un'estensione del calcolo pi greco con crittografia. Traduce automaticamente la descrizione del protocollo in clausole di Horn e determina se le proprietà di sicurezza desiderate sono valide mediante risoluzione su queste clausole. Questa rassegna presenta una panoramica della ricerca su ProVerif ed è il testo più completo disponibile sull'argomento.