Where is HChaCha20 formally defined?

Question

I stumbled upon the Q&A “Advantages of HS1-SIV over ChaCha20-Poly1305-SIV?” which mentions “HChaCha20” in the question.

Trying to look it up via the usual research sources, I failed to find an according paper handling HChaCha20. The only places where it seems to be mentioned and implemented are some github projects (like libsodium – but the libsodium docs likewise fail mentioning a paper of alike reference) and some back-and-forth discussions at twitter (which also fail to point to any paper).

Since even some well-known and respected security libs like libsodium know about HChaCha20 and implemented it, I just have to ask: Where is HChaCha20 formally defined?

Note that I'm asking if any paper exist which formally handles the definition, description, and security analysis of HChaCha20 and where I might find it. I'm not interested in related implementations and/or explanations describing how it practically works. I can read the sourcecode, but I'ld like to check the according paper that should exist as a base for those HChaCha20 implementations. After all, verification and validation requires a formal basis.

If such a paper does not exist, can we even assume HChaCha20 and related implementations to be cryptographically secure? If, on what basis? How and where has that basis' cryptographic security formally been analyzed and verified? Or is HChaCha20 bluntly relying on the ChaCha20 core to be secure, without taking another look at the HChaCha20 specifics that differ from ChaCha20's security assumptions? If the later is the case, can we really assume HChaCha20 to be secure? After all, that would mean there isn't a formal analysis & verification of such claims.

Answer 1

Doing further research accross multiple scientific portals and cryptography-related forums, it turns out that no formal specification exists… at all.

HChaCha20 can be constructed exactly the same way as HSalsa20, but has not really been specified or analysed to the full extend we usually expect cryptographic designs to be specified and analysed.

In this relation, it seems to make sense to also quote what CodesInChaos commented:

I don't think such a spec exists. For the security, you can just directly transfer the "if Salsa20 is secure so is HSalsa20" proof to "if ChaCha is secure, so is HChaCha". Related: Can I use the ChaCha core as a 256-bit to 256-bit one-way function?

The same conclusion can be drawn from postings to the Cfrg mailing list (example):

…
The proof for XSalsa20/HSalsa20 should work for XChaCha20/HChaCha20 too afaics. (http://cr.yp.to/snuffle/xsalsa-20110204.pdf on http://cr.yp.to/snuffle.html)
…