What is a Key Derivation Function? From Wikipedia:


  In cryptography, a key derivation function (or KDF) derives one or more secret keys from a secret value such as a master key or other known information such as a password or passphrase using a pseudo-random function.


Is there a more formal security definition for what they are and what properties they are trying to guarantee, like ind-cpa security for encryption schemes, or collision resistance for hash functions?
This is a summary of the indicated section of Cryptographic Extraction and Key Derivation: The HKDF Scheme from user4982's comment.

Because this is in the context of an academic paper describing a HMAC based KDF, the terminology can be a bit excessive. I have tried to trim it down in this summary.

Definition of a KDF: 

A KDF takes four inputs: a key source value, an output length, a salt, and a context variable. The last two are optional. The security and quality of the KDF depends on the properties of the key source value.

Definition of a key source:

A source comprises two values, the key source material and auxiliary knowledge about it, created using an algorithm with sufficient statistical entropy to be considered random. (The auxiliary knowledge can be the distribution from a statistical entropy source, or the non-secret values of a DH key exchange, or any other related, but not secret data about the key source material)

Definition of the security of a KDF:

A KDF is secure if an attacker knowing the auxiliary data and salt value has little chance of deriving the key source material and context variable from repeated attempts at using the KDF with the auxiliary data, salt, and random key source materials and context variables (a.k.a brute forcing the KDF).