Resource-constrained computational devices with Internet connectivity are collectively termed Internet of Things (IoT) devices, and are particularly vulnerable to attacks, as they cannot afford the implementation of proactive defences against malicious code. IoT devices not only become easy targets for hackers but also a useful weapon to launch further attacks on major services. Verifying the integrity of a remote device is essential to maintaining a secure computer network, as malicious or erroneous code could be used, for example, to compromise secrets and escalate privileges remotely. The current practice is to rely on forensic techniques such as memory attestation and erasure protocols. The former verifies the integrity of a device’s memory and the latter certifies memory has been erased. Both result in devices without unexpected contents in memory. Current attestation and erasure protocols are restricted to highly controlled environments. Either the protocol needs direct access to the device’s hardware, or it requires the device to be isolated from the network. Both restrictions are hard to meet in large-scale networks that exhibit a high level of heterogeneity, such as IoT networks. On the one hand, the area of Security Protocol Analysis produces protocols that resist attackers with full control over the network. On the other hand, memory erasure and attestation protocols are limited in terms of their ability to cope with network attackers, i.e. attackers able to intercept and manipulate network messages. This project will use current experience in developing security protocols and adversary models to make novel memory attestation and erasure protocols resilient against network attackers. To this end, we will identify the limits of memory erasure/attestation protocols in terms of the attacker model and security properties they can cope with, and put forward more robust, efficient and versatile protocols.