HUTTEL, Hans a Jiří SRBA. Recursive Ping-Pong Protocols. In Proceedings of 4th International Workshop on Issues in the Theory of Security (WITS'04). Barcelona: Peter Ryan. s. 129-140. 2004.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Recursive Ping-Pong Protocols
Název česky Ping-pong protocoly s rekurzi
Autoři HUTTEL, Hans (208 Dánsko) a Jiří SRBA (203 Česká republika, garant).
Vydání Barcelona, Proceedings of 4th International Workshop on Issues in the Theory of Security (WITS'04), od s. 129-140, 12 s. 2004.
Nakladatel Peter Ryan
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Španělsko
Utajení není předmětem státního či obchodního tajemství
WWW URL
Kód RIV RIV/00216224:14330/04:00010072
Organizační jednotka Fakulta informatiky
Klíčová slova anglicky cryptographic protocols; automated verification; decidability
Štítky automated verification, cryptographic protocols, decidability
Změnil Změnil: Prof. Jiří Srba, Ph.D., učo 2841. Změněno: 18. 1. 2005 17:27.
Anotace
This paper introduces a process calculus with recursion which allows us to express an unbounded number of runs of the ping-pong protocols introduced by Dolev and Yao. We study the decidability issues associated with two common approaches to checking security properties, namely reachability analysis and bisimulation checking. Our main result is that our channel-free and memory-less calculus is Turing powerful, assuming that at least three principals are involved. We also investigate the expressive power of the calculus in the case of two participants. Here, our main results are that reachability and, under certain conditions, also strong bisimilarity become decidable.
Anotace česky
V clanku je studovano rekurzivni rozsireni tridy kryptografickych protokolu zalozeneho na ping-pong-ovem chovani. Je ukazano, ze dany formalismus je vypocetne ekvivalentni Turingove stroji a pro ruzne podtridy je dokazana rozhodnutelnost jistych verifikacnich problemu.
Návaznosti
GA201/03/1161, projekt VaVNázev: Verifikace nekonečně stavových systémů
Investor: Grantová agentura ČR, Verifikace nekonečně stavových systémů
MSM 143300001, záměrNázev: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů
VytisknoutZobrazeno: 19. 4. 2024 23:30