J 2005

Decidability Issues for Extended Ping-Pong Protocol

HUTTEL, Hans a Jiří SRBA

Základní údaje

Originální název

Decidability Issues for Extended Ping-Pong Protocol

Název česky

Rozhodnutelnostni otazky pro rozsirene ping-pong protokoly

Autoři

HUTTEL, Hans (208 Dánsko) a Jiří SRBA (203 Česká republika, garant)

Vydání

Journal of Automated Reasoning, USA, Kluwer, 2005

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Spojené státy

Utajení

není předmětem státního či obchodního tajemství

Kód RIV

RIV/00216224:14330/05:00012769

Organizační jednotka

Fakulta informatiky

Klíčová slova anglicky

ping-pong protocols; decidability; recursion; replication

Štítky

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 6. 7. 2007 09:04, RNDr. JUDr. Vladimír Šmíd, CSc.

Anotace

ORIG CZ

V originále

We use some recent techniques from process algebra to draw several conclusions about the well studied class of ping-pong protocols introduced by Dolev and Yao. In particular we show that all nontrivial properties, including reachability and equivalence checking wrt. the whole van Glabbeek's spectrum, become undecidable for a very simple recursive extension of the protocol. The result holds even if no nondeterministic choice operator is allowed but reachability is shown to be decidable in polynomial time if only two parties are participating in the protocol. We also show that the calculus is capable of an implicit description of the active intruder, including full analysis and synthesis of messages in the sense of Amadio, Lugiez and Vanackere. We conclude by showing that reachability analysis for a replicative variant of the protocol becomes decidable.

Česky

We use some recent techniques from process algebra to draw several conclusions about the well studied class of ping-pong protocols introduced by Dolev and Yao. In particular we show that all nontrivial properties, including reachability and equivalence checking wrt. the whole van Glabbeek's spectrum, become undecidable for a very simple recursive extension of the protocol. The result holds even if no nondeterministic choice operator is allowed but reachability is shown to be decidable in polynomial time if only two parties are participating in the protocol. We also show that the calculus is capable of an implicit description of the active intruder, including full analysis and synthesis of messages in the sense of Amadio, Lugiez and Vanackere. We conclude by showing that reachability analysis for a replicative variant of the protocol becomes decidable.

Návaznosti

GA201/03/1161, projekt VaV
Název: Verifikace nekonečně stavových systémů
Investor: Grantová agentura ČR, Verifikace nekonečně stavových systémů
MSM0021622419, záměr
Název: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
1M0545, projekt VaV
Název: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky