Bisimulation for Demonic Schedulers View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2009

AUTHORS

Konstantinos Chatzikokolakis , Gethin Norman , David Parker

ABSTRACT

Bisimulation between processes has been proven a successful method for formalizing security properties. We argue that in certain cases, a scheduler that has full information on the process and collaborates with the attacker can allow him to distinguish two processes even though they are bisimilar. This phenomenon is related to the issue that bisimilarity is not preserved by refinement. As a solution, we introduce a finer variant of bisimulation in which processes are required to simulate each other under the “same” scheduler. We formalize this notion in a variant of CCS with explicit schedulers and show that this new bisimilarity can be characterized by a refinement-preserving traditional bisimilarity. Using a third characterization of this equivalence, we show how to verify it for finite systems. We then apply the new equivalence to anonymity and show that it implies strong probabilistic anonymity, while the traditional bisimulation does not. Finally, to illustrate the usefulness of our approach, we perform a compositional analysis of the Dining Cryptographers with a non-deterministic order of announcements and for an arbitrary number of cryptographers. More... »

PAGES

318-332

Book

TITLE

Foundations of Software Science and Computational Structures

ISBN

978-3-642-00595-4
978-3-642-00596-1

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-642-00596-1_23

DOI

http://dx.doi.org/10.1007/978-3-642-00596-1_23

DIMENSIONS

https://app.dimensions.ai/details/publication/pub.1006002399


Indexing Status Check whether this publication has been indexed by Scopus and Web Of Science using the SN Indexing Status Tool
Incoming Citations Browse incoming citations for this publication using opencitations.net

JSON-LD is the canonical representation for SciGraph data.

TIP: You can open this SciGraph record using an external JSON-LD service: JSON-LD Playground Google SDTT

