This HTML5 document contains 44 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
n19http://linked.opendata.cz/ontology/domain/vavai/riv/typAkce/
dctermshttp://purl.org/dc/terms/
n20http://purl.org/net/nknouf/ns/bibtex#
n10http://localhost/temp/predkladatel/
n22http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n4http://linked.opendata.cz/resource/domain/vavai/projekt/
n12http://linked.opendata.cz/ontology/domain/vavai/
n8https://schema.org/
n5http://linked.opendata.cz/resource/domain/vavai/zamer/
shttp://schema.org/
skoshttp://www.w3.org/2004/02/skos/core#
n3http://linked.opendata.cz/ontology/domain/vavai/riv/
n18http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216224%3A14330%2F06%3A00015981%21RIV10-GA0-14330___/
n2http://linked.opendata.cz/resource/domain/vavai/vysledek/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n11http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n15http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n21http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n14http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n13http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n7http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n16http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216224%3A14330%2F06%3A00015981%21RIV10-GA0-14330___
rdf:type
skos:Concept n12:Vysledek
dcterms:description
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. 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.
dcterms:title
Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols
skos:prefLabel
Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols
skos:notation
RIV/00216224:14330/06:00015981!RIV10-GA0-14330___
n3:aktivita
n14:P n14:Z
n3:aktivity
P(1M0545), P(GA201/03/1161), Z(MSM 143300001), Z(MSM0021622419)
n3:dodaniDat
n16:2010
n3:domaciTvurceVysledku
n22:2753057
n3:druhVysledku
n7:D
n3:duvernostUdaju
n15:S
n3:entitaPredkladatele
n18:predkladatel
n3:idSjednocenehoVysledku
486770
n3:idVysledku
RIV/00216224:14330/06:00015981
n3:jazykVysledku
n21:eng
n3:klicovaSlova
prefix rewriting; security protocols
n3:klicoveSlovo
n11:security%20protocols n11:prefix%20rewriting
n3:kontrolniKodProRIV
[13BDE420D8BF]
n3:mistoKonaniAkce
Beijing
n3:mistoVydani
Netherlands
n3:nazevZdroje
Automated Technology for Verification and Analysis (ATVA'06)
n3:obor
n13:IN
n3:pocetDomacichTvurcuVysledku
1
n3:pocetTvurcuVysledku
3
n3:projekt
n4:1M0545 n4:GA201%2F03%2F1161
n3:rokUplatneniVysledku
n16:2006
n3:tvurceVysledku
Esparza, Javier Srba, Jiří Delzanno, Giorgio
n3:typAkce
n19:WRD
n3:zahajeniAkce
2006-01-01+01:00
n3:zamer
n5:MSM0021622419 n5:MSM%20143300001
s:numberOfPages
15
n20:hasPublisher
Springer-Verlag
n8:isbn
3-540-47237-1
n10:organizacniJednotka
14330