One of the links shared by the comment you're linking to points to a paper which concludes:
> We have presented the formalisation of the MTProto 2.0 protocol suite in the applied π-calculus, and its analysis using the protocol verifier ProVerif. This approach adopts the symbolic Dolev-Yao threat model: an active intruder can intercept, modify, forward, drop, replay or reflect any message. Within this model, we have provided a fully automated proof of the soundness of MTProto 2.0’s protocols for first authentication, normal chat, end-to-end encrypted chat, and rekeying mechanisms with respect to several security properties, including authentication, integrity, secrecy and perfect forward secrecy, also in the presence of malicious servers and clients. Moreover, we have discovered that the rekeying protocol is vulnerable to a theoretical unknown key-share (UKS) attack [ 5 ]: a malicious client B, with the help of another client E, can induce a client A to believe that she (still) shares a secret key with E, and instead A shares the key with B. The practical exploitability of this attack in actual implementations is still to be investigated. Our formalization covers also the behaviour of the users, when relevant; e.g., if the users do not check the fingerprints of their shared keys, a MitM attack is possible.
One of the links shared by the comment you're linking to points to a paper which concludes:
> We have presented the formalisation of the MTProto 2.0 protocol suite in the applied π-calculus, and its analysis using the protocol verifier ProVerif. This approach adopts the symbolic Dolev-Yao threat model: an active intruder can intercept, modify, forward, drop, replay or reflect any message. Within this model, we have provided a fully automated proof of the soundness of MTProto 2.0’s protocols for first authentication, normal chat, end-to-end encrypted chat, and rekeying mechanisms with respect to several security properties, including authentication, integrity, secrecy and perfect forward secrecy, also in the presence of malicious servers and clients. Moreover, we have discovered that the rekeying protocol is vulnerable to a theoretical unknown key-share (UKS) attack [ 5 ]: a malicious client B, with the help of another client E, can induce a client A to believe that she (still) shares a secret key with E, and instead A shares the key with B. The practical exploitability of this attack in actual implementations is still to be investigated. Our formalization covers also the behaviour of the users, when relevant; e.g., if the users do not check the fingerprints of their shared keys, a MitM attack is possible.