[Cfrg] Proof of SPAKE2 is sound?

Watson Ladd <watsonbladd@gmail.com> Mon, 09 September 2019 00:34 UTC

MIME-Version: 1.0
From: Watson Ladd <watsonbladd@gmail.com>
Date: Sun, 08 Sep 2019 17:33:56 -0700
Message-ID: <CACsn0cmFmX5VFer5-YMbBsPzyyYG12KzMDwYR7m38uHOb_AORA@mail.gmail.com>
To: cfrg@ietf.org
Content-Type: text/plain; charset="UTF-8"
Archived-At: <https://mailarchive.ietf.org/arch/msg/cfrg/jBUSpq9xOOyOuwVUhd5E55_89TU>
Subject: [Cfrg] Proof of SPAKE2 is sound?
Precedence: list

Dear all,

I've spent the weekend looking at the paper and examining Scott
Fluhrer's claimed flaw. My conclusion is that the paper is sound and
Scott's claimed attacks result from a misreading of the security
claim.

Scott claims the theorem is invalid and one error is in the transition
from Experiment 2 to Experiment 3. However, the only change is in a
query for sessions that haven't been tampered with: there is no
problem with the switch.

Offline he claimed Theorem 8 was wrong because it didn't accommodate
an attacker who knows a discrete log of M or N. I disagree: that's
what the s-pccdh Advantage term captures/ the entire proof is based on
extracting a discrete log from an attacker who breaks the protocol.

It's entirely possible that I'm misrecalling the objection and would
appreciate clarification/more eyes on the paper.

Sincerely,
Watson Ladd

[Cfrg] Proof of SPAKE2 is sound? Watson Ladd