Type of set theory in Halmos' naive set theory.

As you have surmised, Halmos develops ordinary ZFC from axioms.

Note that the fact that he "does not define the notion of a set formally" is not an exception from doing things axiomatically -- on the contrary, it is the very core of the axiomatic method (from a modern perspective) that you don't bother to attempt to define what the objects you're speaking about are. Instead we have axioms that tell us how those objects behave, and that is all we need to know in order to prove things about them.

The title of Halmos's book is something of a misnormer, at least relative to how the terminology has come to be used. Usually, "naive set theory" means the inconsistent theory assumed by Cantor and the rest of the 19th century, in which every definable collection is a set, leading to Russell's paradox and others. But that is certainly not what Halmos is doing.

What Halmos calls "naive" seems to be simply the fact that he develops set theory without first presenting a theory of formal logic -- so he has explicit axioms for set theory, but the way he reasons from those axioms are by the ordinary quasi-formal English prose that is used in the rest of mathematics too, rather than the usual formal-logic game of symbol sequences and exact mechanical rules for "what is a valid proof".