Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif
A biztonsági protokollok ellenőrzése az 1990-es évek óta aktív kutatási terület. Ez a téma több okból is érdekes.
A biztonsági protokollok mindenütt jelen vannak: többek között az e-kereskedelemben, a vezeték nélküli hálózatokban, a hitelkártyákban és az e-szavazásban használják őket. A biztonsági protokollok tervezése közismerten hibatermékeny. Ezek a hibák súlyos következményekkel is járhatnak.
Ezért a protokollok formális ellenőrzése vagy bizonyítása különösen kívánatos.
Ez az áttekintés a protokollok specifikációinak ellenőrzésére összpontosít a szimbolikus modellben. Bár meglehetősen absztrakt, az ellenőrzésnek ez a szintje a gyakorlatban mégis fontos, mivel számos támadás felfedezését teszi lehetővé.
A ProVerif egy automatikus szimbolikus protokoll verifikátor. Támogatja a kriptográfiai primitívek széles skáláját, amelyeket újraírási szabályokkal vagy egyenletekkel definiál. Különböző biztonsági tulajdonságokat tud bizonyítani: titkosság, hitelesítés és folyamat-egyenértékűség, korlátlan üzenettérre és korlátlan számú munkamenetre.
Bemenetként a protokoll leírását veszi fel, amelyet az alkalmazott pi-kalkulus egy dialektusában, a pi-kalkulus kriptográfiával történő kiterjesztésében kell ellenőrizni. Ezt a protokollleírást automatikusan lefordítja Horn-klauzulákra, és e klauzulák felbontásával meghatározza, hogy a kívánt biztonsági tulajdonságok fennállnak-e. Ez az áttekintés áttekintést nyújt a ProVerif kutatásairól, és a témában elérhető legátfogóbb szöveg.