|
|
Evoluční knihovna pro podporu návrhu komunikačních protokolů
Sameš, Martin ; Trchalík, Roman (oponent) ; Očenášek, Pavel (vedoucí práce)
Potreba vyvíjať nové a nové bezpečnostné protokoly, ktoré zodpovedajú stanoveným požiadavkám vedie k automatizácií ich návrhu a následne lepšiu možnosť verifikácie. Táto práca sa zaoberá možnosťou automatizovaného návrhu protokolov s využitím genetických algoritmov. Porovnaním jednotlivých prístupov a následným vytvorením evolučnej knižnice pre podporu návrhu bezpečnostných protokolov.
|
|
|
Metody návrhu platebních protokolů
Matúška, Peter ; Trchalík, Roman (oponent) ; Očenášek, Pavel (vedoucí práce)
Tato práce analyzuje existující přístupy v návrhu bezpečnostních a platebních protokolů. Popisuje jejich návrh použitím BAN logiky a použitím derivačního systému. Speciální pozornost je věnována metodě kompozice, která je založena na vytváření složitějších protokolů z menších celků a je demonstrována na návrhu nákupní procedury protokolu SET. Metoda je v rámci práce automatizována a implementována v jazyce C++, co umožňuje návrháři na základě jeho požadavků vygenerovat množinu kandidátních protokolů, které může dále použít jako základ v další fázi návrhu.
|
|
|
Databáze specifikací bezpečnostních protokolů
Ondráček, David ; Trchalík, Roman (oponent) ; Očenášek, Pavel (vedoucí práce)
Původní protokoly, které vznikaly v počátcích vývoje počítačových sítí, již nejsou pro zajištění potřebné bezpečnosti dostačující. Proto se stále vyvíjejí a implementují protokoly nové. Důležitou součástí tohoto procesu je formální verifikace. Jde o analýzu protokolu po formální stránce, kdy se zjišťuje, zda lze protokol úspěšně napadnout. Diplomová práce se zabývá analýzou vybraných bezpečnostních protokolů a nástrojů pro jejich formální verifikaci. Výstupem praktické části je databáze specifikací protokolů v LySa kalkulu a výsledky jejich verifikace nástrojem LySatool.
|
|
|
Databáze specifikací bezpečnostních protokolů
Papež, Zdeněk ; Trchalík, Roman (oponent) ; Očenášek, Pavel (vedoucí práce)
Tato bakalářská práce pojednává o bezpečnostních protokolech, které slouží jako prostředek pro vytvoření chráněné komunikace ve veřejné síti, Internetu. Bezpečnostních protokolů je celá řada. Proto jsem vybral jen pár nejznámějších protokolů a podrobně je analyzoval. Z dostupných zdrojů jsem shromáždil informace o protokolech, které vždy jednotně uvádím u každého z nich. Hlavním přínosem mé studie o bezpečnostních protokolech je prozkoumání množin, které se úzce vztahují k běhu bezpečnostního protokolu. Jedná se o množinu znalostí a množinu předpokladů jednotlivých subjektů, které se podílí na komunikaci pomocí daného protokolu. Tyto množiny pak uvádím v počátečním, cílovém a aktuálním stavu. Na závěr shrnuji všechny zpracované protokoly do přehledné tabulky, která je i s detaily všech protokolů převedena do počítačové databáze a veřejně přístupná na fakultních stránkách.
|
|
|
Databáze specifikací bezpečnostních protokolů
Papež, Zdeněk ; Trchalík, Roman (oponent) ; Očenášek, Pavel (vedoucí práce)
Tato bakalářská práce pojednává o bezpečnostních protokolech, které slouží jako prostředek pro vytvoření chráněné komunikace ve veřejné síti, Internetu. Bezpečnostních protokolů je celá řada. Proto jsem vybral jen pár nejznámějších protokolů a podrobně je analyzoval. Z dostupných zdrojů jsem shromáždil informace o protokolech, které vždy jednotně uvádím u každého z nich. Hlavním přínosem mé studie o bezpečnostních protokolech je prozkoumání množin, které se úzce vztahují k běhu bezpečnostního protokolu. Jedná se o množinu znalostí a množinu předpokladů jednotlivých subjektů, které se podílí na komunikaci pomocí daného protokolu. Tyto množiny pak uvádím v počátečním, cílovém a aktuálním stavu. Na závěr shrnuji všechny zpracované protokoly do přehledné tabulky, která je i s detaily všech protokolů převedena do počítačové databáze a veřejně přístupná na fakultních stránkách.
|
|
|
Metody návrhu platebních protokolů
Matúška, Peter ; Trchalík, Roman (oponent) ; Očenášek, Pavel (vedoucí práce)
Tato práce analyzuje existující přístupy v návrhu bezpečnostních a platebních protokolů. Popisuje jejich návrh použitím BAN logiky a použitím derivačního systému. Speciální pozornost je věnována metodě kompozice, která je založena na vytváření složitějších protokolů z menších celků a je demonstrována na návrhu nákupní procedury protokolu SET. Metoda je v rámci práce automatizována a implementována v jazyce C++, co umožňuje návrháři na základě jeho požadavků vygenerovat množinu kandidátních protokolů, které může dále použít jako základ v další fázi návrhu.
|
|
|
Databáze specifikací bezpečnostních protokolů
Hadaš, Petr ; Trchalík, Roman (oponent) ; Očenášek, Pavel (vedoucí práce)
Diplomová práce popisuje čtyři nástroje určené pro verifikaci bezpečnostních protokolů Athena, Casper, Isabelle a Murphi. U každého je uvedena stručná charakteristika a část implementace protokolu Needham Schroeder. Součástí je také srovnání vybraných nástrojů. Druhá část práce podrobně popisuje nástroj Athena a uvádí příklady verifikovaných protokolů. U každého protokolu je uvedena specifikace komunikace, odhalený útok a výsledky vlastní verifikace. Na závěr práce porovnává výsledky verifikace s již publikovanými útoky.
|
|
|
Evoluční knihovna pro podporu návrhu komunikačních protokolů
Sameš, Martin ; Trchalík, Roman (oponent) ; Očenášek, Pavel (vedoucí práce)
Potreba vyvíjať nové a nové bezpečnostné protokoly, ktoré zodpovedajú stanoveným požiadavkám vedie k automatizácií ich návrhu a následne lepšiu možnosť verifikácie. Táto práca sa zaoberá možnosťou automatizovaného návrhu protokolov s využitím genetických algoritmov. Porovnaním jednotlivých prístupov a následným vytvorením evolučnej knižnice pre podporu návrhu bezpečnostných protokolov.
|
|
|
Databáze specifikací bezpečnostních protokolů
Ondráček, David ; Trchalík, Roman (oponent) ; Očenášek, Pavel (vedoucí práce)
Původní protokoly, které vznikaly v počátcích vývoje počítačových sítí, již nejsou pro zajištění potřebné bezpečnosti dostačující. Proto se stále vyvíjejí a implementují protokoly nové. Důležitou součástí tohoto procesu je formální verifikace. Jde o analýzu protokolu po formální stránce, kdy se zjišťuje, zda lze protokol úspěšně napadnout. Diplomová práce se zabývá analýzou vybraných bezpečnostních protokolů a nástrojů pro jejich formální verifikaci. Výstupem praktické části je databáze specifikací protokolů v LySa kalkulu a výsledky jejich verifikace nástrojem LySatool.
|
host ::
RSS.