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.