1. 25
    A Formal Security Analysis of the Signal Messaging Protocol ☶ pdf formalmethods security eprint.iacr.org
    pushcx avatar via pushcx 3 months ago | cached | no comments

Updated from the previous post on Lobsters:

V2.0 (2017-10-09) Major updates.

  • Added simplified protocol flow diagram to aid intuition.
  • Clarified and further explained the freshness predicates.
  • Clarified and further explained how our model relates to key indistinguishability and ACCE-like definitions.
  • Made substantial clarifications and expansions to the proof.
  • Added illustrative figures to the proof.
  • Wrote Section C on the use of the PRF-ODH assumption to replace GapDH + ROM.

  1.