IoT deployments grow in numbers and size, which makes questions of long-term support and maintainability increasingly important. Without scalable and standard-compliant capabilities to transfer the control of IoT devices between service providers, IoT system owners cannot ensure long-term maintainability, and risk vendor lock-in. The manual overhead must be kept low for large-scale IoT installations to be economically feasible. We propose AutoPKI, a lightweight protocol to update the IoT PKI credentials and shift the trusted domains, enabling the transfer of control between IoT service providers, building upon the latest IoT standards for secure communication and efficient encodings. We show that the overhead for the involved IoT devices is small and that the overall required manual overhead can be minimized. We analyse the fulfilment of the security requirements, and for a subset of them, we demonstrate that the desired security properties hold through formal verification using the Tamarin prover. 

The standard Constrained Application Protocol (CoAP) is a lightweight, web-transfer protocol based on the REST paradigm and specifically suitable for constrained devices and the Internet-of-Things. Object Security for Constrained RESTful Environment (OSCORE) is a standard, lightweight security protocol that provides end-to-end protection of CoAP messages. A number of methods exist for managing keying material for OSCORE, as to its establishment and update. This paper provides a detailed comparison of such methods, in terms of their features, limitations and security properties. Also, it especially considers the new key update protocol KUDOS, for which it provides a more extended discussion about its features and mechanics, as well as a formal verification of its security properties.

Distance-bounding anonymous credentials could be used for any location proofs that do not need to identify the prover and thus could make even notoriously invasive mechanisms such as location-based services privacy-preserving. There is, however, no secure distance-bounding protocol for general attribute-based anonymous credentials. Brands and Chaum’s (EUROCRYPT’93) protocol combining distance-bounding and Schnorr identification comes close, but does not fulfill the requirements of modern distance-bounding protocols. For that, we need a secure distance-bounding zero-knowledge proof-of-knowledge resisting mafia fraud, distance fraud, distance hijacking and terrorist fraud. Our approach is another attempt toward combining distance bounding and Schnorr to construct a distance-bounding zero-knowledge proof-of-knowledge. We construct such a protocol and prove it secure in the (extended) DFKO model for distance bounding. We also performed a symbolic verification of security properties needed for resisting these attacks, implemented in Tamarin. Encouraged by results from Singh et al. (NDSS’19), we take advantage of lessened constraints on how much can be sent in the fast phase of the distance-bounding protocol and achieve a more efficient protocol. We also provide a version that does not rely on being able to send more than one bit at a time which yields the same properties except for (full) terrorist fraud resistance.

This paper focus on providing a secure and trustworthy solution for virtual machine (VM) migration within an existing cloud provider domain, and/or to the other federating cloud providers. The infrastructure-as-a-service (IaaS) cloud service model is mainly addressed to extend and complement the previous Trusted Computing techniques for secure VM launch and VM migration case. The VM migration solution proposed in this paper uses a Trust_Token based to guarantee that the user VMs can only be migrated and hosted on a trustworthy and/or compliant cloud platforms. The possibility to also check the compliance of the cloud platforms with the pre-defined baseline configurations makes our solution compatible with an existing widely accepted standards-based, security-focused cloud frameworks like FedRAMP. Our proposed solution can be used for both inter- and intra-cloud VM migrations. Different from previous schemes, our solution is not dependent on an active (on-line) trusted third party; that is, the trusted third party only performs the platform certification and is not involved in the actual VM migration process. We use the Tamarin solver to realize a formal security analysis of the proposed migration protocol and show that our protocol is safe under the Dolev-Yao intruder model. Finally, we show how our proposed mechanisms fulfill major security and trust requirements for secure VM migration in cloud environments.