They could have made something like: the client generates a key pair,
  encrypts the public key with the server’s public key, sends it to the server
  with a nonce, and the server sends back the nonce encrypted with the
  client’s public key. Simple and easy.

Just out of curiosity, is it really that easy if you're using verified components? I would naively assume (and hope) so, but then everyone tells me that crypto is fraught with subtle ways to shoot your users in the feet, including if you misuse verified primitives. If yes, I'll continue making pie-in-the-sky plans using the magic of public-key cryptography. :)