Automated Symbolic Verification of Telegram's MTProto 2.0(arxiv.org)
arxiv.org
Automated Symbolic Verification of Telegram's MTProto 2.0
https://arxiv.org/abs/2012.03141
54 comments
Another interesting quote:
“ 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.”
“ 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.”
Apart from choosing RSA over elliptical curves, which primitive in particular is the problem? Otherwise under the hood it's AES256-IGE and SHA256?
The key exchange is a strange choice for a modern greenfields project but hardly that noteworthy.
The key exchange is a strange choice for a modern greenfields project but hardly that noteworthy.
As far as I can tell, AES256-IGE is a made up mode used only by Telegram. That’s far from being a standard choice. I don’t know what authenticated encryption scheme they build on it, but on a very brief look, it doesn’t look authenticated at all.
See: https://mgp25.com/AESIGE/
See: https://mgp25.com/AESIGE/
> made up mode
It's was implemented in OpenSSL 15 years ago.
https://github.com/openssl/openssl/blob/master/crypto/aes/ae...
It's was implemented in OpenSSL 15 years ago.
https://github.com/openssl/openssl/blob/master/crypto/aes/ae...
AES256-IGE is a good choice since it disappeared from papers and suspected to be superior than other modes.
Papers are literally disappeared in first month of public Telegram release.
Source: Myself working at first months after public Telegram release on Android client.
Papers are literally disappeared in first month of public Telegram release.
Source: Myself working at first months after public Telegram release on Android client.
How is disappearance from papers a good thing? I found a patent (!):
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.
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.
[deleted]
Impressive work, but it leaves open the inevitable question of whether the software that is distributed actually implements the protocol as modelled in the proof. With reproducible builds and a trustworthy build environment, we can hopefully assume that the binary matches the source code, but there isn't yet a proof that the source code doesn't have some unmodelled edge cases (as in the 2017 Key Reinstallation AttaCKs[0] on WPA2).
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."
[0] https://www.krackattacks.com/
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."
[0] https://www.krackattacks.com/
The clients are all open source, so you can compile the code on your own machine.
Even if the clients are open source and if the verification of the protocol using ProVerif is sound, there is the possibility of a divergence between the "proof" and the implementation.
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.
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.
> Even if the clients are open source and if the verification of the protocol using ProVerif is sound, there is the possibility of a divergence between the "proof" and the implementation.
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.
See: https://core.telegram.org/reproducible-builds
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.
See: https://core.telegram.org/reproducible-builds
Threema offers reproducible builds as well, for the Android app: https://threema.ch/en/open-source/reproducible-builds
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.
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.
Can you really compile them?
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
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
It's not as if anyone even uses it. It's not even supported in the desktop clients.
Telegram's MAU is 400 mill last checked [0]. On the desktop, you just can't register, so you can't create an auth_key, but that doesn't mean you can't use the Telegram API over a TLS transport, and encrypt messages using the auth_key created on a phone.
[0]: https://www.businessofapps.com/data/telegram-statistics/
[0]: https://www.businessofapps.com/data/telegram-statistics/
I'm not saying Telegram doesn't have a lot of users, I'm saying that pretty much nobody uses the secret chat feature because it's not supported on all clients and even the clients that do support it can only do 1:1. So it's not very useful.
Telegram has more than 500 million active users already. https://t.me/durov/142
> It's not even supported in the desktop clients.
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.
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.
Really? This is the MacOS one version 2.5.1 right? I'm looking and I'm not seeing the option for creating a new secret chat.
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.
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.
Telegram for macOS is the one that's just called Telegram on the App Store. Current version is 7.3. The cross-platform Electron version of Telegram is called Telegram-lite on the App Store.
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.
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.
It's not hidden at all. On the left pane next to search there's a "New chat" button on both chat list and contact list, where you can select "New group", "New secret chat", "New Channel".
> 7.3 (211334) Stable
I installed it outside of the App Store.
I installed it outside of the App Store.
>the cross-desktop one is electron-based
I don't think so, the one I use on Linux uses Qt.
I don't think so, the one I use on Linux uses Qt.
Ah, I stand corrected. It used to be back then (very visible webkit process tree), long time since I moved to the Swift one.
Here's the various current app details: https://telegram.org/apps#source-code
Here's the various current app details: https://telegram.org/apps#source-code
well, kind of useless in practice, if the servers know the keys (except for unsynced 1:1...)
Broken crypto ("bunch of randoms have rolled their own crypto", to be precise [0]) is pretty much the only argument HN has against Telegram.
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...
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...
> Broken crypto ("bunch of randoms have rolled their own crypto", to be precise [0]) is pretty much the only argument HN has against Telegram.
Also that there's no crypto for every group chat and every default 1:1 chat.
Also that there's no crypto for every group chat and every default 1:1 chat.
The reasons given by them are reasonable. Whatsapp ain't e2ee since all chats are backed to google drive and iCloud.
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.
https://t.me/durovschat/527081
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.
https://t.me/durovschat/527081
It is such a shame that we have, in 2021, no way to perform secure computations in untrusted environment. Signal at least had the decency to try for Secure Value Recovery even if Intel SGX as a technology is not really mature.
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.
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.
> The reasons given by them are reasonable. Whatsapp ain't e2ee since all chats are backed to google drive and iCloud.
That's up to the user, I've never backed up my WA data to any cloud service.
That's up to the user, I've never backed up my WA data to any cloud service.
Do you make sure that in group chats no one there ever enables it by accident? Because it's really, really easy to inadvertently do.
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.
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.
> Do you make sure that in group chats no one there ever enables it by accident? Because it's really, really easy to inadvertently do.
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.
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.
Telegram is not a third party. It's the only party you trust. When you use whatsapp, you trust Whatsapp, Facebook and Google.
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.
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 trust Whatsapp, Facebook
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 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.
There is also not-metadata data that WhatsApp stores (group names, status updates, ...). But I think the point is that if you're using WhatsApp (especially group chats), there is a high chance that Facebook, Google AND Apple end up storing your personal data - even if Facebook might not have access to message contents (but Google and Apple still do). Still your data is all over the place. Doesn't matter if you disabled cloud backups because the people you chat with most likely didn't. With Telegram your data is stored on their servers - but but only on their servers.
> That's up to the user, I've never backed up my WA data to any cloud service.
You don't but almost every person you chat with backs it up.
You don't but almost every person you chat with backs it up.
None of my whatsapp chats are backed up to Google drive and iCloud, it’s optional.
Have you gone and disabled the backup options for every contact you chat with, in every personal and group chat?
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.
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.
Default 1:1 chat and group chat are secured by the server-client protocol. No e2e encryption by default is deliberate
https://telegram.org/faq#q-why-not-just-make-all-chats-39sec...
https://telegram.org/faq#q-why-not-just-make-all-chats-39sec...
Well, anyone releasing a serious communication app in the last 11 years that didn't do at least that should have been flogged...
I disagree with this. A point the FAQ didn't mention is user psychology.
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.
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'd argue that no-one having access to my messages should be the default case. The fact that a government could potentially get access to all unencrypted telegram messages sent by everyone is pretty off-putting. If they want my signal messages they would have to hack my phone, or MITM me and face potential discovery since verification status is unknown to the server. And that would only get them access to messages sent from thereon.
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.
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.
A lot of users just think that Telegram is E2EE by default. I really don't see why a user would make a conscious choice to activate E2EE on Telegram but not verify the fingerprints on Signal. In both cases a manual step is involved.
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.
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.
There sure are many technical reasons to not have e2ee by default.
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.
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.
Yes... just like this message I'm typing into hacker news right now is client-server encrypted. Having any trouble reading it?
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.
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.
Then you may be very disappointed to learn that most of the Internet, I'd wager >90% of it, is, in fact, unencrypted by your definition.
So you can be 100% sure Russia gets a copy of every message you send.
They have been banned for not giving the messages to Russia. How can be be so confident that Russia gets copies of the messages.
https://en.wikipedia.org/wiki/Blocking_Telegram_in_Russia
Please don't post such accusations without sources.
https://en.wikipedia.org/wiki/Blocking_Telegram_in_Russia
Please don't post such accusations without sources.
The bounty isn't as much of an assurance as they would have you believe. Good publicity nonetheless.
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.
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.
I think this exact comment sequence with these exact links has been played out on every Hacker News thread about Telegram since its inception.
Yeah I know it's just publicity. Just like 'Apple will pay 1 million dollars for iphone hack' articles.
But Moxie (or any other cryptographer) could use the money for Signal's development. It's a large amount.
But Moxie (or any other cryptographer) could use the money for Signal's development. It's a large amount.
Moxie clearly states that: the competition is framed in such a way that it would be bordering impossible to break it even uf it had been using primitives known to be broken.
Durov (Telegram CEO) responded to some questions regarding this: https://t.me/durov/146
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