It is well known that designing and coding security protocols is an error-prone task. Several flaws are constantly being found in protocol specifications and implementations, and some of them are discovered even years after their issue. The formal modelling and verification of security protocols, through formal methods, can mitigate this problem and increase the confidence in the final artefact security, by backing protocol specifications and implementations with rigorous proofs about their expected behavior in the presence of attackers.
For this reason, the security model designed within RAINBOW, which includes security protocols for aspects like key exchange and remote attestation, has to be verified formally, by verifying that the proposed protocols, satisfy the security requirements of RAINBOW.
In formal security protocol verification, two main types of models are used: the symbolic model and the computational model. The symbolic model is a more abstract model, which makes it easier to build automatic verification tools, while the computational model is closer to the real execution of protocols, but the proofs are more difficult to automate. This difference depends mainly on the fact that, in the symbolic model, cryptographic primitives are considered as perfect black- boxes, modelled by function symbols in an algebra of terms, possibly with equations. Messages are terms on these primitives and the adversary can compute only using these primitives. On the other hand, in the computational model, a message is a bit-string and the protocol is formalised as a probabilistic polynomial-time Turing machine. The security of the protocol is then defined in terms of a game, where an arbitrary probabilistic polynomial-time Turing machine, which models the adversary, interacts with the protocol. The analysed protocol is secure if all adversaries have a negligible probability of winning the game.
Compared to the computational model, the symbolic model abstracts many details away. On the one hand, this means that the symbolic model may miss protocol flaws that are captured by the computational model. Most notably, the possibility of attacks on the protocol that exploit weaknesses related to the specific cryptosystems used in the protocol is missed by analyses made using symbolic models. On the other hand, although the symbolic model is considerably simpler than the computational one, many practically relevant attacks on a protocol can still be found using this kind of model, including all those that are enabled by logical flaws. e.g., man-in-the-middle attacks. Moreover, because of the relative simplicity of the model, several fully automated tools are available that can find security proofs for a wide range of security protocols: ProVerif, AVISPA, Maude-NPA, Scyther, Tamarin. For the computational model approach, there are few tools, like cryptoverif, that can automatically perform a verification, but they make assumptions about cryptographic primitives that are not satisfied by the most commonly used cryptographic systems.
Based on the above considerations, even though the symbolic model does have some limitations, it is the most appropriate approach for the purpose of achieving good confidence that the logic of the protocols is correct, with a reasonable effort.
