Formal Verification of the mERA-Based eServices with Trusted Third Party Protocol

Internet services such as online banking, social networking and other web services require identification and authentication means. The European Citizen card can be used to provide a privacy-preserving authentication for Internet services enabling e.g. an anonymous age verification or other forms of anonymous attribute verification. The Modular Enhanced Symmetric Role Authentication (mERA) - based eServices with trusted third party protocol is a privacy-preserving protocol based on eID card recently standardized at CEN TC224 WG16. In this paper, we provide a formal analysis of its security by verifying formally several properties, such as secrecy, message authentication, unlinkability, as well as its liveness property. In the course of this verification, we obtain positive results about this protocol. We implement this verification with the ProVerif tool.