Formal verification of security properties for remote attestation protocols

Formal verification refers to a set of techniques based on formal methods, which aim to assess whether a certain formal model is well-defined or that a system satisfies some specific properties. This kind of formal analysis lends itself very well to the use of automated algorithms that help reach the desired outcome in reasonable time. This technique has been successfully applied in the verification of cryptographic protocols in the literature, to evaluate their security in case of hostile actors interference; the main advantage of this analysis is its ability to identify potential vulnerabilities that would not be intuitively detectable, as was the case for widely used protocols which believed secure for years. A possible application of cryptographic protocols is to protect the process of Remote Attestation, which is a key component of a trusted computing environment. In particular, the attestation purpose is to assess whether a certain system, that wishes to join a trusted network, is not behaving maliciously. When the attestation process is carried out through a public network, it is necessary to employ a number of security measures that can prevent adversaries from illegitimately obtaining a trusted state. Some automatic formal verification techniques, through the use of the popular and successful tool ProVerif and its extension, are applied on two main security protocol for Remote Attestation procedures developed in the context of a trusted fog computing platform: a simpler implementation that is proved to have some flaws in its definition and a more complex one, as an enhanced version of the previous, fixing most of the initial issues. The results obtained from the analysis are only partial with respect to the initial objective to prove all properties on both protocols, since the tool used is shown to not be the ideal choice for this particular application.