Some notes on recent Signal Protocol analysis paper

[jbenet]

I'm reading through A Formal Security Analysis of the Signal Messaging Protocol https://eprint.iacr.org/2016/1013.pdf. I'll be taking some notes here relating to:

• security considerations in applications of the signal protocol
• security and thread model considerations for distributing/decentralizing the key server (i.e. how to do this without honest key servers)
• considerations for implementations in other programming contexts (signal.js ?)
• considerations for CRDTs / orbit-db

please feel free to jot down your own notes here or discuss as needed. my goal is to get to some version of Signal that can work well with ipfs distribution models.

[jbenet]

I should clarify that the goal is to talk about the Signal protocol, not just this particular analysis, but this particular analysis was published recently and offers a nice formal language. we should be careful not to mistake the protocol in this paper for the real protocol, as im sure some differences exist (or will exist).

[jbenet]

Some quickly jotted down notes. (DISCLAIMER: these are quick observations and probably wrong.)

• Relevant HN discussion: https://news.ycombinator.com/item?id=12899398 -- mostly discussion on the product, not the paper/protocol.
• Relevant Reddit discussion: https://www.reddit.com/r/netsec/comments/59rf92/a_formal_security_analysis_of_the_signal/ (includes authors, but very few comments).

(abstract) We then prove the security of Signal’s core in our model, demonstrating several standard security properties. We have found no major flaws in the design

Yay!

(Figure 2, pg 7)

Useful protocol exchange diagram. But notation is dense and sub-optimal. I think tweaking the notation, more abstraction/more greek, or another pass at it could seriously improve presentation and understandability.

I wonder what Signal team thinks about this diagram, and the paper as a whole. TODO: figure it out / ask them.

(S6) Out-of-band key verification .... We simply assume that long-term and medium-term public key distribution is honest, and do not analyse the out-of-band verification channel.

Hmmm. seems like a big assumption. We should endeavor to understand the model better there and what advantages an adversarial key server could exploit. This will help design a byzantine-tolerant distributed key server.

I would like to get to "as long as there is a byzantine-tolerant broadcast channel for keys, everything works", because then all we need is byzantine agreement (eg a blockchain, stellar, something stamped to a blockchain, etc).

Further questions here-- what historical data can a malicious key server store? I was impressed by the signal announcements here: https://whispersystems.org/bigbrother/eastern-virginia-grand-jury/ -- in particular the tiny attachment. but that seems like that showed less than what everything the server actually has, server should have some the public keys too (identity key, medium term keys, etc). More Qs: what about message ciphertexts? are they only exchanged p2p synchronously? i thought it supported async distribution?

Some of these questions seem to be answered in https://whispersystems.org/blog/asynchronous-security/

(The TextSecure Protocol) Package up the prekey id, the locally generated key exchange message, and the ciphertext. .... Send it all in one bundle to the destination client. ... The user experience for the sender is ideal: they type a message, hit send, and an encrypted message is immediately sent. .... The destination client receives all of this as a single push notification.

So assuming this is still the case for Signal, this means the ciphertext moves in the push notification. May or may not be in Signal's servers, but definitely the push notification server (apple, etc). This does seem to leak more messaging metadata (message times, maybe lengths or rough lengths (order of magnitude)) than i thought previously. Still secure (forward secrecy; OTR-style), but adversary can collect the metadata. (this is good news for a distributed version, as it lowers the bar to achieve the same guarantees, though less private than other, mixer style protocols).

(S6) Application Variants ... WhatsApp implements a re-transmission mechanism: if Bob appears to change his identity key, clients will resend messages encrypted under the new value. Hence, an adversary with control over identity registration can disconnect Bob and replace his key, and Alice will re-send the message to the adversary.

That seems very concerning. Is this right? or did the paper get this wrong? If it's right, what exactly is the threat model here? IIUC, this claim is that WhatsApp could MITM the communication with minimal to no warning (what does the "retransmission mechanism" look like for the user? what's the UX?). Maybe not without being detected (rolling the key may produce a warning for the user, but a warning without total halting or a BRS may not go heeded by most average consumer users.).

[jbenet]

cc

• @lgierth @Kubuxu @cpacia @hoffmabc i know you're interested
• @zooko @warner @christianlundkvist in case you're interested

[Kubuxu]

In case of android I read that GCM servers (push) are only used to notify Signal to fetch the message, so it is Push for wake-up and pull for the encrypted message.

[haadcode]

Subscribing myself to this threat.

[cpacia]

So I'd really like to use the signal protocol for OpenBazaar offline messaging. There is even a Go implementation. But the problem I have is it seems to be designed entirely for a client server model, not p2p.

