"[1AD73BE00E4D]" . "Recursive Ping-Pong Protocols" . "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." . "Recursive Ping-Pong Protocols"@en . "Barcelona, Spain" . "Huttel, Hans" . "14330" . . "2004-01-01+01:00"^^ . "RIV/00216224:14330/04:00010072!RIV08-MSM-14330___" . . "Ping-pong protocoly s rekurzi"@cs . . "Recursive Ping-Pong Protocols" . "1"^^ . . . . "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."@cs . . . . . "2"^^ . "Peter Ryan" . . . "Srba, Ji\u0159\u00ED" . . "12"^^ . "cryptographic protocols; automated verification; decidability"@en . "Ping-pong protocoly s rekurzi"@cs . "RIV/00216224:14330/04:00010072" . "Proceedings of 4th International Workshop on Issues in the Theory of Security (WITS'04)" . . . "Barcelona" . "Recursive Ping-Pong Protocols"@en . "129-140" . . "583865" . "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."@en . . . "P(GA201/03/1161), Z(MSM 143300001)" .