Formalization and Verification of Enhanced Group Communication CoAP

With the flourish of the Internet of Things (IoT), the group communication Constrained Application Protocol (CoAP) emerged at the historic moment, enabling homogeneous devices with constrained computing ability to communicate with ease. CoAP is widely used in transportation, health care and many other aspects. Hence, it is prominent to propose a flexible and efficient architecture for usage in such scenarios and study the data security and consistency of the architecture from the perspective of formal methods. In this paper, we extend the group communication CoAP model to the enhanced group communication CoAP by the introduction of smart gateways and binding to new security suites. We make further improvements to increase the scalability and flexibility of the architecture, making it more applicable in a healthcare scenario or smart home scenario. And we adopt process algebra Communicating Sequential Processes (CSP) with real-time extension to model the enhanced group communication CoAP. We use model checker PAT to verify eight properties of our model on an abstract level, including four basic properties and four security properties. We also conduct a simulation on the local machine for validation of the above properties on a more detailed level. Despite some simplifications of physical properties, both results of the verification and simulation show that the proposed architecture can satisfy those requirements and demonstrate a good possibility of being securely put into service.