[
  {
    "@context": "https://springernature.github.io/scigraph/jsonld/sgcontext.json", 
    "about": [
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/08", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Information and Computing Sciences", 
        "type": "DefinedTerm"
      }, 
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0802", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Computation Theory and Mathematics", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Eindhoven University of Technology, The Netherlands", 
          "id": "http://www.grid.ac/institutes/grid.6852.9", 
          "name": [
            "Eindhoven University of Technology, The Netherlands"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Chatzikokolakis", 
        "givenName": "Konstantinos", 
        "id": "sg:person.011335525015.38", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011335525015.38"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Oxford Computing Laboratory, UK", 
          "id": "http://www.grid.ac/institutes/None", 
          "name": [
            "Oxford Computing Laboratory, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Norman", 
        "givenName": "Gethin", 
        "id": "sg:person.016323171577.36", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016323171577.36"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Oxford Computing Laboratory, UK", 
          "id": "http://www.grid.ac/institutes/None", 
          "name": [
            "Oxford Computing Laboratory, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Parker", 
        "givenName": "David", 
        "id": "sg:person.014007552600.37", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014007552600.37"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2009", 
    "datePublishedReg": "2009-01-01", 
    "description": "Bisimulation between processes has been proven a successful method for formalizing security properties. We argue that in certain cases, a scheduler that has full information on the process and collaborates with the attacker can allow him to distinguish two processes even though they are bisimilar. This phenomenon is related to the issue that bisimilarity is not preserved by refinement. As a solution, we introduce a finer variant of bisimulation in which processes are required to simulate each other under the \u201csame\u201d scheduler. We formalize this notion in a variant of CCS with explicit schedulers and show that this new bisimilarity can be characterized by a refinement-preserving traditional bisimilarity. Using a third characterization of this equivalence, we show how to verify it for finite systems. We then apply the new equivalence to anonymity and show that it implies strong probabilistic anonymity, while the traditional bisimulation does not. Finally, to illustrate the usefulness of our approach, we perform a compositional analysis of the Dining Cryptographers with a non-deterministic order of announcements and for an arbitrary number of cryptographers.", 
    "editor": [
      {
        "familyName": "de Alfaro", 
        "givenName": "Luca", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-642-00596-1_23", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-642-00595-4", 
        "978-3-642-00596-1"
      ], 
      "name": "Foundations of Software Science and Computational Structures", 
      "type": "Book"
    }, 
    "keywords": [
      "process", 
      "successful method", 
      "information", 
      "variants", 
      "notion", 
      "equivalence", 
      "certain cases", 
      "cases", 
      "collaborate", 
      "phenomenon", 
      "issues", 
      "anonymity", 
      "usefulness", 
      "full information", 
      "approach", 
      "number", 
      "method", 
      "refinement", 
      "analysis", 
      "order", 
      "announcements", 
      "characterization", 
      "system", 
      "properties", 
      "compositional analysis", 
      "attacker", 
      "CCS", 
      "third characterization", 
      "finite systems", 
      "new equivalence", 
      "arbitrary number", 
      "bisimulation", 
      "scheduler", 
      "bisimilarity", 
      "solution", 
      "probabilistic anonymity", 
      "Dining Cryptographers", 
      "cryptographers", 
      "security properties", 
      "finer variant", 
      "variant of CCS", 
      "explicit scheduler", 
      "non-deterministic order"
    ], 
    "name": "Bisimulation for Demonic Schedulers", 
    "pagination": "318-332", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1006002399"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-642-00596-1_23"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-642-00596-1_23", 
      "https://app.dimensions.ai/details/publication/pub.1006002399"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-05-10T10:42", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20220509/entities/gbq_results/chapter/chapter_230.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-642-00596-1_23"
  }
]
 

Download the RDF metadata as:  json-ld nt turtle xml License info

HOW TO GET THIS DATA PROGRAMMATICALLY:

JSON-LD is a popular format for linked data which is fully compatible with JSON.

curl -H 'Accept: application/ld+json' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-00596-1_23'

N-Triples is a line-based linked data format ideal for batch operations.

curl -H 'Accept: application/n-triples' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-00596-1_23'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-00596-1_23'

RDF/XML is a standard XML format for linked data.

curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-00596-1_23'


 

This table displays all metadata directly associated to this object as RDF triples.

120 TRIPLES      23 PREDICATES      69 URIs      62 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-642-00596-1_23 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author N6b87149b3631430cb9bbf89cf5100dec
4 schema:datePublished 2009
5 schema:datePublishedReg 2009-01-01
6 schema:description Bisimulation between processes has been proven a successful method for formalizing security properties. We argue that in certain cases, a scheduler that has full information on the process and collaborates with the attacker can allow him to distinguish two processes even though they are bisimilar. This phenomenon is related to the issue that bisimilarity is not preserved by refinement. As a solution, we introduce a finer variant of bisimulation in which processes are required to simulate each other under the “same” scheduler. We formalize this notion in a variant of CCS with explicit schedulers and show that this new bisimilarity can be characterized by a refinement-preserving traditional bisimilarity. Using a third characterization of this equivalence, we show how to verify it for finite systems. We then apply the new equivalence to anonymity and show that it implies strong probabilistic anonymity, while the traditional bisimulation does not. Finally, to illustrate the usefulness of our approach, we perform a compositional analysis of the Dining Cryptographers with a non-deterministic order of announcements and for an arbitrary number of cryptographers.
7 schema:editor N5ac7e797f9464c319627bf75a8176999
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf N95f6b6dba29d4d76a72d450335211f3a
12 schema:keywords CCS
13 Dining Cryptographers
14 analysis
15 announcements
16 anonymity
17 approach
18 arbitrary number
19 attacker
20 bisimilarity
21 bisimulation
22 cases
23 certain cases
24 characterization
25 collaborate
26 compositional analysis
27 cryptographers
28 equivalence
29 explicit scheduler
30 finer variant
31 finite systems
32 full information
33 information
34 issues
35 method
36 new equivalence
37 non-deterministic order
38 notion
39 number
40 order
41 phenomenon
42 probabilistic anonymity
43 process
44 properties
45 refinement
46 scheduler
47 security properties
48 solution
49 successful method
50 system
51 third characterization
52 usefulness
53 variant of CCS
54 variants
55 schema:name Bisimulation for Demonic Schedulers
56 schema:pagination 318-332
57 schema:productId N513a14c35fbd40219175cc00b1f956a1
58 Nfaddc0cb9e004d8c8a61ad3711dd947f
59 schema:publisher N17a2c2c845a441bb93a293e5b4c5ed41
60 schema:sameAs https://app.dimensions.ai/details/publication/pub.1006002399
61 https://doi.org/10.1007/978-3-642-00596-1_23
62 schema:sdDatePublished 2022-05-10T10:42
63 schema:sdLicense https://scigraph.springernature.com/explorer/license/
64 schema:sdPublisher Nde0ac10b5d5246de9a77905af9d7acc1
65 schema:url https://doi.org/10.1007/978-3-642-00596-1_23
66 sgo:license sg:explorer/license/
67 sgo:sdDataset chapters
68 rdf:type schema:Chapter
69 N17a2c2c845a441bb93a293e5b4c5ed41 schema:name Springer Nature
70 rdf:type schema:Organisation
71 N4157d04cdb614e98a1e9c50e911c2b12 rdf:first sg:person.016323171577.36
72 rdf:rest Nadb88603d4af4007ac35c5ab8902fcda
73 N513a14c35fbd40219175cc00b1f956a1 schema:name dimensions_id
74 schema:value pub.1006002399
75 rdf:type schema:PropertyValue
76 N5ac7e797f9464c319627bf75a8176999 rdf:first Na6f9328084444b5fac080a41a7fb4b75
77 rdf:rest rdf:nil
78 N6b87149b3631430cb9bbf89cf5100dec rdf:first sg:person.011335525015.38
79 rdf:rest N4157d04cdb614e98a1e9c50e911c2b12
80 N95f6b6dba29d4d76a72d450335211f3a schema:isbn 978-3-642-00595-4
81 978-3-642-00596-1
82 schema:name Foundations of Software Science and Computational Structures
83 rdf:type schema:Book
84 Na6f9328084444b5fac080a41a7fb4b75 schema:familyName de Alfaro
85 schema:givenName Luca
86 rdf:type schema:Person
87 Nadb88603d4af4007ac35c5ab8902fcda rdf:first sg:person.014007552600.37
88 rdf:rest rdf:nil
89 Nde0ac10b5d5246de9a77905af9d7acc1 schema:name Springer Nature - SN SciGraph project
90 rdf:type schema:Organization
91 Nfaddc0cb9e004d8c8a61ad3711dd947f schema:name doi
92 schema:value 10.1007/978-3-642-00596-1_23
93 rdf:type schema:PropertyValue
94 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
95 schema:name Information and Computing Sciences
96 rdf:type schema:DefinedTerm
97 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
98 schema:name Computation Theory and Mathematics
99 rdf:type schema:DefinedTerm
100 sg:person.011335525015.38 schema:affiliation grid-institutes:grid.6852.9
101 schema:familyName Chatzikokolakis
102 schema:givenName Konstantinos
103 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011335525015.38
104 rdf:type schema:Person
105 sg:person.014007552600.37 schema:affiliation grid-institutes:None
106 schema:familyName Parker
107 schema:givenName David
108 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014007552600.37
109 rdf:type schema:Person
110 sg:person.016323171577.36 schema:affiliation grid-institutes:None
111 schema:familyName Norman
112 schema:givenName Gethin
113 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016323171577.36
114 rdf:type schema:Person
115 grid-institutes:None schema:alternateName Oxford Computing Laboratory, UK
116 schema:name Oxford Computing Laboratory, UK
117 rdf:type schema:Organization
118 grid-institutes:grid.6852.9 schema:alternateName Eindhoven University of Technology, The Netherlands
119 schema:name Eindhoven University of Technology, The Netherlands
120 rdf:type schema:Organization
 




Preview window. Press ESC to close (or click here)


...