Which Italian university's team formally verified MTProto 2.0?

The Italian university team that formally verified MTProto 2.0 was from the University of Udine.

Researchers Marino Miculan and Nicola Vitacolonna, from the University of Udine’s Department of Mathematics, Computer Science and Physics, analyzed Telegram’s second-generation protocol. Their work was published in 2020 as Automated Symbolic Verification of Telegram’s MTProto 2.0 and later expanded in a 2023 Computers & Security paper.

MTProto 2.0 is the protocol family used at the core of Telegram’s messaging system. The Udine researchers modeled its authentication, cloud-chat, end-to-end encrypted chat and re-keying mechanisms. They examined properties including authentication, integrity, secrecy and perfect forward secrecy.

The result should not be read as an unconditional guarantee that Telegram is secure in every practical situation. The work used a symbolic model and identified limitations, including a possible unknown-key-share issue in re-keying. The researchers also noted that users must check key fingerprints to help detect a man-in-the-middle attack. The universities listed as alternatives—Turin, Pisa and Bologna—were not the institution named in this research.