Proving HMAC collision probability bounds? Could someone point to results or proofs about the probability of $$HMAC(k, m_1) = HMAC (k, m_2)$$ assuming the underlying hash function is SHA-256? Would those probabilities be higher/lower if $m_1$ and $m_2$ are not independent? 

Please don't point to birthday attack results. I am only interested in the probability that the tags are equal given two messages (random or not) and a single key.
The following is a method of calculating the probability using the random Oracle model, where the random Oracle is substituted for the HMAC function:

$\mathcal{A}^{\mathcal{O}}$ works as follows:

Generate $m_1$ and $m_2$ in whatever way

set: $tag = \mathcal{O}(m_1)$

output: $[m_2,tag]$

and observe that $\mathcal{A}^{\mathcal{O}}$ has trivial runtime and makes only one query to the oracle. $\:$

This leads to:

$\operatorname{Prob}(m_1 ≠ m_2 \text{ and } \operatorname{HMAC}(k,m_1) = \operatorname{HMAC}(k,m_2))= \operatorname{Prob}(\mathcal{A}^{\text{HMAC}(k,\cdot)} \: \text{succeeds})$