Kryptografické protokoly - ÚINF/KRP


Kurz ku kryptografickým protokolom bude tento semester v pondelky od 14:25 v P16 alebo v LKB (podľa oznámenia).

I. Kryptografické protokoly, možnosti automatickej verifikácie
II. Neštandardné protokoly, zabezpečujúce špeciálne ciele
III. Aktuálne problémy a riešenia pomocou kryptografických protokolov (semináre)
Odporúčaná literatúra a ďalšie zdroje informácií
Pravidlá hodnotenia

  Prebraté a plánované témy
24.9.2018
P16
Úvod - bezpečnostné ciele modernej kryptografie, kryptografické protokoly a možnosti útokov.
Autentifikácia a distribúcia kľúčov pomocou symetrickej a asymetrickej kryptografie - príklady a známe útoky.
Pozrite tiež kapitoly 3. a 4. z knihy
Boyd, Mathuria: Protocols for Authentication and Key Establishment (v intranete)
Slajdy z prednášky - úvod Slajdy z prednášky - protokoly
Úlohy na precvičenie (doc, pdf) - riešenia odovzdajte písomne najneskôr do 1.10.2018, 14:25
1.10.2018
P16
Cvičenia v LKB
Analýza protokolov pomocou logík vier - idealizácia protokolu, odvodzovacie pravidlá.
BAN logika, ohraničenia, GNY rozšírenie.
Prostredie ABLOB (Win) - skopírujte súbor ABLOBinst.exe a spustite inštaláciu.
Slajdy použité na prednáške
Úlohy na precvičenie (doc) - riešenia odovzdajte písomne najneskôr do 8.10.2018, 14:25
8.10.2018
P16
Cvičenia v LKB
Ohraničenia použitia BAN logiky, GNY a iné rozšírenia.
Analýza protokolov dokazovaním tvrdení - prostredie Isabelle
Možnosti a ohraničenia použitia modálnych logík v analýze protokolov
Analýza bezpečnosti metódou Strand Spaces (guide) .
Modelovanie protokolu a modelovanie útočníka, spôsoby dokazovania niektorých bezpečnostných cieľov.
Fabrega, Herzog, Guttman: Strand Spaces: Proving Security Protocols Correct.
Slajdy z prednášky - Strand Spaces
Cvičenia - analýza protokolov v prostredí Ablob (s upravenými logikami) a prostredie Isabelle
Úlohy na precvičenie (doc) - riešenia odovzdajte písomne najneskôr do 15.10.2018, 14:25
15.10.2018
P16
Cvičenia v LKB
Formalizácia protokolu pomocou procesného kalkulu.
Formulácia bezpečnostných cieľov a model útočníka - spi-kalkul.
Metóda verifikácie overovaním modelu (model checking).
Slajdy z prednášky
Úlohy na precvičenie (doc) - riešenia odovzdajte písomne najneskôr do 22.10.2018, 14:25
22.10.2018 Simulácia vykonávania procesov v procesnom kalkule.
Slajdy z prednášky
Overovanie dôvernosti a autentičnosti.
Cvičenia - analýza protokolov v prostredí ProVerif.
Slajdy z TU Eindhoven k ProVerif - Intro Secrecy & Authentication
Úlohy na precvičenie (doc) - riešenia odovzdajte najneskôr do 29.10.2018, 14:25
29.10.2018
P16
Cvičenia v LKB
Dohody na kľúčoch.
Transport kľúčov - forward secrecy.
Idealizácia protokolov SSL/TLS, IPSec.
Kapitola 5. z knihy Boyd, Mathuria: Protocols for Authentication and Key Establishment (v intranete)
slajdy z prednášky
Cvičenia - možnosti hľadania útokov v prostrediach Scyther a Tamarin.
Scyther-manual
Cremers, Mauw: Operational Semantics and Verification of Security Protocols (v intranete)
Obraz systému s nainštalovaným prostredím Scyther
5.11.2018 Autentifikácia na základe identity.
Autentifikačné protokoly s pomocou hesla (EKE protokol)
Dohody na kľúčoch medzi viacerými účastníkmi.
Konferenčné kľúče.
Pozrite tiež kapitoly 6. a 7. z knihy
Boyd, Mathuria: Protocols for Authentication and Key Establishment (v intranete)
slajdy z prednášky
Úlohy na precvičenie (doc) - riešenia odovzdajte najneskôr do 19.11.2018, 14:25
12.11.2018 Hádzanie mincou, poker po telefóne, anonymizované prenosy - oblivious transfer
Utajená voľba, porovnávanie čísel
slajdy z prednášky
19.11.2018 Interaktívne dôkazy bez šírenia tajomstva
slajdy z prednášky
Distribúcia kľúčov kvantovou kryptografiou [Mižák]
26.11.2018 Bitcoin protokol, bezpečnosť virtuálnej meny [Kázsmérová]
Techniky blokových reťazcov a ich využitie [Chomič]
3.12.2018 Elektronické bankovníctvo, SET, 3D Secure, mikroplatby (MR1) [Kokuľová]
Bezpečnosť prenosov v sieti Skype [Linková]
10.12.2018 Wireless security - bezpečnosť bezdrôtových sietí WPA2, WPA3 [Pivarníková]
Bezpečnosť komunikácie v prostredí IoT [Chrastina]
17.12.2018 Ak ostane čas
Elektronické voľby
Elektronické aukcie
WhatsApp/Signal protokol

Odporúčaná literatúra :

Boyd, Mathuria: Protocols for Authentication and Key Establishment, Springer, 2003 (local)
Ryan, Schneider: Modelling and Analysis of Security Protocols, Addison Wesley, 2001
Mao: Modern Cryptography: Theory and Practice, Prentice Hall, 2003
Menezes, van Oorschot, Vanstone: Handbook of Applied Cryptography, CRC Press, 1996
Douglas R. Stinson: Cryptography: Theory and Practice, Third Edition, Chapman & Hall/CRC, 2006
Bruce Schneier: Applied Cryptography, Second Edition, John Wiley & Sons Inc., 1996
ePrint archív aktuálnych článkov IACR
Skriptá Kryptológia od Martina Staneka

Doplnková literatúra:
Burrows, Abadi, Needham: A logic of authentication. Rep. 39, DEC SRC, 1989. (pôvodné značenie)
Burrows, Abadi, Needham: A logic of authentication, ACM TOCS, 1990
L. Gong, R. Needham, R. Yahalom: Reasoning About Belief in Cryptographic Protocols, IEEE S&P 1991
P. Syverson,P.C. van Oorschot: On Unifying Some Cryptographic Protocol Logics, IEEE S&P 1994
D. Monniaux: Analysis of cryptographic protocols using logics of belief: an overview. JTIT 2002.
C. Boyd, W. Mao: On a Limitation of BAN Logic
V. Kessler, G. Wedel: AUTLOG - An advanced logic of authentication


Ďalšie zdroje na Sieti :

Kryptografické kompendium J. Savarda
CryptoDox
Lipmaa - kryptopointre
Crypto-world
IACR
NSA
RSA Laboratories

Projekt AVISPA - Vybrané protokoly; zoznam v ps
Špecifikačný jazyk - tutoriál
SPORE - Security Protocols Open Repository



Kritériá hodnotenia - bodované aktivity: Celkové hodnotenie - aspoň 70 bodov E, 80 bodov D, 90 bodov C, 100 bodov B, 110 bodov A