From what I know, Cohen constructed a model that satisfies $ ZF\neg C $. But if such a model exists, how can AC be an axiom? Wouldn't it be a contradiction to the existence of the model?
Only explanation I can think of, is that this model requires other axioms in addition to ZF, and these axioms contradict AC. Is it true?
You're treating the word "axiom" as you were probably taught in high school. That an axiom is something which is "simply true as an assumption".
Modern mathematics has changed that definition to "an assumption made in a certain context". Not every axiom is called an axiom, some axioms are proved as theorems, and sometimes lemmas are used for axioms. And not to mention various hypotheses used as axioms sometimes.
But in the modern context, an axiom is really just an assumption that you begin with. And different contexts begin with different axioms. From the axioms of $\sf ZF$ we can prove that the axioms of Peano hold in the natural numbers; we can prove that the completeness axiom holds for the real numbers. So these are all theorems of $\sf ZF$.
From the axioms of $\sf ZF$ and Zorn's Lemma we can prove the axiom of choice, so the axiom of choice is a theorem of Zorn's Lemma when working in $\sf ZF$.
When Cohen showed there is a model of $\sf ZF+\lnot AC$, he effectively completed the proof that $\sf ZF$ neither proves nor disproves the axiom of choice. Which is quite fitting as far as "axiom" goes. So you shouldn't worry about it, this is more of a linguistic issue.
The existence of a model of a statement does not mean that statement is "true" (whatever that means; see below). For example, the Poincare disk is a model of Euclid's first four postulates plus the negation of the parallel postulate; this does not mean that the parallel postulate is "false."
What having a model of a set of statements does mean, is: that set of statements is consistent. In particular, if there is a model of $T\cup\{\neg p\}$, then $p$ cannot be a consequence of $T$. Cohen's result, for instance, shows that $AC$ cannot be proved from $ZF$ alone.
As to your comments about its value of an axiom: knowing that there is a model of $ZF$ where $AC$ fails shows that, if we believe that $AC$ is "true" (again, see below), then we have a good reason to adopt it as an axiom. Conversely, if there were no model of $ZF+\neg AC$, that would mean (by Goedel's completeness theorem) that $ZF$ proves $AC$, so there would be no need to add $AC$ as an additional axiom.
OK, so now another question: what is going on when we use the word "true" in these contexts? Basically, we're presupposing the existence of a "correct" model. But the statement "$AC$ is true in the actual universe of set theory" doesn't have anything to do with the statement "there is some model in which $AC$ fails."
To repeat: all we know from the existence of a model of $ZF+\neg AC$ is that $AC$ is not a consequence of $ZF$.
The same idea as other answers, but a different explanation (which makes more sense to me, at least): there is no such thing as true, period. A statement can only be true or false in some model, which consists of a certain set of "original" statements whose truth is assumed, and everything provable from those statements. The "original" statements are the axioms.
So any given statement might be an axiom, or not an axiom, depending on the model. The axiom of choice, for example, is an axiom in ZFC, but you could make another model in which it is not an axiom.
