The heterogeneity of Internet of Things (IoT) systems has so far prevented the definition of adequate standards, hence making it difficult to compare meaningfully the security degree of diverse architectural choices. This task can be nonetheless achieved with formal methodologies. However, the dedicated IoT literature shows no evidence of a universal model allowing the security evaluation of any arbitrary system. Based on these considerations, we propose a new model that aims at being global and all-encompassing. Our model can be used to fairly analyse the security level of different IoT systems and compare them in a significant way. It is designed to be adaptive with realistic definitions of the adversary’s (1) actions of interacting with IoT systems; (2) capabilities of accessing the data generated by and exchanged in IoT systems with established rules; and (3) objectives of attacking IoT systems according to the four recognised security properties of confidentiality, integrity, availability and soundness. Such a design enables the straightforward characterization of new adversaries. It further helps in providing a fine-grained security evaluation of IoT systems by either accurately describing attacks against the analysed systems or formally proving their guaranteed level of security.

The coronavirus pandemic is a new reality and it severely affects the modus vivendi of the international community. In this context, governments are rushing to devise or embrace novel surveillance mechanisms and monitoring systems to fight the outbreak. The development of digital tracing apps, which among others are aimed at automatising and globalising the prompt alerting of individuals at risk in a privacy-preserving manner is a prominent example of this ongoing effort. Very promptly, a number of digital contact tracing architectures has been sprouted, followed by relevant app implementations adopted by governments worldwide. Bluetooth, and specifically its Low Energy (BLE) power-conserving variant has emerged as the most promising short-range wireless network technology to implement the contact tracing service. This work offers the first to our knowledge, full-fledged review of the most concrete contact tracing architectures proposed so far in a global scale. This endeavour does not only embrace the diverse types of architectures and systems, namely centralised, decentralised, or hybrid, but it equally addresses the client side, i.e., the apps that have been already deployed in Europe by each country. There is also a full-spectrum adversary model section, which does not only amalgamate the previous work in the topic, but also brings new insights and angles to contemplate upon.