Táto práca patrí do oblasti analýzi bezpečnosti protokolov. Za posledné desaťročia vzniklo množstvo protokolov na zaistenie bezpečnosti prenášaných správ, ale po čase sa objavili rôzne útoky na ne. Manipulovaním správy a vydávaním sa za niekoho iného je častokrát možné uskutočniť útok na protokol tak, že legitímny úèastník si bude myslie, že celá komunikácia prebieha v poriadku, ale pritom komunikuje iba s útočníkom. Na analýzu takéhoto typu útokov vznikli formálne analyzátory, ktoré umožňujú overiť bezpečnosť za istých dopredu špecifikovaných podmienok. V práci popisujeme analýzu protokolu IKE pomocou modálnych logík viery, ako aj rôzne redukcie stavového priestoru na prehľadávanie. Na príklade protokolu SRP-6 ukážeme ako v prostredí Scyther analyzovať protokoly so silným matematických zázemím použitím viacprotokolovej analýzy. Matematické pozadie modelujeme ako samostnatný protokol, ktorý vykonáva len jeden účastník.