In this paper, we model fresh names in the $\pi$-calculus using
  \emph{abstractions} with respect to a new binding operator $\theta$.
  Both the theory and the metatheory of the $\pi$-calculus benefit
  from this simple extension.  The operational semantics of this new
  calculus is \emph{finitely branching}. Bisimulation can be given
  without mentioning any constraint on names, thus allowing for a
  straightforward definition of a coalgebraic semantics, within a
  category of coalgebras over \emph{permutation algebras}.  Following
  previous work by Montanari and Pistore, we present also a
  \emph{finite} representation for \emph{finitary} processes and a
  finite state verification procedure for bisimilarity, based on the
  new notion of \emph{$\theta$-automaton}.