Many secure end-to-end messaging protocols exist in the wild, most of which claim to provide the same basic security properties. However, each protocol exists in a different context and has different requirements to fulfill. The protocol and the security that is achieved is not independent of that context. In particular we take a look at the Silent Circle instant messaging protocol (SCIMP), the former default messaging protocol on the BlackPhone. We construct a model of the protocol using the formal verifier ProVerif, with which we prove that version one of the protocol is secure, and we find a man-in-the-middle attack against version two. By comparing the model against the actual implementation we find a discrepancy that allows an attacker to perform the attack completely undetected. A similar situation arises in OMEMO (an multi-device XMPP implementation of the Signal protocol), which did not achieve the full potential security when deployed in a multi-device setting. Both protocols have been patched and should no longer be vulnerable against the found attacks.
Sebastian Verschoor got his Masters degree in Information Security Technology at the Eindhoven University of Technology. In his thesis, supervised by Dan Bernstein and Tanja Lange, he analyzed the Silent Circle instant messaging protocol. While working at Radically Open Security, he audited the proposed OMEMO protocol, the patched version of which is currently being considered for standardization. He is currently a PhD student at the Institute for Quantum Computing at the University of Waterloo.