Modelovanie a overovanie bezpečnostných protokolov pomocou Applied Pi Calculus a ProVerif

Pôvodný názov:

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

Obsah knihy:

Overovanie bezpečnostných protokolov je aktívnou oblasťou výskumu od 90. rokov 20.

storočia. Táto téma je zaujímavá z niekoľkých dôvodov. Bezpečnostné protokoly sú všadeprítomné: používajú sa okrem iného pri elektronickom obchode, bezdrôtových sieťach, kreditných kartách, elektronickom hlasovaní.

Návrh bezpečnostných protokolov je notoricky známy tým, že je náchylný na chyby.

Tieto chyby môžu mať aj vážne dôsledky. Preto je formálna verifikácia alebo dôkaz protokolov mimoriadne žiaduca.

Tento prehľad sa zameriava na overovanie špecifikácií protokolov v symbolickom modeli. Aj keď je táto úroveň verifikácie pomerne abstraktná, má v praxi význam, pretože umožňuje odhaliť mnohé útoky. ProVerif je automatický verifikátor symbolických protokolov.

Podporuje širokú škálu kryptografických primitív definovaných pomocou pravidiel prepisu alebo pomocou rovníc. Dokáže dokázať rôzne bezpečnostné vlastnosti: utajenie, autentifikáciu a ekvivalenciu procesov pre neobmedzený priestor správ a neobmedzený počet relácií. Ako vstup sa berie opis protokolu, ktorý sa má overiť v dialekte aplikovaného pi kalkulu, rozšírenia pi kalkulu o kryptografiu.

Automaticky prekladá tento opis protokolu do Hornových klauzúl a určuje, či požadované bezpečnostné vlastnosti platia pomocou riešenia týchto klauzúl. Tento prehľad predstavuje prehľad výskumu ProVerif a je najkomplexnejším dostupným textom na túto tému.