Algebraic method to model secure IoT

Process algebra can be considered to be one of the best methods to model IoT systems since it can represent the main properties of things in the systems: communication, movements, deadlines, etc. The best known algebras are π-calculus and mobile ambient. However, there are some limitations to model the different types of movements of the things with secure requirements. π-calculus passes the name of ports for indirect movements unrealistically, and mobile ambient uses ambient to synchronize asynchronous movements forcefully and unnaturally. This paper presents new process algebra, called δ-calculus, to model the different types of such synchronous movements for the things in IoT over some target geographical space. A process can be nested in another process, and their configuration will be changed by these movements. Any violation of the secure movements can be detected and prevented by the properties of the movements: synchrony, priority and deadline. To demonstrate the feasibility, a tool, called SAVE, was developed on the ADOxx metamodeling platform with an emergency medical system, which is one of the best suitable application domains for IoT.