Hi, one of the authors here, and first-time poster on Lobsters! Just wanted to clarify that this is not (yet) a full verification of Telegram’s protocol: mistakes notwithstanding, we have formally proved it correct “at a high level” (that’s what “symbolic” in the title stands for), and of course only with respect to the security model described in the paper (there may be other properties one might want to consider, and we are working to extend our analysis). Besides, “correct” here means “correct with respect to Telegram’s specification”: that is different from “it is secure to use for private communications”. For instance, cloud chats are not e2e-encrypted, secret chats are not the default, and there are other usability issues in practice. Finally, the verification of MTProto 2.0’s ad-hoc encryption scheme (the most controversial part of Telegram’s protocol) is still an open problem: that can’t be done at the symbolic level, and we are working on computational and/or manual proofs (that it is correct or broken). In the paper, the encryption scheme is abstracted as an ideal primitive providing perfect cryptography. Anyway, should MTProto’s encryption scheme turn out to be insecure, the results of the paper would still hold (in practice, one could plug a better encryption scheme to get a secure protocol).
Thanks for the good work!
Did you consider symbolic verification of Signal and its protocol? We are planning to review this paper, however it would be nice to have similar verification / comparison to Signal’s protocols.
That has been done already by another research group: https://hal.inria.fr/hal-01575923/document
Also i seen somewhere mtproto model for verifpal too.
Yeah, I’ve seen MTProto mentioned in some slides about Verifpal, but I’ve never found any published code. Verifpal is a great tool to learn about automated cryptographic proofs, though!
Proverif and verifpal is easy for me in both directions. Lets see what can i do. I will take a look.