Formalization And Verification Of Pub/Sub IoT Systems Using CSP

The Internet of Things(IoT)is a revolutionary technology in IT industries.It provides a unified device management platform for people by connecting the devices with the Internet.Among all kinds of IoT systems,the pub/sub IoT system is an IoT architecture based on the publish/subscribe scheme.Due to the superb message processing capability,it becomes the most popular IoT architecture.In the pub/sub IoT system,devices publish the collected data to the Internet,and users obtain the required environmental information by subscribing to IoT services.With the widespread application of the pub/sub IoT system,its security and privacy are attracting more and more attention from industries.ICN-IoT system and Authenticated Publish/Subscribe(AUPS)system are two pub/sub IoT systems designed to solve the security and privacy issues.ICN-IoT system aims to improve the security of the system by introducing Information-Centric Networking(ICN)into IoT.ICN identifies a network object by the name instead of IP address,which can better support content oriented security.AUPS adopts the traditional access control technology to improve the security of the critical data.In AUPS,users can subscribe to IoT services only after passing the access control.As two typical schemes to enhance the security and privacy of IoT frameworks,ICN-IoT system and AUPS system are attracting more and more attention.Hence,the study on the security and privacy of ICN-IoT system and AUPS system is extremely important.In this paper,formal methods are adopted to investigate the security and privacy of the above two pub/sub IoT systems.Using Communicating Sequential Processes(CSP),we establish formal models of ICN-IoT system and AUPS system.Feeding the models into the model checking tool PAT,we abstract the functional and security properties of the two models,and then verify the properties of the models.The verification results show that neither ICN-IoT system nor AUPS system can fully guarantee the security and privacy of the system once intruders appear.Hence,we improve the ICN-IoT model and AUPS model respectively,and then verify the improved model with PAT.According to the verification results,our work can improve the security and privacy of the two systems.