Automated Symbolic Verification of Telegram's MTProto 2.0
arxiv.org
arxiv.org
In the light of these results, we can affirm that MTProto 2.0 does not present any logical flaw. Vulnerabilities can arise only from the cryptographic primitives, from implementation flaws (e.g. insufficient checks), from side-channels exfiltration (such as timing or traffic analysis), or from incorrect user behaviour. Hence, these are the aspects which deserve further investigation and particular care in the implementation and use of this protocol.
The basic encryption primitive of MTProto 2.0 is assumed to be a perfect authenticated encryption scheme (IND-CCA and INT-CTXT). Although no attack on this scheme is known to date, these properties need to be formally proved in order to deem MTProto 2.0 definitely secure. This proof cannot be done in a symbolic model like ProVerif’s, but it can be achieved in a computational model, using tools like CryptoVerif or EasyCrypt [5, 2], which we leave to future work. However, even in the very unlikely case that a flaw is found in the encryption scheme, the results in this paper would be still valid: the protocol could be used just by replacing the encryption scheme, and no other changes would be required.
[/quote]
This analysis the protocol, not the cryptographic primitives, which was what get criticized
“ Following this approach, in our model we consider the message encryption scheme used in MTProto 2.0 as a robust authenticated-encryption scheme, abstracting from its actual implementation.”
So yeah, they’re abstracting away the AE part of it, which may not be an accurate reflection of what telegram uses.
That being said, they’re aware this is a strong assumption:
“ Namely, the only assumption we make is that the latter is an authenticated encryption scheme, guaranteeing both integrity of ciphertext (INT-CTXT) and indistinguishability of chosen plaintext (IND-CPA). These properties are difficult to prove in a symbolic model like ProVerif’s, but can be proved in a computational model, e.g. using tools like CryptoVerif or EasyCrypt [5, 2]. This assumption may appear strong, especially considering that Telegram has been widely criticized for its design choices (such as ad hoc cryptographic primitives and an unusual encryption mode), and vulnerabilities have been found in MTProto v1.0 (but actually, none of these attacks have been replicated on the new MTProto 2.0). Still, proving the logical correctness of the protocol under a fairly general threat model is very important because, if a weakness in the protocol exists, it must be looked for in the “lower-level” part of the protocol, among the chosen cryptographic functions and other implementation choices.”
The key exchange is a strange choice for a modern greenfields project but hardly that noteworthy.
It's was implemented in OpenSSL 15 years ago.
https://github.com/openssl/openssl/blob/master/crypto/aes/ae...
Papers are literally disappeared in first month of public Telegram release.
Source: Myself working at first months after public Telegram release on Android client.
https://patents.google.com/patent/US6973187B2/en
It’s written in patent-ese, but it looks like a mediocre attempt at an efficient authenticated encryption scheme, and it doesn’t appear to use the building blocks of modern schemes. I can’t even find a coherent description of what the “non-cryptographic manipulation detection code” is or what properties are required.
Meanwhile, the Telegram protocol is new. Surely it should use a standard AEAD with a security proof.
About this threat, the paper says:
"Concerning implementation flaws, our formalisation can be used as a reference for the correct implementation of MTProto 2.0 clients (and servers). Tools like Spi2Java or FS2PV can be useful to this end."
This is why it's important to have them in the same code base.
I've heard about attempts at inria to implement signal/double ratchet using F-star and verify the correctness. But no such implementation seems to be publicly available.
One of the things I'm interested in is to see if it's possible to bring these verification technologies to more mainstream programming languages such as python.
https://github.com/adsharma/zre_raft/blob/main/zre_raft/zre_...
is something I'd love to verify.
FWIW, not exactly the same but related: Telegram releases verifiable builds in both Play Store and App Store.
AFAIK they are pretty much alone among mainstream IM services to offer this.
Signal too: https://github.com/signalapp/Signal-Android/blob/master/repr...
Regarding the iOS app store, Telegram writes:
> As things stand now, you'll need a jailbroken device, at least 1,5 hours and approximately 90GB of free space to properly set up a virtual machine for the verification process.
https://core.telegram.org/reproducible-builds#reproducible-b...
It's a manual process within a new VM. I wouldn't be surprised if it frequently breaks without anyone noticing. But at least they're trying, I'm not aware of any better approach. Apple's GUI-focussed approach doesn't make these things easy.
If you look at the iOS repo, first there is no license associated with the repo. Second, there are lots of people reporting failed builds in the issue tracker without a response.
https://github.com/TelegramMessenger/Telegram-iOS
https://github.com/TelegramMessenger/Telegram-iOS/issues/377
[0]: https://www.businessofapps.com/data/telegram-statistics/
Secret chat is supported on the macOS native client (there are two clients, the cross-desktop one is electron-based, the native one is in Swift and shares code with the iOS client.
Is this not the native one? Because the other one had a higher version number and I was running it on Linux for a while.
The secret chat button is hidden behind 3 levels on the macOS native app. You have to click the contact's icon > More > Secret. It's the same deal on iOS.
I installed it outside of the App Store.
I don't think so, the one I use on Linux uses Qt.
Here's the various current app details: https://telegram.org/apps#source-code
They use the same 7 year old russian article [1] to show the said broken crpyto, despite that being written like the month telegram launched on HN. They have fixed all these long ago and even rolled out MTProto 2.0.
Nobody wants to break this crypto despite criticizing it. There's a 300K$ cash prize [2].
[0] - https://news.ycombinator.com/item?id=6913632
[1] - https://m.habr.com/en/post/206900/
[2] - https://telegram.org/faq#q-what-if-my-hacker-friend-says-the...
Also that there's no crypto for every group chat and every default 1:1 chat.
I'd rather Telegram be able to read my chats with a way I can control, that use whatsapp and feed all my messages into google drive with no way for me to control my contact's backup settings.
Durov has answered this multiple times. He even explained it yesterday.
So, what is the Telegram excuse for not being able to put the same amount of effort? That sounds dubious to say it is reasonable when in fact it is only the very bare minimum that everyone does.
As a matter of fact, trusted computing is a very active and practical field as far as I know.
That's up to the user, I've never backed up my WA data to any cloud service.
Telegram's UX is better for security. You know when you can expect difference levels of security, and the best that can be done is just as good if not better.
Fair comment. Still, at that point, you're trusting a third party just like in Telegram case. In any case, if anything, the default settings in WA are closer to an ideal E2EE than Telegram.
The default setting in whatsapp is to show a full screen prompt asking you to backup to google drive. 98% of users enable this, meaning it is worse than Telegram. You don't even know who has enabled it.
You don't trust WA nor Facebook regarding your data, which is what we were discussing. You do trust them regarding your metadata, and it's indeed a problem.
You don't but almost every person you chat with backs it up.
They back it up. Your chats are included in the backups that happens to their Google accounts.
WhatsApp pushes the drive backups frequently. Every single person I chat with has enabled it. I've checked.
https://telegram.org/faq#q-why-not-just-make-all-chats-39sec...
Technically, the correct way to use e2ee chat on both Signal and Telegram is to verify the key fingerprint using a secure channel separate from Telegram. In reality, few people do it, so the default makes a huge difference.
If all of my Signal chats are e2ee by default, and I operate under the assumption that most if not all of my chats are encrypted and secure by default, when a chat that really needs to be secured comes in, I wouldn't think of verifying the fingerprint in a separate channel first, because Signal didn't train me to do so. If it did, Signal would have been a lot more annoying to use, because it'll have to pop up warnings and all that.
Enabling e2ee in Telegram is an explicit act, which means that what that mean is enabled, I know for sure I need to make sure it's really secure, and it will trigger my memory about verifying fingerprints. I would argue this trains the user to think more about operational security instead of just theoretical information security.
As far as I can understand, Telegram's secrecy by default is __good enough__. They control all of their data centers and internal networks, and they have been known to refuse to comply with government orders. Given that I continue to use Apple and Google services with similar or lessor guarantees, I consider that good enough, and I'll choose my messaging app based on secondary factors such as usability and features. Telegram wins hands down in these areas.
I understand your argument about the marketing and UI blurring the definitions, but I disagree on the fundamental issue. My messages should be readable only to me and whomever I sent them to.
As others have pointed out, there's no good reason to have no E2EE by default in 2020.
Signal also protects against a whole lot of passive attacks (e.g. bulk collection), which Telegram doesn't. Any vulnerability in Telegram's servers and all your chat history is made public. I don't know how Signal secures their servers, and I don't have to care.
Security-wise there's no good reason to use Telegram vs Signal.
In Signal, at least as recently as in August, you may still get messages from the group you just quit if a member send a message to the group before the group metadata is reconciled. This happens because every group message is an e2ee message to every other group member.
If you have signed in from two devices, disappearing messages that have disappeared on one device will still show up on another. This happens because the server cannot store or sync the states of two sessions participating in the same chat.
Signal is full of little distributed system data consistency bugs that you just wouldn't expect in traditional client-server model application.
If your point is that telegram is no more private than a public message forum like, well then OK.
But I think that's at odds with the "only problem is hand rolled crypto" comment I was replying to.
https://en.wikipedia.org/wiki/Blocking_Telegram_in_Russia
Please don't post such accusations without sources.
Relevant article from Moxie Marlinespike: https://archive.vn/SIl9M
A theorized valid attack that was deemed invalid by the fine print in their bounty program: https://web.archive.org/web/20181118154823/https://www.alexr...
These are criticisms of MTproto 1, there is barely any literature about the new version.
But Moxie (or any other cryptographer) could use the money for Signal's development. It's a large amount.