Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols

DELZANNO, Giorgio, Javier ESPARZA a Jiří SRBA. Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols. In Automated Technology for Verification and Analysis (ATVA'06). Netherlands: Springer-Verlag. 15 s. ISBN 3-540-47237-1. 2006.

Základní údaje

• Originální název: Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols
• Název česky: Monotonni Prefixove Prepisovani Rozsirene o Mnoziny a Overovani Rekurzivnich Ping-Pong Protokolu
• Autoři: DELZANNO, Giorgio (380 Itálie), Javier ESPARZA (724 Španělsko) a Jiří SRBA (203 Česká republika, garant).
• Vydání: Netherlands, Automated Technology for Verification and Analysis (ATVA'06), 15 s. 2006.
• Nakladatel: Springer-Verlag

Další údaje

• Originální jazyk: angličtina
• Typ výsledku: Stať ve sborníku
• Obor: 10201 Computer sciences, information science, bioinformatics
• Stát vydavatele: Nizozemské království
• Utajení: není předmětem státního či obchodního tajemství
• Kód RIV: RIV/00216224:14330/06:00015981
• Organizační jednotka: Fakulta informatiky
• ISBN: 3-540-47237-1
• UT WoS: 000241648200031
• Klíčová slova anglicky: prefix rewriting; security protocols
• Štítky: prefix rewriting, security protocols
• Příznaky: Mezinárodní význam, Recenzováno

Anotace

Ping-pong protocols with recursive definitions of agents, but without any active intruder, are a Turing powerful model. We show that under the environment sensitive semantics (i.e. by adding an active intruder capable of storing all exchanged messages including full analysis and synthesis of messages) some verification problems become decidable. In particular we give an algorithm to decide control state reachability, a problem related to security properties like secrecy and authenticity. The proof is via a reduction to a new prefix rewriting model called Monotonic Set-extended Prefix rewriting (MSP). We demonstrate further applicability of the introduced model by encoding a fragment of the ccp (concurrent constraint programming) language into MSP.

Anotace česky

Ping-pong protocols with recursive definitions of agents, but without any active intruder, are a Turing powerful model. We show that under the environment sensitive semantics (i.e. by adding an active intruder capable of storing all exchanged messages including full analysis and synthesis of messages) some verification problems become decidable. In particular we give an algorithm to decide control state reachability, a problem related to security properties like secrecy and authenticity. The proof is via a reduction to a new prefix rewriting model called Monotonic Set-extended Prefix rewriting (MSP). We demonstrate further applicability of the introduced model by encoding a fragment of the ccp (concurrent constraint programming) language into MSP.

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ů

• MSM 143300001, záměr: Ná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ů

• 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