Formal Information-Theoretic Key Expansion Definition Is there a formal definition for a protocol that expands keys that are pre-shared among 2 or more parties?
How about an informal definition?

Example:

Alice and Bob pre-share a $n$-bit string $k$.  After running algorithm $\Pi$ Alice and Bob have a common ($n$+$q$)-bit string $k'$, where $q&gt;0$.  In addition Eve learns nothing about $k$ or $k'$. Eve is an an eavesdropper on the channel between Alice and Bob with unlimited computational power.  i.e. If $P_x$ are the odds of Eve learning $x$ then $P_k\le \frac{1}{2^n}$ and  $P_{k'}\le \frac{1}{2^{n}}$.
NIST SP-800 108 seems to have a semi-formal definition in chapter 5.0:

Section 1:


  A key derivation function iterates a pseudorandom function (ed: PRF) $n$ times and concatenates the outputs until $L$ bits of keying material are generated, where $n = ⎡L/h⎤$.


Section 2:


  For each of the iterations of the PRF, the key derivation key $K_I$ is used as the key, and the input data consists of an iteration variable and a string of fixed input data.


But I must admit that this seems more a description of the inner workings of the described KDF's than a formal definition of one, if such a thing exists.

As about any KDF actually works this way it remains to be seen if this isn't enough of a formal description.



The original HKDF paper has this more formal definition:


  Definition 5: A key derivation function (KDF) accepts as input four arguments:  
  
  
  a value $\sigma$ sampled from a source of keying material (Def. 6),
  a length value $l$,
  
  
  and two additional arguments,
  
  
  a salt
  value $r$ defined over a set of possible salt values
  and a context variable $c$,
  
  
  both of which are optional, i.e., can be set to the null string or to a constant. The KDF output is a string of $l$ bits.