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

Giorgio Delzanno; Javier Esparza; Jiri Srba

doi:10.1007/11901914_31

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

Giorgio Delzanno, Javier Esparza, Jiri Srba

Department of Computer Science

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-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.

Original language	English
Title of host publication	Automated Technology for Verification and Analysis : Proceedings of the 4th International Symposium, ATVA 2006, Beijing, China, October 23-26, 2006
Number of pages	15
Publisher	IEEE Computer Society Press
Publication date	2006
Pages	415-429
ISBN (Print)	9783540472377
DOIs	https://doi.org/10.1007/11901914_31
Publication status	Published - 2006
Event	International Symposium on Automated Technology for Verification and Analysis (ATVA'06) - Bejing, China Duration: 23 Oct 2006 → 26 Oct 2006 Conference number: 4

Conference

Conference	International Symposium on Automated Technology for Verification and Analysis (ATVA'06)
Number	4
Country/Territory	China
City	Bejing
Period	23/10/2006 → 26/10/2006

Series	Lecture Notes in Computer Science
Number	4218
ISSN	0302-9743

Access to Document

10.1007/11901914_31

AUB Link

Search for the material in Aalborg University Library's search engine

Cite this

Delzanno, Giorgio ; Esparza, Javier ; Srba, Jiri. / Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols. Automated Technology for Verification and Analysis: Proceedings of the 4th International Symposium, ATVA 2006, Beijing, China, October 23-26, 2006. IEEE Computer Society Press, 2006. pp. 415-429 (Lecture Notes in Computer Science; No. 4218).

@inproceedings{474eebe0a0de11db8ed6000ea68e967b,

title = "Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols",

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.",

author = "Giorgio Delzanno and Javier Esparza and Jiri Srba",

year = "2006",

doi = "10.1007/11901914_31",

language = "English",

isbn = "9783540472377",

series = "Lecture Notes in Computer Science",

publisher = "IEEE Computer Society Press",

number = "4218",

pages = "415--429",

booktitle = "Automated Technology for Verification and Analysis",

address = "United States",

note = "International Symposium on Automated Technology for Verification and Analysis (ATVA'06) ; Conference date: 23-10-2006 Through 26-10-2006",

}

Delzanno, G, Esparza, J & Srba, J 2006, Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols. in Automated Technology for Verification and Analysis: Proceedings of the 4th International Symposium, ATVA 2006, Beijing, China, October 23-26, 2006. IEEE Computer Society Press, Lecture Notes in Computer Science, no. 4218, pp. 415-429, International Symposium on Automated Technology for Verification and Analysis (ATVA'06), Bejing, China, 23/10/2006. https://doi.org/10.1007/11901914_31

Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols. / Delzanno, Giorgio; Esparza, Javier; Srba, Jiri.
Automated Technology for Verification and Analysis: Proceedings of the 4th International Symposium, ATVA 2006, Beijing, China, October 23-26, 2006. IEEE Computer Society Press, 2006. p. 415-429 (Lecture Notes in Computer Science; No. 4218).

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review

TY - GEN

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

AU - Delzanno, Giorgio

AU - Esparza, Javier

AU - Srba, Jiri

N1 - Conference code: 4

PY - 2006

Y1 - 2006

N2 - 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.

AB - 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.

U2 - 10.1007/11901914_31

DO - 10.1007/11901914_31

M3 - Article in proceeding

SN - 9783540472377

T3 - Lecture Notes in Computer Science

SP - 415

EP - 429

BT - Automated Technology for Verification and Analysis

PB - IEEE Computer Society Press

T2 - International Symposium on Automated Technology for Verification and Analysis (ATVA'06)

Y2 - 23 October 2006 through 26 October 2006

ER -

Delzanno G, Esparza J, Srba J. Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols. In Automated Technology for Verification and Analysis: Proceedings of the 4th International Symposium, ATVA 2006, Beijing, China, October 23-26, 2006. IEEE Computer Society Press. 2006. p. 415-429. (Lecture Notes in Computer Science; No. 4218). doi: 10.1007/11901914_31

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

Abstract

Conference

Access to Document

AUB Link

Fingerprint

Cite this