Nástroje pro analýzu bezpečnostních protokolů

bezpečnostní protokol, statická analýza, verifikace, LySa, OFMC, kryptografie

Bezpečností protokoly jsou komunikační sekvence, ktere slouží k výměně dat mezi entitami za účelem ověření identity, vyměny šifrovacího klíče apod. Při návrhu těchto protokolů je potřeba ověřit, zda výměna dat je korektní a odolná proti různým útokům (podvržení dat, zachycení paketu, předstírání identity). V semináři představíme způsoby formálního popisu bezpečnostních protokolů a možnosti analýzy návrhů. Ukážeme také některé verifikační nástroje (např. model checker OFMC/AVISPA).