SKS 2022 cvicenie tyzden 7

Zhrnutie prednášky

Cvičenie sa najprv venuje softvérovým nástrojom na formálnu verifikáciu protokolov, ktoré sa delia na podporné nástroje pre tvorbu dôkazov bezpečnosti (EasyCrypt, CryptoVerif) a symbolické nástroje. Symbolické nástroje modelujú protokol formálnym jazykom a pracujú s ohraničeným počtom behov, takže vedia odhaliť útok, no ak ho nenájdu, nezaručujú bezpečnosť protokolu v reálnom svete. Hlavná časť je zameraná na neformálnu analýzu protokolov so symetrickou kryptografiou bez servera: jednoduchý protokol s jednou správou (časová pečiatka, identifikátor Boba a nový session key) a protokol s výmenou nonce a keying materialu, z ktorého sa pomocou key derivation function odvodí session key. Ku každému protokolu patrí bonusová úloha s 14 otázkami a záver naznačuje prechod k protokolom využívajúcim dôveryhodný server.

• - Nástroje formálnej verifikácie sa delia na podporné nástroje pre dôkazy bezpečnosti (EasyCrypt, CryptoVerif) a symbolické nástroje.
• - Symbolické nástroje modelujú protokol formálnym jazykom a hľadajú reťazce reprezentujúce úspešný útok.
• - Limitácia symbolických nástrojov: ohraničený počet behov a zjednodušený model, takže nenájdenie útoku neznamená bezpečnosť v reálnom svete.
• - Protokol 1: Alica pošle Bobovi jednu správu so značkou času, ID Boba a novým session key zašifrovanými autentizovanou symetrickou šifrou.
• - Protokol 2: výmena nonce a keying materialu (FAB, FBA), z ktorých sa pomocou key derivation function (napr. hash konkatenácie) vytvorí session key.
• - Bonusy 5 a 6 vyžadujú neformálnu analýzu protokolov (14 otázok so zdôvodnením), deadline 4.4. o 23.59, s možnosťou predĺženia.
• - Nasleduje protokol 3 so serverom, kde Alica a Bob zdieľajú s ním long-term kľúče KAS a KBS.

Zhrnutie pripravené s pomocou AI z prepisu videa.