A few questions on nonstandard analysis

$\mathsf{IST}$ is a conservative extension of $\mathsf{ZFC}$: any internal formula that can be proved within internal set theory can be proved in $\mathsf{ZFC}$. This is proved in the Appendix to Edward Nelson’s original $1977$ paper in the Bulletin of the American Mathematical Society, ‘Internal Set Theory: A New Approach to Nonstandard Analysis’.

To answer your first question, one can indeed think of nonstandard analysis, in a first approximation, as entailing the existence of infinitesimal numbers as you write, but to be more precise one would have to elaborate further. I like to think of it in terms of three approaches (other editors may disagree), as follows:

(1) the most straightforward approach (in my opinion) is through the construction of a proper field extension $\mathbb R^\star$ (notation varies, but let's stick with this one which is used in Keisler's book, see http://www.math.wisc.edu/~keisler/calc.html) of the real field $\mathbb R$. This field extension can be constructed in a way somewhat similar to constructing $\mathbb R$ out of the rationals $\mathbb Q$. Namely, one starts with sequences of real numbers, introduces a suitable equivalence, and obtains the hyperreal field $\mathbb R^\star$ as the quotient. This construction is called the ultrapower construction. A serious undergraduate algebra course provides enough background to understand this construction; namely what is required is the existence of a certain maximal ideal in a suitable ring.

(2) A more sophisticated route (and the one taken by Robinson in his 1966 book, see http://www.google.co.il/books?id=OkONWa4ToH4C&source=gbs_navlinks_s) is to invoke the compactness theorem from mathematical logic (more specifically, model theory) so as to prove the existence of such an $\mathbb R^\star$ (in Robinson's book this is denoted $^\star\mathbb R$).

(3) Edward Nelson's approach, called IST (internal set theory) is a reformulation of Robinson's approach where, instead of extending the field $\mathbb R$, Nelson takes the "syntactic" route. This means that the language of ordinary set theory is enriched by the addition of a unary predicate "Standard". Then infinitesimals are found within the "ordinary" $\mathbb R$ itself; so to speak they have been there all along, it's just that we haven't noticed (because the ordinary syntax of set theory is insufficiently rich). An infinitesimal number is NOT "Standard".

All three approaches are equivalent (at least at a basic level), so one proves the same theorems in all of them. No new axioms are needed beyond those of ZFC.

A more detailed summary by Joel David Hamkins appears here.