Jech, Axiom of Choice, Chapter 5, Problem 25 says that a certain symmetric model of ZF disproves the Hahn-Banach theorem, by failing to have a measure on $\mathcal{P}(\omega)/I$ where $I$ is the ideal of finite sets. The forcing conditions are finite $0,1$-valued functions with domain contained in $\omega\times\omega,$ and the symmetries act on forcing conditions by permuting digits ($(\pi p)(\pi(n,m))=p(n,m)$ where $\pi$ is the identity for sufficiently large $n$) and flipping bits ($(\pi p)(n,m)=\pi_{n,m}(p(n,m))$). The permutations have to be in the ground model so I don't see how they can be useful - they are just shifting around some generic binary digits. I've copied the exercise below. It relies on the notation in Chapter 5 for symmetric submodels of generic models.
Why does the model in problem 25 have no measure on $\mathcal P(\omega)/I$?
The historical remarks section says "Problem 25 is due to Pincus [1973b]" where [1973b] = The strength of the Hahn-Banach Theorem, Proc. 1972 Symp. on Nonstandard Analysis, Lecture Notes in Math. (Springer, Berlin). But that paper doesn't use a symmetric submodel, it uses an inner model of a forcing extension - see that paper's definition of $M$ on page 237.
I'm fine with what I understand of Pincus's proof and I think I can see why Hahn-Banach would be false in a suitable inner model of a forcing extension, such as the Cohen model L(A) "Fefferman's model" $HOD^{V[G]}(a_1,a_2,\dots)$ containing infinitely many mutually $V$-generic Cohen reals $a_1,a_2,\dots$ but not the set containing them. But I don't see how this is quite the same as the permutation models.
I can construct a symmetric submodel disproving Hahn-Banach using conditions of finite partial functions $\omega\times\omega\to\omega$ instead of $\omega\times\omega\to\{0,1\},$ and symmetries that permutate each value separately, so they're of the form $(\pi p)(n,m)=\pi_{n,m}(p(n,m)).$ Breaking $\omega$ into three infinite sets $A,B,C,$ there is a permutation $\alpha$ (in the ground model) that sends $A$ to $B$ to $C$ to $A,$ and a permutation $\beta$ that sends $A$ to $B\cup C$ to $A.$ I can use $\alpha$ to argue that the real $y_n=\{m\in\omega:(\exists p\in G)\; p(n,m)\in A\}$ must have $\mu(y_n)=\tfrac13,$ and use $\beta$ to argue that $\mu(y_n)=\tfrac12,$ giving a contradiction. But I don't see how to translate this idea to use $0,1$-valued conditions.
Halbeisen's "Combinatorial Set Theory" has details of "A Model in Which Every Ultrafilter over $\omega$ Is Principal" but does not consider measures.
Jech, Axiom of choice, Chapter 5, Problem 25:
*25. Independence of the Hahn-Banach Theorem. Modify the construction of the model $\mathcal N$ in Problem 24 as follows: in addition to the ‘symmetries’ $\pi_X,$ consider those ‘permutations of $\omega\times\omega$’ which move only elements in finitely many columns (compare with Problem 16). In the resulting model, there is no measure on the Boolean algebra $\mathcal P(\omega)/I,$ where $I$ is the ideal of finite sets. Therefore (cf. Problem 2.19), the Hahn-Banach Theorem fails in the model.
[Hint: Let $\underline{\mu}\in\mathrm{HS}$ be a measure on $\mathcal P(\omega),$ vanishing on finite sets, with $\operatorname{sym}(\underline{\mu}) \supseteq \operatorname{fix}(e).$ The same argument as in Problem 24 gives $\mu(x_n)=\mu(\omega-x_n)$ whenever $n \not\in e;$ therefore $\mu(x_n) = \tfrac12.$ Then use a permutation $\pi$ which maps $\underline{x}_{n_1}$ and $\underline{x}_{n_2}$ (up to a finite set) onto disjoint subsets of $\underline{x}_{n_3}$ and such that $\pi\underline{\mu}=\underline{\mu}.$ A contradiction.]
It should be mentioned that the models in Problems 24 and 25, as well as the model $\mathcal N_2$ in Problem 16 are the same. This model is the least submodel of the basic Cohen model which contains all the sets $x_n$ (but not the collection $A = \{x_n : n \in \omega\}$ of these sets).
I am curious about that last sentence as well!
And here's Problem 24, for the definition of $\mathcal N.$ I have no questions about this exercise.
24. Let $(P, <)$ be the set of all finite functions $p$ with values $0,1,$ and $\operatorname{dom} (p) \in\omega\times\omega.$ Every $X \subseteq\omega\times\omega$ induces an automorphism $\pi_X$ of $\mathrm{RO}(P)$ via $(\pi_X)(n, m) =$ either $p(n, m)$ or $1 -p(n, m),$ according to whether $(n, m) \not\in X$ or $(n, m) \in X.$ Let $\mathcal G = \{\pi_X : X \subseteq \omega\times\omega\}.$ Let $\mathcal F$ be the filter on $\mathcal G$ generated by $\{\operatorname{fix}(e) : e \subseteq \omega\text{ finite}\},$ where $\operatorname{fix} (e) = \{\pi_X : X \cap (e \times \omega) = 0\}.$ Let $\mathcal N$ be the corresponding symmetric model.
THEOREM. In $\mathcal N,$ there is no nontrivial ultrafilter over $\omega.$
[Hint: Let $\underline{D}\in \mathrm{HS}$ and let $p \Vdash\underline{D}$ be an ultrafilter over $\check\omega;$ let $\operatorname{sym} (\underline{D}) \supseteq \operatorname{fix} (e)$ for some finite $e \subseteq \omega.$ Let $n \not\in e$ and let $x_n$ be the subset of $\omega$ defined in (5.11). If $q\Vdash\underline{x}_n\in \underline{D},$ let $m_0$ be such that for each $m\geq m_0,$ $(n,m)\not\in\operatorname{dom}(q);$ let $X = \{(nm), m \geq m_0\}.$ Then we have $\pi_Xq=q\Vdash\pi_X(x_n)\in\underline{D}.$ Similarly for $q \Vdash \underline{x}_n \not\in D$ [sic]. Since $x_n\cap i(\pi\underline x_n)\subseteq m_0,$ $D$ must be trivial.]
(5.11) is $$x_n=\{m\in\omega:(\exists p\in G)\;p(n,m)=1\}.$$