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.