Abstract-Många populära webbprogram innehåller end-toend säkra meddelandeprotokoll, som försöker se till att meddelanden som skickas mellan användare hålls konfidentiella och autentiserade, även om webbapplikationens servrar bryts in i eller på annat sätt tvingas att släppa alla sina data. Protokoll som lovar sådana starka säkerhetsgarantier bör hållas upp till rigorös analys, eftersom protokoll brister och implementationer buggar lätt kan leda till verkliga attacker. Vi föreslår en ny metod som gör det möjligt för protokolldesigners, implementerare och säkerhetsanalytiker att tillsammans verifiera ett protokoll med hjälp av automatiserade verktyg. Protokollet implementeras i ProScript, ett nytt domänspecifikt språk som är utformat för att skriva kryptografisk protokollkod som både kan köras inom JavaScript-program och automatiskt översättas till en läsbar modell i den tillämpade pi-kalkylen. Denna modell kan sedan analyseras symboliskt med ProVerif för att hitta attacker i en mängd olika hotmodeller. Modellen kan också användas som grund för ett beräkningsunderlag med hjälp av CryptoVerif, vilket minskar säkerheten i protokollet till standard kryptografiska antaganden. Om ProVerif hittar en attack, eller om CryptoVerif-beviset avslöjar en svaghet, ändrar protokolldesignern ProScript-protokollkoden och återskapar modellen för att möjliggöra en ny analys. Vi demonstrerar vår metodik genom att implementera och analysera en variant av det populära signalprotokollet med endast mindre skillnader. Vi använder ProVerif och CryptoVerif för att hitta nya och tidigare kända svagheter i protokollet och föreslå praktiska motåtgärder. Vår ProScript protokollkod ingår i den aktuella utgåvan av Cryptocat, en stationär säker budbärare program skriven i JavaScript. Våra resultat tyder på att den systematiska analysen av komplexa kryptografiska webbapplikationer nu håller på att bli praktisk med disciplinerad programmering och viss verifieringsexpertis.
ProScript REF är ett sådant exempel som kan köras inom JavaScript-program och användas för symbolisk analys.
Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach
{'venue': '2017 IEEE European Symposium on Security and Privacy (EuroS&P)', 'journal': '2017 IEEE European Symposium on Security and Privacy (EuroS&P)', 'mag_field_of_study': ['Computer Science']}