Kryptografické protokoly - ÚINF/KRP


Kurz ku kryptografickým protokolom bude tento semester v LKB (SJ1L19) v pondelky od 13:30 cvičenia a od 15:10 prednáška.
Dištančné vzdelávanie bude prebiehať v skupine KRP2020 prostredníctvom systému MS Teams.
Odporúčaná literatúra a ďalšie zdroje informácií
Pravidlá hodnotenia

Prvý záverečný test bude dištančný.
Bude prebiehať v prostredí MS Teams KRP2020 vo štvrtok 21.1.2021 od 10:00.
Na overenie rovnakých podmienok sa predpokladá, že budete mať spustenú kameru
počas celého testu a na stole prípadne len čistý papier, písacie potreby
a vytlačený BAN guide a spi guide.
Riešenia môžte vpisovať pomocou integrovaného editora MS Teams v poznámkovom bloku
alebo písať na papier a v závere riešenie oskenovať a poslať cez MS Teams editor alebo e-mailom.
Bude dobré, keď sa pripojíte už okolo 9:30, aby sme vyladili technické problémy.

Výsledky prvého testu som (konečne) zapísal do AIS-u.
Ak nie ste spokojní s navrhovaným hodnotením, môžete sa pripojiť do ďalších testov (aj bez prihlásenia cez AIS).
Do záverečného hodnotenia sa započíta najlepší výsledok testu.

Ďalší test bude dištančne v MS Teams KRP2020 vo štvrtok 4.2.2021 od 10:00

Prosím, vyplňte aj dotazník s hodnotením vyučovania.

  Prebraté a plánované témy
