Why do we ignore non-standard finite sets in ordinary mathematics? Here is a how a typical proof might look like in group theory--- Suppose we are given a finite group $G$. Enumerate the elements $g_1, \dots, g_n$. Now consider a formula $\phi(g_1, \dots, g_n)$ which discusses some property of $G$....
This proof is not rigorous. In any set theory I can think of, a finite set is equinumerous to $\{0, \dots, n}$ where $n$ may be a non-standard integer. So when we are proving things about finite sets, we really should allow the size of the set to be non-standard. But, at least implicitly, any proof assumes that $n$ is a standard integer.
This seems to be different than proofs of arithmetic, in which we can assume that the computations are occurring in the true structure of $\mathbf N$, which contains only standard integers. We may need extra axioms to pin down the behavior of $\mathbf N$, but we ultimately will never need the non-standard integers.
EDIT: I think I have boiled down this issue to the the following example.
We will prove that $CON(ZFC) \vdash (ZFC \vdash CON(ZFC))$, which is obviously false.
Consider the following proof. Suppose CON(ZFC) is true. Given a model $M$ of ZFC and $n$ an integer of $M$. If $n$ is a standard integer, then by assumption $n$ is not a proof of contradiction of ZFC. So we have shown that for all standard integers $n$ and all models $M$ of ZFC, $n \in M$ does not disprove ZFC. Hence, by the transfer principle, ZFC proves that all integers $n$ are not disproofs of ZFC. Hence ZFC proves CON(ZFC).
The key issue is that some formulas do behave differently for standard and non-standard formulas. In this case, the formula "$x$ is a disproof of ZFC" is a formula which picks out the non-standard integers.
 A: I'm used to formal logic being formulated internally. The theory of groups is not an external notion to whatever mathematical universe you're working in -- instead, it is an (internal) set of strings in a set-theoretic universe, or a finite-limit sketch in a category-theoretic universe. Models are then merely set functions or functors with appropriate properties. And proof theory and model theory are all defined internally to the universe.
In particular, for any internal natural number $n$, there are perfectly good formulas $\varphi(g_1, g_2, \cdots, g_n)$.
If you had an external notion of natural number (and a corresponding external notion of formal logic), then the internally constructed version could very well be infinitary when viewed from the external perspective. But only when viewed from the external perspective: it is still finitary when viewed internally to the model.
A: Your example concerning proving the consistency of ZFC in ZFC invokes the transfer principle in a situation where it simply doesn't hold.  The transfer principle is for elementary extensions, so your use of it presupposes that the natural numbers of $M$ (with their addition and multiplication) form an elementary extension of the standard natural numbers.  Con(ZF) will indeed be true in such $M$'s (if, as you assumed, its really true), but such $M$'s are far from being all the models of ZFC, so it wouldn't follow that ZFC proves Con(ZF).
I would also question the description, at the beginning of your message, of a typical proof in group theory.  All the proofs I've seen in group theory (on its own --- not set-theoretic independence results about group theory) have been formalizable in ZFC.  What they say about finite groups (or finite sets) makes perfectly good sense and remains correct if interpreted in any model $M$ of ZFC, with "finite" being interpreted in $M$ also (and therefore including non-standard finite numbers, if there are such numbers in $M$).
A: Non-standard numbers do not exist in isolation but only in the context of working in a non-standard model. If we take an argument of the sort you mention and interpet it in a non-standard model, Eveything Will Be Just Fine. True, the model has some infinite numbers from which we can make strange things such as non-standardly large syntactic expressions, non-standard "finite yet infinitely large" sequences of powers $1, x, x^2, \ldots, x^n$, etc., but so what? The beauty of non-standard models is that all the "finite" proofs still work in it, so I do not understand your objection.
A: Here are a few nice quotes from treatises on non-standard analysis:

These non-standard finite ordinals do correspond to idea of “infinitely great numbers”, 
  (that's why we call them 'unlimited'); still, they are finite ordinals, according to the mathematical definition of finity (note : a set is finite if, and only if, there is no possible bijection between one of its sub-sets and itself). 
Moreover, any classical theorem that is true for all standard numbers is necessarily true for all natural numbers. Otherwise the formulation "the smallest number that fails to satisfy the theorem" would be an internal formula that uniquely defined a non-standard number.
Non-standard numbers are precisely those that cannot be uniquely specified (due to limitations of time and space) by an internal formula.
  Non-standard numbers are elusive: each one is too enormous to be manageable in decimal notation or any other representation, explicit or implicit, no matter how ingenious your notation. Whatever you succeed in producing is by-definition merely another standard number.
Note that the ZFC schemata of separation and replacement are not extended to the new language, they can only be used with internal formulas. 

#2 tells you why it is enough to deal with standard integer cardinalities in all proofs like the one you quoted and #4 is the reason why the non-standard analysis is not quite an extension of ZFC: adding a huge set of predicates and explicitly prohibiting their usage in the old axioms of the theory to avoid any contradiction smells of cheating. Basically, IST postulates that each infinite set contains elements beyond our perception but whatever is true for all elements within our reach is true for them too. I personally consider IST one of those unwelcome monsters that feed on the unavoidable incompleteness of ZFC but I'm a known retrograde :). Nevertheless, all our standard proofs of standard properties for finite sets remain valid in IST if you just mindlessly add an application of the transfer axiom in the end, so IMHO it is a bit too early to declare them "non-rigorous". 
A: You are right, a lot of published proofs are non-rigorous in something like the sense you describe.  See this answer and the comments attached to it:
Why is it so difficult to write complete (computer verifiable) proofs?
I remember chasing down some of the references from that post and finding them interesting too.
The Bundy et paper is here: http://www.jstor.org/pss/30039733  (link courtesy of schropp on reddit).
