Re: [Cfrg] Review of (security of) remaining candidates

["Stanislav V. Smyshlyaev" <[e-mail]>]

Thanks a lot, Julia!

Regards,
Stanislav

пт, 6 марта 2020 г. в 23:36, Julia Hesse <[e-mail]>om>:

> Apologies for the lengthy and late review. I looked at security aspects
> of the four remaining candidates, and the recommendations are not taking
> other properties such as efficiency or integration into standards into
> account.
>
> To summarize, security-wise I (conditionally) recommend SPAKE2 and OPAQUE.
>
> SPAKE2
> ======
> I reviewed the following documents: the candidate's specification as
> described in draft-irtf-cfrg-spake2-09, and proofs of (what they call)
> SPAKE2 in https://www.di.ens.fr/~mabdalla/papers/AbPo05a-letter.pdf
> (passive and MITM security) and https://eprint.iacr.org/2019/1194
> (adaptive corruption and forward secrecy).
>
> Security pro's and con's:
> + Existing security proofs require one programmable global RO and Gap-DH
> (needed for forward secrecy, passive/mitm proof requires CDH instead of
> Gap-DH)
> + SPAKE2 has forward secrecy
> + None of the proofs require key confirmation (draft-irtf-cfrg-spake2-09
> puts it as MUST = absolute requirement)
> + Security proofs cover multi-party & multi-session setting (including
> re-use of passwords)
> + Security proofs are tight (i.e., guarantees do not degrade with the
> number of users)
> + Security proof for passive/MITM security was published already in 2005
> and since today no issues have been found (see also notes on Scott's
> review below)
> - Security proofs cover only executions where users use passwords chosen
> uniformly random from the dictionary
> - draft-irtf-cfrg-spake2-09 adds a cofactor h to the protocol, but no
> security analysis exists for that
> - No quantum preparedness, no option to switch to it, limited crypto
> agility since not a modular protocol
> - No quantum annoyance if M,N generated system-wide
>
> Notes on SPAKE2's reliance on parameters M,N (both group elements):
> If the dlog of M or N is known, then SPAKE2 is offline attackable
> (meaning that attacking only one run of the protocol allows the attacker
> to later test arbitrarily many passwords). However, the protocol's
> security does not rely on M != N
>
> Notes regarding other reviews:
> Scott Fluhrer mentions an issue in the proof of passive and MITM
> security, which to me is not a concern. Namely, he indicates that there
> exists a distinguisher between Ext2 and Ext3. In this game hop, random
> self-reducibility of CDH is exploited to plant a CDH problem instance
> into hashed outputs of participants, such that any hash query of a
> distinguisher would contain a CDH solution. Scott's concern is that
> parts of the CDH problem instances could be adversarially generated (and
> thus self-reducibility does not help in replacing MITM-attacked
> instances). However, Ext3 only replaces outputs of sessions that are
> *not* attacked by a MITM (indicated by "for all sessions generated via
> an Execute oracle query"). Instead, those sessions are handled only in
> Ext4 where the analysis correctly concludes that the attacker can only
> distinguish replacement of the RO in case he guesses the correct
> password. Therefor I don't see any issue with the proof.
>
> Comments:
> Both security proofs seem sound to me. If possible,
> draft-irtf-cfrg-spake2-09 should demand a gap-DH group instead of a CDH
> group such that SPAKE2 is guaranteed to achieve forward secrecy. Since
> all variants discussed on the list of generating M,N will leave the
> proofs valid, security-wise the only concern is that system-wide M,N
> would hinder quantum annoyance, which seems already well-known to
> everybody.
> Clearly, a strong point in favor of SPAKE2 is that proofs show that only
> one RO suffices to obtain strong guarantees.
> My main concern is that the protocol in the RFC is not the one analyzed
> in the papers. Some modifications seem to add to its security (e.g.,
> using w=MHF(pw) mod p instead of pw partly mitigates the fact that
> security is only analysed wrt randomly distributed passwords), but for
> others it is less clear (e.g., usage of cofactor h, cf also Karthik's
> review) and more analysis needs to be carried out. I am also slightly
> worried that the authors of draft-irtf-cfrg-spake2-09 say that key
> confirmation is mandatory while security analysis clearly shows that it
> is not necessary. I am not an expert in implementing crypto protocols,
> but to me it seems desireable to state SPAKE2 without key confirmation
> and leave it up to the application protocol if/how key confirmation is
> implemented.
>
> CPace
> =====
> I reviewed the updated security analysis
>
> https://github.com/BjoernMHaase/AuCPace/blob/master/aucpace_security_analysis_20200208.pdf
> and the specification https://tools.ietf.org/html/draft-haase-cpace-01.
> For details on how to implement Map2Point I looked at the most recent
> version of the original CPace publication at
> https://eprint.iacr.org/2018/286.
>
> Security pro's and con's:
> + Strong security notion with adversarially-chosen passwords,
> composability, adaptive corruptions and forward secrecy
> + Security properties do not rely on key confirmation
> + CPace is quantum annoying
> + Security proof covers multi-party & multi-session setting (including
> re-use of passwords)
> - Security proof does not analyze distinguishing advantage, thus I also
> cannot say whether the proof is tight
> - Trusted setup required for Map2Point
> - Heavy use of random oracles (2, both are programmed)
> - Proof posted only in 2019 with several issues already discovered (and
> probably containing more, see below)
> - No quantum preparedness, no option to switch to it, limited crypto
> agility since not a modular protocol
>
> Note on sid handling:
> As clarified by Ran Canetti, the sid can be chosen by the initiator and
> transmitted to the responder. Security-wise let me note that the sid
> does *not* have to be randomly distributed, and it does *not* have to be
> kept secret. It only has to be unique system-wide (e.g., contains a
> nonce or counter and some addressing information of both initiator and
> responder, which needs to be unique anyway to correctly route the
> message). CPace is thus a 1-round protocol assuming that the application
> protocols allows transmitting the sid along with the initiator's first
> message.
>
> Comments:
> Even though the author(s) continuously improve the security analysis of
> CPace, I am still not able to follow. One reason is that it is a
> simulation-based proof without any formal indistinguishability
> arguments. Another reason is that, while the proof is written as a
> sequence of games, most non-trivial changes happen in the step Exp2 to
> Exp3. In this step it is shown how to simulate a CPace execution without
> knowledge of passwords. However, all possible corruption scenarios
> (corrupted initiator, corrupted sender, and different times where these
> corruptions can each happen) are handled simultaneously, resulting in so
> many different cases that, at least to me, it is impossible to say
> whether the simulation is complete.
> While the security definition in the UC framework originates from a
> paper of 2005 by Canetti et al, it had to be adapted to allow for proofs
> of implicit authenticated CPace. On the plus side, adaptation has been
> done in coordination with, among others, authors of OPAQUE who face the
> same problem since they use also the UC framework. However, it still
> seems to me that the changes made are not sufficient for CPace to
> realize the current version, called F_ipwKE. An attacker leaving both
> parties uncorrupted but injecting a self-chosen Y_b will observe the
> hashed output of the initiator (obtained from F_ipwKE, oblivious to the
> simulator). If he then afterwards queries the random oracle on the
> shared secret Y_a^y_b, the simulator can use the newly introduced
> DelayedTestPwd query to learn whether the attacker and the initiator
> used the same password. However, to program the random oracle H_2
> according to this answer, the simulator needs to learn the output given
> towards the honest initiator. This is not possible with F_ipwKE.
> This might seem nit-picky, and indeed I do not have any doubts that
> CPace UC-emulates a slightly revised but not crucially weakened version
> of F_ipwKE. However, the proof relies on heavy tools: two programmable
> random oracles and several properties of Map2Point (efficiently
> invertible such that dlogs of images can be chosen by the simulator
> etc.) which additionally require availability of a shared trusted setup
> among all protocol participants (called CRS in the paper). Let me stress
> that a UC secure balanced (!) PAKE protocol can be obtained *without*
> any idealized assumptions, although such a protocol would be less
> efficient than CPace. Still, the question remains what the current proof
> is worth: due to the heavy usage of idealized assumptions it is only a
> rudimentary sanity check of the protocol and it does not rule out a very
> large class of attacks exploiting properties of instantiations of any of
> the idealized building blocks.
>
> Recommendation balanced PAKE
> ============================
> While the proven guarantees for SPAKE2 are a bit weaker than for CPace,
> I do believe that they are sufficient for a widely deployed SPAKE2 not
> to have any serious security issues. For CPace, I unfortunately cannot
> state the same. Upon deployment and instantiation of Map2Point and the
> programmable random oracles, there are just too many things which could
> go wrong due to the strong/idealized assumptions on all of these
> components. In that sense, the analyzed protocol is too far away from
> what will be actually deployed. Security-wise I thus recommend SPAKE2,
> conditioned on a thorough analysis on usage of cofactors.
>
> AuCPace
> =======
> I reviewed the updated security analysis in
>
> https://github.com/BjoernMHaase/AuCPace/blob/master/aucpace_security_analysis_20200208.pdf
> .
>
> Security pro's and con's:
> + Strong security notion with adversarially-chosen passwords,
> composability, adaptive corruptions and forward secrecy
> + Security properties do not rely on key confirmation
> + Modular: AuCPace can be instantiated with any (implicit) UC-secure
> balanced PAKE
> + Minimal usage of idealized assumptions (1 programmable RO)
> - Proof not convincing without further analysis
>
> Comments:
> After thoroughly checking the proof of the implicit (not strongly
> secure) AuCPace I am unfortunately not convinced that AuCPace can be
> proven UC secure (i.e., to emulate F_aipwKE as stated in the paper).
> While the authors give a simulator for AuCPace, they do not give any
> arguments why this simulation is sufficient. Such arguments should be
> intelligible from the sequence of games they provide. Below is an
> incomplete list of issues with this sequence.
> * The first game is the real execution without F_aipwKE, and none of the
> games introduce (any part of) this ITI. But then, the last game suddenly
> contains F_aipwKE.
> * Games G_2,G_3(1),G_3(2) do not say how to formally change the
> execution, nor do they contain formal reductions to, e.g., CDH.
> * Game G_4 contains no indistinguishability arguments despite the fact
> that almost all changes happen from G_3(2) to G_4
> * The newly introduced interfaces are analyzed only rudimentary: G_4
> lets the simulator relay Interrupt and DelayedTestPwd queries towards
> F_ipwKE to F_aipwKE. According to the text, this should work because the
> interfaces in both functionalities are equal. However, whether F_aipwKE
> gives an answer that can be used to simulate F_ipwKE depends on the
> *values* set in the functionalities. To say the least, one has to prove
> that dPT=1 in F_aipwKE whenever dPT=1 in F_ipwKE.
>
> OPAQUE
> ======
> I reviewed the security analysis in https://eprint.iacr.org/2018/163.pdf
> (rev of Oct 22) and the specification in
> https://tools.ietf.org/html/draft-krawczyk-cfrg-opaque-03.
>
> Security pro's and con's:
> + Strong security notion with adversarially-chosen passwords,
> composability, adaptive corruptions and forward secrecy
> + Security properties do not rely on key confirmation
> + Modular, good crypto agility
> + Security proof covers multi-party & multi-session setting (including
> re-use of passwords)
> + No idealized assumptions outside of building blocks required
> - No quantum preparedness and not quantum annoying
>
> Comments:
> OPAQUE's security proof is wrt the same strong model as AuCPace. OPAQUE
> is modular, using KCI-secure AKE and an OPRF as building blocks. OPAQUE
> is nowhere close to quantum prepared since it is a long way towards a
> quantum-safe OPRF that is efficient enough. The protocol comes with an
> impressive security analysis that does not leave a lot of wiggle room.
> Obvious downsides are the complexity of the current proof (~20 pages in
> the OPAQUE paper, plus one has to assemble the HMQV security proof from
> few other papers) and the fact that it is relatively new and thus
> presumably not checked by many people.
> I checked the (evolving) proof of OPAQUE already few times, and with the
> current version I find only one issue I could not (trivially) solve
> myself: the non-modular way in which HMQV is used. Namely, HMQV's
> security proof is wrt a protocol-internal key generation algorithm
> setting up a key pair for each user. When using HMQV modularly, those
> keys would never "leave" honest parties. However, in OPAQUE the keys are
> generated and used outside HMQV (they form the password file and are
> send, encrypted with the OPRFed password, from the server to the user).
> Still, the OPAQUE proof uses the HMQV simulator as a sub-algorithm. I am
> not convinced that this simulator can be run on externally-chosen keys.
> For example, in an honest execution the saPAKE adversary can, after a
> successful key exchange, try a late password guess by decrypting any
> ciphertext sent by the server. The adversary then learns the HMQV keys
> *without corrupting any party* and can compute the shared HMQV secret of
> those parties. It seems to me that this is not simulatable by the saPAKE
> simulator without learning the session key generated by honest protocol
> participants. (Note: this is a similar issue as described for CPace above.)
>
> Recommendation augmented PAKE
> =============================
> Both proofs come with similar pro's. The conducted analysis of OPAQUE is
> clearly superior to the one of AuCPace. Conditioned on me being wrong
> about the issue with HMQV's keys, or the authors being able to fix it, I
> thus recommend OPAQUE.
>
> _______________________________________________
> Cfrg mailing list
> [e-mail]
> https://www.irtf.org/mailman/listinfo/cfrg
>