21. 9. 2020
Úvod - bezpečnostné ciele modernej kryptografie
Používané kryptografické nástroje - princípy -
symetrická kryptografia, kryptografické odtlačky (hash)
Využitie na konkrétne bezpečnostné ciele
van Oorschot: Cryptographic Building Blocks
slajdy z prednášky
28 9. 2020
Používané kryptografické nástroje - princípy - pokračovanie -
asymetrická kryptografia
Využitie na konkrétne bezpečnostné ciele
van Oorschot: Cryptographic Building Blocks
slajdy z prednášky
Úlohy na precvičenie (doc, pdf) - riešenia odovzdajte v systéme MS Teams v skupine KRP2020 najneskôr do 12.10.2020, 15:10
5.10.2020 Digitálne podpisy, certifikáty.
van Oorschot: Cryptographic Building Blocks
Detailnejšie popisy základných kyptografických nástrojov možno nájsť
v Paar, Pelzl: Understanding Cryptography (prístupné v Intranete)
slajdy z prednášky
Úlohy na precvičenie (doc, pdf) - riešenia odovzdajte do skupiny KRP2020 najneskôr do 19.10.2020, 15:10
12.10.2020 Generovania a distribúcia symetrických kľúčov.
Autentifikácia, ciele, preukazovanie identity.
Autentifikačný protokol, možnosti útokov.
van Oorschot: User Authentication
van Oorschot: Chapter 4.1 - 4.4
Boyd, Mathuria, Stebila: Intro to Authentication ...
slajdy z prednášky
19.10.2020 Formálne modely bezpečnosti protokolov a možnosti útokov.
Autentifikácia pomocou symetrickej a asymetrickej kryptografie - príklady a známe útoky.
Boyd, Mathuria, Stebila: Computational Security Model
slajdy z prednášky
Úlohy na precvičenie (doc, pdf) - riešenia odovzdajte do skupiny KRP2020 najneskôr do 26.10.2020, 12:00
26.10.2020
13:30
Autentifikácia pomocou symetrickej a asymetrickej kryptografie - príklady a známe útoky.
Využitie dôveryhodných centier.
Boyd, Mathuria, Stebila: Kap. 3.2 a 4.2 (v intranete resp. v Teams/Prednášky/Súbory)
Analýza protokolov pomocou logík vier - idealizácia protokolu, odvodzovacie pravidlá.
BAN logika, ohraničenia, GNY rozšírenie.
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
Bleeker, Meertens: A semantics for BAN logic
BAN guide
M. Novotný: Prostredie ABLOB (Win) - skopírujte súbor ABLOBinst.exe a spustite inštaláciu.
Slajdy použité na prednáške (v intranete resp. v Teams/Prednášky/Súbory)
Úlohy série D na precvičenie (doc, pdf) - riešenia odovzdajte do skupiny KRP2020 najneskôr do 2.11.2020, 12:00
2.11.2020 Distribúcia kľúčov pomocou symetrickej a asymetrickej kryptografie - príklady a známe útoky.
Ohraničenia použitia BAN logiky, GNY a iné rozšírenia.
L. Gong, R. Needham, R. Yahalom: Reasoning About Belief in Cryptographic Protocols, IEEE S&P 1991
Mathuria, Safavi-Naini, Nickolas: On the Automation of GNY Logic
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
Vyhľadávanie chýb a možných útokov na konkrétne protokoly.
Zjednodušovanie protokolu.
Možnosti a ohraničenia použitia modálnych logík v analýze protokolov
Boyd, Mathuria, Stebila: Kap. kap. 3 a kap. 4 (v intranete resp. v Teams/Prednášky/Súbory)
Slajdy z prednášky
Úloha série E na precvičenie (doc, pdf) - riešenia odovzdajte do skupiny KRP2020 najneskôr do 9.11.2020, 12:00
9.11.2020 Formalizácia protokolu pomocou procesného kalkulu.
Formulácia bezpečnostných cieľov a model útočníka - spi-kalkul.
Simulácia vykonávania procesov v procesnom kalkule.
Metóda verifikácie overovaním modelu (model checking).
Overovanie dôvernosti a autentičnosti v spi-kalkule.
Abadi, Gordon: A Calculus for Cryptographic Protocols - The Spi Calculus
Prostredie ProVerif - rozšírený manuál.
ProVerif - Online demo.
Slajdy z prednášky
Úloha série F na precvičenie (doc, pdf) - riešenia odovzdajte do skupiny KRP2020 najneskôr do 16.11.2020, 12:00
16.11.2020 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.
Možnosti hľadania útokov v prostredí Scyther, Scyther-manual, Tamarin (Tamarin-manual)
Cremers: Scyther - Semantics and Verification of Security Protocols.
Slajdy z prednášky - Strand Spaces
Úloha série G na precvičenie (doc, pdf) - riešenia odovzdajte do skupiny KRP2020 najneskôr do 23.11.2020, 12:00
23.11.2020 Dohody na kľúčoch cez nezabezpečený kanál.
Efemérne kľúče - forward secrecy.
Protokol IKEv2 pre IPsec.
Zraniteľnosti v implementáciách TLS protokolu
Boyd, Mathuria, Stebila: kapitola 5 a kapitola 6 (v intranete resp. v Teams/Prednášky/Súbory)
slajdy z prednášky
Úloha série H na precvičenie (doc, pdf) - riešenia odovzdajte do skupiny KRP2020 najneskôr do 30.11.2020, 12:00
30.11.2020 Dohoda na kľúči na základe identity, s pomocou hesla (EKE, PAKE protokol)
Dohody na kľúčoch medzi viacerými účastníkmi.
Konferenčné kľúče.
Boyd, Mathuria, Stebila: kapitola 7, kapitola 8 a kapitola 9 (v intranete resp. v Teams/Prednášky/Súbory)
slajdy z prednášky
7.12.2020 Dohoda na kľúči kvantovou kryptografiou (ak si nikto nevyberie na seminár)
Hádzanie mincou, poker po telefóne, anonymizované prenosy - oblivious transfer
Utajená voľba, porovnávanie čísel
Interaktívne dôkazy bez šírenia tajomstva
slajdy z prednášky
Úlohy série I na precvičenie (doc, pdf) - riešenia odovzdajte do skupiny KRP2020 najneskôr do 21.1.2021, 9:30
14.12.2020
13:30-17:00
Bitcoin protokol, bezpečnosť virtuálnej meny [Revický]
elektronické aukcie [Marková]
elektronické voľby [Kováčová]
21.12.2020
13:30-17:00
protokol Signal [Fuska]
bezpečnosť RFID identifikácie a kódov EPC [Vojtek]
LTE, GSM autentifikácia, bezpečnosť v 3G, 4G a 5G sieťach [Amrichová]

Odporúčaná literatúra :

Boyd, Mathuria: Protocols for Authentication and Key Establishment, Springer, 2020 (v Intranete)
Ryan, Schneider: Modelling and Analysis of Security Protocol, Addison Wesley, 2001
Cremers, Mauw: Operational Semantics and Verification of Security Protocols, Springer, 2012
van Oorschot: Computer Security and the Internet, Springer, 2020 (v Intranete)

Paar, Pelzl: Understanding Cryptography, Springer 2010 (vďaka licencii Springer prístupné v Intranete)
Menezes, van Oorschot, Vanstone: Handbook of Applied Cryptography, CRC Press, 2001 (free!)
Mao: Modern Cryptography: Theory and Practice, Prentice Hall, 2003
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


Ďalšie zdroje na Sieti :

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

Odporúčané dĺžky kľúčov (ECRYPT II)
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



Možné okruhy otázok na ŠZS

* Formálny popis kryptografického protokolu, formulácia bezpečnostnych cieľov a model útočníka.
* Formálne metódy verifikácie kryptografických protokolov - prehľad a možnosti automatizácie.
* Generovanie a distribúcia symetrických kľúčov.
* Certifikácia, certifikačné autority, distribúcia dôvery. Systém PKI, overovanie certifikátov.
* Autentifikácia pomocou zdieľaného hesla a dohody na kľúči v dôvernom prostredí (forward secrecy).
* Silná autentifikácia pomocou asymetrickej kryptografie.
* Skupinová autentifikácia a dohoda na kľúči medzi viacerými účastníkmi.