How exactly does on describe the formal semantics of the Applied $\pi$-Calculus?
You are roughly correct. From an operational point-of-view, applied-$\pi$ is 'just' a $\pi$-calculus where interesting  values (rather than just pure names) can be communicated.

Note that in process theory we usually care about coarser notions of equality, such as observational equivalence. This is defined in Section 4.1. Alas observational equivalence is hard to work with in practise due to the universal quantification over all contexts, so we define a second relation which is easier to deal with, in this case  labelled bisimilarity. In order to do this, we need labelled transitions rather than reductions. We must show that  these two forms of computation coincide.

To make matters even more complicated, Theorem 1 which claims that observational equivalence coincides with labelled bisimilarity is wrong.