2004
Recursive Ping-Pong Protocols
HUTTEL, Hans a Jiří SRBAZákladní údaje
Originální název
Recursive Ping-Pong Protocols
Název česky
Ping-pong protocoly s rekurzi
Autoři
HUTTEL, Hans a Jiří SRBA
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
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í
Odkazy
Kód RIV
RIV/00216224:14330/04:00010072
Organizační jednotka
Fakulta informatiky
Klíčová slova anglicky
cryptographic protocols; automated verification; decidability
Změněno: 18. 1. 2005 17:27, Prof. Jiří Srba, Ph.D.
V originále
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.
Č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 VaV |
| ||
| MSM 143300001, záměr |
|