A formal analysis of the signal messaging protocol
Signal is a new security protocol that provides end-to-end encryption for instant messaging. It has recently been adopted by WhatsApp, Facebook Messenger and Google Allo among many others; the first two of these have at least 1 billion active users. Signal includes several uncommon security propert...
| Main Authors: | , , , , |
|---|---|
| Format: | Conference item |
| Published: |
IEEE
2017
|
| _version_ | 1826291996344451072 |
|---|---|
| author | Cohn-Gordon, K Cremers, C Dowling, B Garratt, L Stebila, D |
| author_facet | Cohn-Gordon, K Cremers, C Dowling, B Garratt, L Stebila, D |
| author_sort | Cohn-Gordon, K |
| collection | OXFORD |
| description | Signal is a new security protocol that provides end-to-end encryption for instant messaging. It has recently been adopted by WhatsApp, Facebook Messenger and Google Allo among many others; the first two of these have at least 1 billion active users. Signal includes several uncommon security properties (such as "future secrecy" or "post-compromise security"), enabled by a novel technique called *ratcheting* in which session keys are updated with every message sent. Despite its importance and novelty, there has been little to no academic analysis of the Signal protocol. We conduct the first security analysis of Signal's Key Agreement and Double Ratchet as a multi-stage key exchange protocol. We extract from the implementation a formal description of the abstract protocol, define a security model which can capture the "ratcheting" key update structure, and prove the security of Signal's core in our model. Our presentation and results can serve as a starting point for other analyses of this widely adopted protocol. |
| first_indexed | 2024-03-07T03:07:54Z |
| format | Conference item |
| id | oxford-uuid:b32f4e17-ceae-4c53-a54c-edeca815d827 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T03:07:54Z |
| publishDate | 2017 |
| publisher | IEEE |
| record_format | dspace |
| spelling | oxford-uuid:b32f4e17-ceae-4c53-a54c-edeca815d8272022-03-27T04:17:11ZA formal analysis of the signal messaging protocolConference itemhttp://purl.org/coar/resource_type/c_5794uuid:b32f4e17-ceae-4c53-a54c-edeca815d827Symplectic Elements at OxfordIEEE2017Cohn-Gordon, KCremers, CDowling, BGarratt, LStebila, DSignal is a new security protocol that provides end-to-end encryption for instant messaging. It has recently been adopted by WhatsApp, Facebook Messenger and Google Allo among many others; the first two of these have at least 1 billion active users. Signal includes several uncommon security properties (such as "future secrecy" or "post-compromise security"), enabled by a novel technique called *ratcheting* in which session keys are updated with every message sent. Despite its importance and novelty, there has been little to no academic analysis of the Signal protocol. We conduct the first security analysis of Signal's Key Agreement and Double Ratchet as a multi-stage key exchange protocol. We extract from the implementation a formal description of the abstract protocol, define a security model which can capture the "ratcheting" key update structure, and prove the security of Signal's core in our model. Our presentation and results can serve as a starting point for other analyses of this widely adopted protocol. |
| spellingShingle | Cohn-Gordon, K Cremers, C Dowling, B Garratt, L Stebila, D A formal analysis of the signal messaging protocol |
| title | A formal analysis of the signal messaging protocol |
| title_full | A formal analysis of the signal messaging protocol |
| title_fullStr | A formal analysis of the signal messaging protocol |
| title_full_unstemmed | A formal analysis of the signal messaging protocol |
| title_short | A formal analysis of the signal messaging protocol |
| title_sort | formal analysis of the signal messaging protocol |
| work_keys_str_mv | AT cohngordonk aformalanalysisofthesignalmessagingprotocol AT cremersc aformalanalysisofthesignalmessagingprotocol AT dowlingb aformalanalysisofthesignalmessagingprotocol AT garrattl aformalanalysisofthesignalmessagingprotocol AT stebilad aformalanalysisofthesignalmessagingprotocol AT cohngordonk formalanalysisofthesignalmessagingprotocol AT cremersc formalanalysisofthesignalmessagingprotocol AT dowlingb formalanalysisofthesignalmessagingprotocol AT garrattl formalanalysisofthesignalmessagingprotocol AT stebilad formalanalysisofthesignalmessagingprotocol |