An IoT System for Air Pollution Monitoring with Safe Data Transmission.

Air pollution has become a global issue due to rapid urbanization and industrialization. Bad air quality is Europe's most significant environmental health risk, causing serious health problems. External air pollution is not the only issue; internal air pollution is just as severe and can also lead to adverse health outcomes. IoT is a practical approach for monitoring and publishing real-time air quality information. Numerous IoT-based air quality monitoring systems have been proposed using micro-sensors for data collection. These systems are designed for outdoor air quality monitoring. They use sensors to measure air quality parameters such as CO2, CO, PM10, NO2, temperature, and humidity. The data are acquired with a set of sensors placed on an electric car. They are then sent to the server. Users can subscribe to the list and receive information about local pollution. This system allows real-time localized air quality monitoring and sending data to customers. The work additionally presents a secure data transmission protocol ensuring system security. This protocol provides system-wide attack resiliency and interception, which is what existing solutions do not offer.

SAT and SMT-Based Verification of Security Protocols Including Time Aspects.

For many years various types of devices equipped with sensors have guaranteed proper work in a huge amount of machines and systems. For the proper operation of sensors, devices, and complex systems, we need secure communication. Security protocols (SP) in this case, guarantee the achievement of security goals. However, the design of SP is not an easy process. Sometimes SP cannot realise their security goals because of errors in their constructions and need to be investigated and verified in the case of their correctness. Now SP uses often time primitives due to the necessity of security dependence on the passing of time. In this work, we propose and investigate the SAT-and SMT-based formal verification methods of SP used in communication between devices equipped with sensors. For this, we use a formal model based on networks of communicating timed automata. Using this, we show how the security property of SP dedicated to the sensors world can be verified. In our work, we investigate such timed properties as delays in the network and lifetimes. The delay in the network is the lower time constraint related to sending the message. Lifetime is an upper constraint related to the validity of the timestamps generated for the transmitted messages.

Security protocols analysis including various time parameters.

Communication is a key element of everyone's life. Nowadays, we most often use internet connections for communication. We use the network to communicate with our family, make purchases, we operate home appliances, and handle various matters related to public administration. Moreover, the Internet enables us to participate virtually in various official meetings or conferences. There is a risk of losing our sensitive data, as well as their use for malicious purposes. In this situation, each connection should be secured with an appropriate security protocol. These protocols also need to be regularly checked for vulnerability to attacks. In this article, we consider a tool that allows to analyze different executions of security protocols as well as simulate their operation. This research enables the gathering of knowledge about the behaviour of the security protocol, taking into account various time parameters (time of sending the message, time of generation confidential information, encryption and decryption times, delay in the network, lifetime) and various aspects of computer networks. The conducted research and analysis of the obtained results enable the evaluation of the protocol security and its vulnerability to attacks. Our approach also assumes the possibility of setting time limits that should be met during communication and operation of the security protocol. We show obtained results on Andrew and Needham Schroeder Public Key protocols examples.