Abstrakt. Kontroll av säkerhetsprotokoll har varit ett mycket aktivt forskningsområde sedan 1990-talet. I detta dokument undersöks olika tillvägagångssätt på detta område, med beaktande av kontrollen i den symboliska modellen, liksom de nyare tillvägagångssätt som bygger på beräkningsmodellen eller som verifierar protokollgenomföranden snarare än specifikationer. Dessutom beskriver vi kortfattat vår symboliska säkerhetsprotokoll kontrollant ProVerif och placera det bland dessa metoder. Säkerhetsprotokoll är program som syftar till att säkra kommunikation på osäkra nätverk, till exempel Internet, genom att förlita sig på kryptografiska primitiva. Säkerhetsprotokoll är allmänt förekommande: de används till exempel för e-handel (t.ex. protokollet TLS [109], som används för https:// URLs), banktransaktioner, mobiltelefon- och WiFi-nätverk, RFID-taggar och e-voting. Utformningen av säkerhetsprotokoll är dock särskilt felbenägen. Detta kan till exempel illustreras med det mycket berömda Needham-Schroeder-protokollet [160], där Lowe hittade en brist [147] 17 år efter dess publicering. Även om stora framsteg har gjorts sedan dess finns det fortfarande många brister i de nuvarande säkerhetsprotokollen (se t.ex. http://www.opensl.org/news/ och http://www.openssh.org/security.html). Säkerhetsfel kan få allvarliga konsekvenser, vilket leder till förlust av pengar eller till att användarna förlorar förtroendet för systemet. Dessutom, säkerhetsfel kan inte upptäckas genom funktionell programvara testning eftersom de visas endast i närvaro av en illvillig motståndare. Automatiska verktyg kan därför vara till stor hjälp för att få faktiska garantier för att säkerhetsprotokoll är korrekta. Detta är ett skäl till att kontrollen av säkerhetsprotokoll har varit ett mycket aktivt forskningsområde sedan 1990-talet och fortfarande är mycket aktiv. Syftet med denna undersökning är att sammanfatta de resultat som uppnåtts på detta område. På grund av det stora antalet dokument om verifiering av säkerhetsprotokoll och det begränsade utrymmet var vi tvungna att utelämna många av dem. Vi anser att vi fortfarande presenterar företrädare för huvudstrategierna. Dessutom, Sect. 2.2 Kort beskriver vårt symboliska verifieringsverktyg ProVerif. Vi illustrerar begreppet säkerhet protokoll med följande exempel, en förenklad version av Denning-Sacco offentlig nyckel distribution protokoll [108].
Det har varit ett omfattande arbete med den formella kontrollen av viktiga utbytesprotokoll, se till exempel den senaste undersökningen REF.
Security protocol verification: Symbolic and computational models
{'venue': 'PRINCIPLES OF SECURITY AND TRUST - FIRST INTERNATIONAL CONFERENCE, POST 2012, VOLUME 7215 OF LECTURE NOTES IN COMPUTER SCIENCE', 'journal': None, 'mag_field_of_study': ['Computer Science']}