For example, users upload pre-keys to a server which vends them to other parties on request and keeps track of which ones have been issued. The pre-keys are then used to start the ratchet protocol.

Does anyone have an idea how to make this work? We could obviously seed a list of pre-keys on IPFS, but then there's a chance a sender will pick one that had been used before. (obviously an initial handshake is one way around it, but that prevents sending messages where both parties haven't yet done a handshake).

[cpacia]

Also, I'm trying my best to keep the metadata leakage to a minimum, and I think the signal protocol has the sender and recipient IDs attached to each message. The server is trusted to keep the metadata secure (I think). Again, adapting that to a p2p environment is challenging.

[haadcode]

Here's something I read recently that may or may not help to understand how Signal works http://www.alexkyte.me/2016/10/how-textsecure-protocol-signal-whatsapp.html.

[jbenet]

@haadcode whoops i meant to cc you too but somehow failed.

@cpacia yeah-- i'm trying to explore how to adapt the schemes to something totally distributed. There's something here, but will take some time to figure out in full. let's keep exploring :)

[kelnage]

On the WhatsApp retransmission vulnerability - this was reported earlier this year (see https://tobi.rocks/2016/04/whats-app-retransmission-vulnerability/). WhatsApp just responded that it is a threat model they don't protect against.

[RichardLitt]

Subscribing.

[coder5876]

Moxie & Trevor just published double ratchet spec:

https://whispersystems.org/docs/specifications/doubleratchet/

[coder5876]

Also X3DH key agreement:
https://whispersystems.org/docs/specifications/x3dh/

Signature schemes:
https://whispersystems.org/docs/specifications/xeddsa

[jbenet]

Thanks for posting these links @christianlundkvist !

Hopefully they will publish exactly what gets stored on third-party servers and for how long it's (intended) to be there. I may email and ask.

Reading this, and re-reading the OTR paper, i'm curious how they do groups.

• (1) the double ratchet makes heavy use of DHE exchanges for 1-1 shared secrets (input to the KDF), and derives 2 keys (sending and receiving) in 2 ratchet steps. At first pass, it seems difficult to adapt this to the group model, if we want to preserve the nice properties of the double ratchet (forward secrecy, future secrecy, OTR-like authentication, OTR-like repudiation), and not do full pairwise ratchets with everyone, or some clunky sync round protocol.

• (2) I found this: https://matrix.org/docs/spec/megolm.html i think it does not provide future secrecy (compromising the ephemeral keys at one point is not healed later with future ratchet steps). And am not sure about proper repudiation (anyone can forge, as in Signal). I'm also not sure what the whole big cyclical seeding is all about yet

• (3) it looks like OpenWhisperSystems did pairwise ratchets -- https://whispersystems.org/blog/private-groups/ -- cleverly they propose sending shared keys for long messages / media (circumventing the n^2 problem). the end discusses keeping the UI linearized (not threaded) despite arrival of messages being unordered and potentially confusing. (unordered at least in existence-- when they arrive, i believe they can be ordered). I do think showing the "threaded-ness" is useful, particularly when it's not clear that everyone has seen everything, or rather unclear who has seen what. (I laughed at the president-icecream example at the end).

• (4) all this makes me think that there are interesting UI challenges in showing (a) the arrival of encrypted messages and their decryption keys, (b) any messages sent on messages still waiting to show up (the "threadedness" can be used to show previous placeholders for messages that have not arrived), or generally (c) participants synchronizing conversations threaded in time (which is already a problem (interesting UI challenge) for Orbit). --- i think there's something to be used here, threadedness can be "linearized" by showing "receipt of previously unknown past messages" now, not interleaved where they belong in the timeline. (think: each participant sees their merge history -- not a linear, simultaneous conversation -- which is a simplifying fiction anyway). --- color (or other visual elements) could be used to signal transitions, or "mix-points", when a batch of past messages from participants not heard recently arrive.

• (5) the good news is this is well trodden ground and we have a way forward. "do what signal does", or rather "something close to it that doesn't break the security properties and works for CRDT style messaging.

[jbenet]

I'll dig deeper into Matrix's megolm. This post is promising https://matrix.org/blog/2016/11/21/matrixs-olm-end-to-end-encryption-security-assessment-released-and-implemented-cross-platform-on-riot-at-last/ and the security review is here: https://www.nccgroup.trust/globalassets/our-research/us/public-reports/2016/november/ncc_group_olm_cryptogrpahic_review_2016_11_01pdf (from NCC Group). If this works for our use case (which seems very close to Matrix's) -- then this is great (available library, just audited, wow this comes in good time!). I'll be curious to hear what Moxie, Trevor, @zooko, and @warner think of it, too.