Properties of the bilinear pairing groups?

In pairing-based cryptography, bilinear pairings are usually defined as follows:

Let $G_1, G_2, G$ be finite cyclic groups of the same order. A bilinear pairing is then a map $e : G_1 \times G_2 \rightarrow G$ which is bilinear, that is: $$ e(p^a, q^b) = e(p, q)^{ab} $$

It is often also implied or required that:

• $e$ is not the trivial pairing which maps all inputs to the neutral element of $G$
• We have a way to compute $e$ 'efficiently'
• if $g_1$ is a generator of $G_1$, and $g_2$ of $G_2$, then $e(g_1, g_2)$ is a generator of $G$
• In some contexts $G_1 = G_2$ is used, that is $e$ will be of the form $e : G_1 \times G_1 \Rightarrow G$.

Thus, informally, a bilinear pairing allows to "pull out" the exponents (assuming multiplicative notation) of its inputs.

The correctness proof you quote is straight-forward, then: $$ \begin{align} e(g^r,H(id)^x) & = e(g, H(id))^{rx} & \text{ bilinearity} \\ & = e(g, H(id))^{xr} & \text{ commutativity} \\ & = e(g^x, H(id)^r) & \text{ bilinearity} \end{align} $$

You can find a decent (I find) introduction into pairing-based cryptography in these lecture slides by John Bethencourt.