SROS Security through Model Checking

The goal of this work is to thoroughly identify the security problems in SROS communication. To do this, we use model checking method with the assist of tool event-b.

One of the useful paper: https://www.iiitb.ac.in/SELab/preprints/TR_IoTProtocolModel.pdf

The links to learn event-b: https://blog.csdn.net/Campsisgrandiflora/article/details/113575445?utm_medium=distribute.pc_relevant_t0.none-task-blog-2%7Edefault%7EBlogCommendFromMachineLearnPai2%7Edefault-1.control&depth_1-utm_source=distribute.pc_relevant_t0.none-task-blog-2%7Edefault%7EBlogCommendFromMachineLearnPai2%7Edefault-1.control

Model the protocol

Several considerations:

  1. The communication channel is not modeled in detail. We only consider if the participants of QoS has the correct access right.
  2. Status change is the key thing to model in this protocol; however, the initial model should be simple and clear.

Problems and Solutions

[03/07/2021] How to model rules? Set or what? My current consideration is to use set; for each node, there should be a corresponding set of rule.

[04/07/2021]

  1. How to code for restrictions: check this https://blog.csdn.net/Campsisgrandiflora/article/details/116108540.
  2. Finished the first model with subscribe only; no node-to-node layers but simply subscribing behaviors.
  3. Model finished. However, need to confirm on recipient privacy.