Výzkum prezentovaný v této práci je zaměřen na evoluční optimalizaci vybraných komponent síťových aplikací určených pro monitorovací systémy vysokorychlostních sítí. Práce začíná studiem současných monitorovacích systémů. Jako experimentální platforma byl zvolen systém SDM (Software Defined Monitoring). Detailně bylo analyzováno zpracování síťového provozu, protože tvoří důležitou součást všech monitorovacích systémů. Jako demonstrační komponenty pro aplikaci optimálních technik navržených v této práci byly zvoleny klasifikátor aplikačních protokolů a hashovací funkce pro síťové toky. Evoluční algoritmy byly zkoumány s ohledem nejen na optimalizaci kvality zpracování dat danou síťovou komponentou, ale i na čas potřebný pro výpočet dané komponenty. Byly zkoumány jednokriteriální i vícekriteriální varianty evolučních algoritmů.     Byl navržen nový přístup ke klasifikaci aplikačních protokolů. Přesná i aproximativní verze klasifikátoru byla optimalizována pomocí CGP (Kartézské Genetické Programování). Bylo dosaženo výrazné redukce zdrojů a zpoždění v FPGA (Programovatelné Logické Pole) oproti neoptimalizované verzi. Speciální síťové hashovací funkce byly navrženy pomocí paralelní verze LGP (Lineární Genetické Programování). Tyto hashovací funkce vykazují lepší funkcionalitu oproti moderním hashovacím funkcím. S využitím vícekriteriální optimalizace byly vylepšeny výsledky původní jednokriteriální verze LGP. Paralelní zřetězené verze hashovacích funkcí byly implementovány v FPGA a vyhodnoceny za účelem hashování síťových toků. Nová rekonfigurovatelná hashovací funkce byla navržena jako kombinace vybraných hashovacích funkcí.  Velmi konkurenceschopná obecná hashovací funkce byla rovněž navržena pomocí multikriteriální verze LGP a její funkčnosti byla ověřena na reálných datových sadách v provedených studiích. Vícekriteriální přístup produkuje mírně lepší řešení než jednokriteriální LGP. Také se potvrdilo, že obecné implementace LGP a CGP jsou použitelné pro automatizovaný návrh a optimalizaci vybraných síťových komponent. Je však důležité zvládnout vícekriteriální povahu problému a urychlit časově kritické operace GP

Model checking problems suffer from state space explosion. State space explosion is the number of states in the graph increases exponentially with the number of variables in the state description. Searching the large graphs required in model checking requires an efficient algorithm. This dissertation explores several methods to improve an externalmemory search algorithm for model checking problems. A tool implementing these methods is built on top of the Murphi model checker. One improvement is a state cache for immediate detection leveraging the properties of state locality. A novel type of locality, intralayer locality is explained and shown to exist in a variety of search spaces. Another improvement, partial delayed duplicate detection, exploits interlayer locality to reduce search times. An automatic partitioning function is described that allows hash-based delayed duplicate detection to be used without domain knowledge of the state space. A phased delayed duplicate detection algorithm combining features of hash-based delayed duplicate detection and sorting-based delayed duplicate detection is explained and compared to the other methods.

Tendering is a method for entering into a sales contract. Numerous electronic tendering systems have been established with the intent of improving the efficiency of the tendering process. Although providing adequate security services is a desired feature in an e-tendering system, current e-tendering systems are usually designed with little consideration of security and legal compliance. This research focuses on designing secure protocols for e-tendering systems. It involves developing methodologies for establishing security requirements, constructing security protocols and using formal methods in protocol security verification. The implication is that it may prove suitable for developing secure protocols in other electronic business domains. In depth investigations are conducted into a range of issues in relation to establishing generic security requirements for e-tendering systems. The outcomes are presented in a form of basic and advanced security requirements for e-tendering process. This analysis shows that advanced security services are required to secure e-tender negotiation integrity and the submission process. Two generic issues discovered in the course of this research, functional difference and functional limitations, are fundamental in constructing secure protocols for tender negotiation and submission processes. Functional difference identification derives advanced security requirements. Functional limitation assessment defines how the logic of generic security mechanisms should be constructed. These principles form a proactive analysis applied prior to the construction of security protocols. Security protocols have been successfully constructed using generic cryptographic security mechanisms. These protocols are secure e-tender negotiation integrity protocol suite, and secure e-tender submission protocols. Their security has been verified progressively during the design. Verification results show that protocols are secure against common threat scenarios. The primary contribution of this stage are the procedures developed for the complex e-business protocol analysis using formal methods. The research shows that proactive analysis has made this formal security verification possible and practical for complex protocols. These primary outcomes have raised awareness of security issues in e-tendering. The security solutions proposed in the protocol format are the first in e-tendering with verifiable security against common threat scenarios, and which are also practical for implementation. The procedures developed for securing the e-tendering process are generic and can be applied to other business domains. The study has made improvements in: establishing adequate security for a business process; applying proactive analysis prior to secure protocol construction; and verifying security of complex e-business protocols using tool aided formal methods.

Tato diplomová práce představuje model a prototyp kooperativního distributivního systému zálohování dat založeném na P2P komunikační síti. Návrh systému umožňuje uživatelům přispět svým lokálním volným místem na disku do systému výměnou za spolehlivé úložiště jejich dat u jiných uživatelů. Představené řešení se snaží splnit požadavky uživatelů na ukládání dat, zároveň však také řeší, jak se vypořádat s mírou nepředvídatelnosti uživatelů  ohledně poskytování volného místa. To je prováděno dvěma způsoby - využitím Reed - Solomon kódů a zároveň také tím, že poskytuje možnost nastavení parametrů dostupnosti. Jedním z těchto parametrů je časový rozvrh, který značí, kdy uživatel může nabídnout předvídatelný přínos do systému. Druhý parametr se týká spolehlivosti konkrétního uživatele v rámci jeho slíbeného časového úseku. Systém je schopen najít synchronizaci ukládaných dat na základě těchto parametrů. Práce se zaměřuje rovněž na řešení zabezpečení systému proti širšímu spektru možných útoků. Hlavním cílem je publikovat koncept a prototyp. Jelikož se jedná o relativně nové řešení, je důležitá také zpětná vazba od široké veřejnosti, která může produkt používat. Právě jejich komentáře a připomínky jsou podnětem pro další vývoj systému.

Thesis is analyzing czech laws which are related to medical documentation. Describes the points  which are mandatory for information system, so the medical documentation can be stored electronically. Includes various algorithms for implementation of certain electronic signature and for  identification of person. This thesis deals with asymmetric cryptography, specifically RSA, DSA, and ECDSA. Describes the hash functions and their functions and their characteristics. Describes the principle of the certificate, ways of its obtaining, invalidation and their formats. Analyzes medical information system and suggests ways to create a program for signing medical records. Then based on that analysis, the program is implemented. At the conclusion of the work is discussed, if created program meets the criteria.