The Internet of Things (IoT) comprises a wide range of interconnected devices capable of autonomous communication. As these devices exchange sensitive information, ensuring secure communication becomes critical. This paper addresses the challenge of securing peer-to-peer communication in IoT environments, particularly in scenarios involving social meeting arrangements. We propose a dedicated security protocol supporting device-to-device interactions for coordinating real-world meetings based on users’ proximity preferences. The protocol includes an initialisation phase, session key establishment, and a secure communication phase. Additionally, we present a supporting theoretical framework involving user applications, a semi-trusted server, and an algorithm for optimal meeting point selection. To validate the protocol’s effectiveness, we conduct a comprehensive evaluation using formal methods (BAN logic), informal reasoning, and automated verification tools. The results confirm that our protocol ensures key security properties, including mutual authentication, anonymity, revocation support, and resilience against common cyberattacks such as impersonation, replay, and man-in-the-middle attacks. To our knowledge, this is the first verified D2D protocol designed for real-time, privacy-aware social meeting coordination without relying on centralised infrastructure.

Our everyday lives cannot function without intelligent devices, which create the so-called Internet of Things networks. Internet of Things devices have various sensors and software to manage the work environment and perform specific tasks without human intervention. Internet of Things networks require appropriate security at various levels of their operation. In this article, we present a new security protocol that protects communication in IoT networks and enables interconnected devices to communicate and exchange information to increase the security of people living in urban agglomerations. The Control Station device evaluates the collected data about events that may threaten the life or health of residents and then notifies the Emergency Notification Center about it. The protocol guarantees the security of devices and transmitted data. We verified this using automatic verification technology, formal verification using Burrows, Abadi and Needham logic and informal analysis. The proposed protocol ensures mutual authentication, anonymity and revocation. Also, it is resistant to Man-in-the-middle, modification, replay and impersonation attacks. Compared to other protocols, our solution uses simple cryptographic techniques that are lightweight, stable and do not cause problems related to high communication costs. It does not require specialist equipment, so we can implement it using typical hardware. At each stage of protocol execution, communication occurs between two entities, so it does not require interaction between different entities, which may limit its adaptability in the context of interoperability.

The quality of air has emerged as a worldwide concern, primarily driven by the rapid growth of urban areas and industrialization. Poor air quality represents a significant environmental health risk in Europe, leading to severe health issues. It’s not only external air pollution that poses a problem; internal air pollution can be equally detrimental, resulting in adverse health consequences. Utilizing the Internet of Things (IoT) is a practical solution for monitoring and disseminating real-time information about air quality. Numerous IoT-based systems for air quality monitoring, employing micro-sensors for data collection, have been suggested. This proposed system enables real-time localized monitoring of air quality and data transmission to end-users. Furthermore, the work introduces a secure data transmission protocol to ensure the system’s security. This protocol offers protection against system-wide attacks and interception, which could otherwise be exploited for disinformation purposes.

In recent months, the demand for services provided on the Internet (scientific conferences, training, webinars) has increased. As this activity grew, so did cybercrime. Social networks share invitations to various training and webinars. We also receive similar announcements via e-mail. It is not difficult to accidentally click on the attached link. The submitted URL may contain a script. The script may infect our device or steal our login details. We have developed a new security protocol — Amelia, to protect against responding to a false invitation to a web event. Our protocol makes it possible to check if the link sent is valid. Also, it enables the generation of unique user identifiers. Amelia protocol provides users’ verification and distribution of symmetric session keys. We conducted a study of our protocol. We checked its vulnerability to Intruder attacks. The obtained results are promising. We did not find an attack on this protocol.

This paper presents our next research related to the use of SMT techniques for the analysis of security protocols. The behaviours of users and their changing knowledge during an investigated protocol executions are modelled as networks of communicating timed automata. The time properties are defined as the reachability properties of some, properly indicated states in the product automaton. We can do it using specially described time conditions, that can express dependencies between defined as a reachability property of some, chosen states in automata network, the possibility of performing some desired protocol steps and filling time constraints that use generation time of timestamps and lifetimes or/and networks delays. For our experiments we use boolean and SMT encodings that are the basis for respectively, SAT-and SMT-based bounded model checking. For SMT, the runs in product automaton are translated into the quantifier-free first-order formula. So far, we have implemented a well known bounded model checking algorithm and evaluated it for Needham-Schroeder Public Key, Needham Schroeder Symmetric Key, Woo Lam Pi and Wide Mouth Frog protocols. Now we show the tests carried out for the group of four known from the literature security protocols. We also compared our new SMT-based approach with a previous, only SAT-based, technique. For experiments, we used Minisat SAT solver, Z3, Yices2, CVC4 and MathSAT SMT solvers.