This blog post was written by ENTRUST partner Eindhoven University of Technology (TU/e).
The role of the Formal Verification component within the ENTRUST architecture is to apply the ’secure-by-design’ approach and to support the concept of zero-trust (i.e. ’never trust, always verify’) by applying formal verification techniques for all phases in the CMD (connected medical device) lifecycle, starting with its onboarding.
In ENTRUST, we recognize that applying formal verification for all internal operations might be unfeasible due to their inherent complex nature. To address this complexity, proper abstractions might be needed to achieve an effective verification process that converges and produces an outcome. These abstractions enable a granular definition of trust policies that need to be attested at runtime. Thus, attestation at runtime is needed only for those system and domain properties that cannot be formally verified at design time.
Formal Verification
Formal verification techniques provide a systematic way of discovering protocol flaws, making them an imperative step in the design of security protocols. There are various automated verification tools for security protocols in the literature, such as ProVerif, Tamarin, Scyther, and many others.
Automated verification tools for security protocols often require domain-specific expertise to use effectively, and each tool has different capabilities and limitations. As a result, users must acquire in-depth knowledge of multiple tools to verify the security of their protocols thoroughly and formally. Moreover, developers of the automated verification tools often have a formal verification background and might have a different approach than protocol designers, who often have a security background. Therefore, this usually leads to the need to gain formal verification expertise to be able to model security protocols.
Each verification tool provides means to verify specific security properties. For example, the unlinkability property can be modeled and verified using Tamarin but not with ProVerif. Tamarin analyzes the protocol traces (records of protocol executions) to reason about linkability across multiple sessions. This means it can determine whether different protocol runs can be correlated. On the other hand, ProVerif’s abstractions cannot express or analyze these relationships.
Domain-Specific Language
It is often difficult to formulate security properties in terms of the language of the verification tool, for example, in Tamarin. In ENTRUST, we propose a domain-specific language (DSL) that enables protocol designers to model and verify their protocols without requiring the knowledge of multiple automated protocol verification tools, therefore specifying them in a familiar notation.
On top of this DSL, we propose another level of abstraction that automatically generates models for various security properties to help designers kick off their verification process. Therefore, security properties are supported as first-class language constructs. Furthermore, based on these models, ProVerif and Tamarin models will be generated to enable protocol designers to verify various security properties by making use of multiple verification tools. This DSL aims to enable security protocol designers to model and verify their protocols in a familiar notation.