Formal Analysis of the Signal Protocol using the Scyther Tool

Signal is a popular cryptographic protocol designed by the Open Whisper System that delivers end-to-end encryption for instant messaging (IM) conversations. Furthermore, Signal is considered the core security protocol for numerous applications such as Facebook Messenger and the Google Allo application. The increased use of the signal protocol in different IM applications has made it imperative, which also makes it highly attractive for the intruders. Therefore, security analysis for the signal protocol is deemed necessary to ensure its capability in the security domain. This paper conducts a formal analysis of the security protocol using Scyther, which is a model checking tool that has been used in analysis of different protocols. In this work, the signal protocol is analyzed in three phases: registration phase, sending and receiving message phase, and sending a reply phase. The obtained results are addressed and compared with those from mathematical and other model checking approaches.