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

Giorgio Delzanno, Javier Esparza, Jiri Srba

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

Abstract

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.
OriginalsprogEngelsk
TitelAutomated Technology for Verification and Analysis : Proceedings of the 4th International Symposium, ATVA 2006, Beijing, China, October 23-26, 2006
Antal sider15
ForlagIEEE Computer Society Press
Publikationsdato2006
Sider415-429
ISBN (Trykt)9783540472377
DOI
StatusUdgivet - 2006
BegivenhedInternational Symposium on Automated Technology for Verification and Analysis (ATVA'06) - Bejing, Kina
Varighed: 23 okt. 200626 okt. 2006
Konferencens nummer: 4

Konference

KonferenceInternational Symposium on Automated Technology for Verification and Analysis (ATVA'06)
Nummer4
Land/OmrådeKina
ByBejing
Periode23/10/200626/10/2006
NavnLecture Notes in Computer Science
Nummer4218
ISSN0302-9743

Fingeraftryk

Dyk ned i forskningsemnerne om 'Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols'. Sammen danner de et unikt fingeraftryk.

Citationsformater