To prove there is an elementary topos with natural numbers object, it should be sufficient to assume ZF has a model. Probably ZF by itself, or IZF, is already sufficient. And probably even this is not necessary. Do we know what is?



Under what assumptions does an elementary topos (+infinity) exist?
This question was studied in the early days of elementary topos theory, and the connection was worked out by Bill Mitchell and J.C. Cole (independently, as far as I know). The MathSciNet references are:


MR0319757 (47 #8299) 
Mitchell, William,
Boolean topoi and the theory of sets. 
J. Pure Appl. Algebra 2 (1972), 261--274. 


MR0357116 (50 #9584) 
Cole, J. C.,
Categories of sets and models of set theory. The Proceedings of the Bertrand Russell Memorial Conference (Uldum, 1971), pp. 351--399. Bertrand Russell Memorial Logic Conf., Leeds, 1973. 


Essentially, they show that Boolean topos theory with a natural numbers object is equivalent to a version of Zermelo set theory (not ZF, i.e., without the replacement scheme) and with the separation scheme restricted to formulas with all quantifiers bounded (but the bounds can involve power sets, so quite a lot of separation is available). (I'm omitting some technicalities here, not because they're negligible but because I don't remember them.) 


If you don't assume Boolean logic for your topos, I don't think it changes the consistency strength of the theory. In any nontrivial topos with a natural numbers object, the subtopos of double-negation sheaves will also be nontrivial and will have a natural numbers object (the associated sheaf of the original one). In other words, the double-negation translation of classical logic into intuitionistic logic works here.


