Hi, I perform research in the area of PAKEs. I'm not a "foremost expert" but I know a bit. Before I start, I don't believe that it's standard to use the term "doubly augmented PAKEs". Instead, I'll use the more accepted shorthand "saPAKE" for "strong asymmetric PAKE". I think it's important to note that the provided saPAKE Double BS-SPEKE does not come with a security proof. A proof of a similar protocol is not hard…
I mixed up "b" stored by the server in the registration phase and the "b" used in the online phase. In that case, the adversary can't compute either b * C or c * B (by probably just CDH).
This being said, there's a more technical problem with the protocol as-is with how the OPRF is used. Currently, the adversary can malleate the OPRF messages resulting in a valid/invalid session between two honest parties without the simulator being able to distinguish between the two cases. This comes from the perfect blinding property of 2hDH and is discussed in the OPAQUE paper[1].
There may be other problems, but _most_ of the protocol passes a quick smell test.
Sorry for any confusion!
-- EDIT --
I'm not really surprised that this problem came out as the JKX compiler is quite nuanced (more so than the paper immediately lets on). So I definitely suggest walking through the proof before applying this protocol anywhere; however, the current protocol seems like a good jumping off point. I think there also needs to be a clear reason to use a SPEKE derivative as the aPAKE building block.