%0 Conference Proceedings %T Formal Verification of the mERA-Based eServices with Trusted Third Party Protocol %+ GEMALTO (GEMALTO) %+ Université de Versailles Saint-Quentin-en-Yvelines (UVSQ) %A Christofi, Maria %A Gouget, Aline %Z Part 8: Applied Cryptography, Anonymity and Trust %< avec comité de lecture %( IFIP Advances in Information and Communication Technology %B 27th Information Security and Privacy Conference (SEC) %C Heraklion, Crete, Greece %Y Dimitris Gritzalis %Y Steven Furnell %Y Marianthi Theoharidou %I Springer %3 Information Security and Privacy Research %V AICT-376 %P 299-314 %8 2012-06-12 %D 2012 %R 10.1007/978-3-642-30436-1_25 %K privacy %K authentication %K mERA %K formal verification %K cryptographic protocol %K ProVerif %Z Computer Science [cs]Conference papers %X 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. %G English %2 https://inria.hal.science/hal-01518237/document %2 https://inria.hal.science/hal-01518237/file/978-3-642-30436-1_25_Chapter.pdf %L hal-01518237 %U https://inria.hal.science/hal-01518237 %~ IFIP %~ IFIP-AICT %~ UVSQ %~ IFIP-TC %~ IFIP-TC11 %~ IFIP-SEC %~ IFIP-AICT-376