Non-forking global types Work inside a large saturated model ${\cal U}$. Let $p(x)$ be a global type that does not fork (=divide) over $A$. Let $\varphi(x,b)$ be a formula in $p(x)$. And let $\langle b_i:i<\omega\rangle$ such that $b_0=b$ and $b_i\equiv_A b$.
Is the following true?

For every $k<\omega$ there $I\in[\omega]^k$ and $f\in{\rm Aut\,}({\cal U}/A)$ such that $p(x)$ contains $\varphi(x,fb_i)$ for all $i\in I$.

(I suspect the answer is "of course not". Then, can the statement be approximated by anything true?)
 A: The statement is true for stable theories. Let me state it in a stronger form:
Proposition: Let $T$ be stable, let $p(x)$ be a global type that does not fork over $A$, let $\varphi(x,b)$ be a formula in $p(x)$, and let $\langle b_\alpha \mid i\in\omega \rangle$ be such that $b_0=b$ and $b_i \equiv_A b$ for all $i\in\omega$. Then there is an infinite subset $I\subseteq \omega$ and $f\in\text{Aut}(\mathcal{U}/A)$ such that $p(x)$ contains $\varphi(x,f(b_i))$ for all $i\in I$.
Proof: Since $p$ does not fork over $A$, there is a formula $d_p\varphi(y,a)$ with $a\in\text{acl}^\text{eq}(A)$, such that $\varphi(x,b')\in p$ if and only if $\mathcal{U}\models d_p\varphi(b',a)$. Now for all $i$, let $f_i\in\text{Aut}(\mathcal{U}/A)$ be an automorphism with $f_i(b) = b_i$. Since $a$ is algebraic over $A$, there are only finitely many images of $a$ under the $f_i$, so there is some $a'$ and an infinite subset $I\subseteq \omega$ such that $f_i(a) = a'$ for all $i\in I$. Applying $f_i$ to $\mathcal{U}\models d_p\varphi(b,a)$, we have $\mathcal{U}\models d_p\varphi(b_i,a')$. Now fix some $j\in I$ and shift back by $f = f_j^{-1}$. This gives $\mathcal{U}\models d_p\varphi(f(b_i),a)$ for all $i\in I$, so $\varphi(x,f(b_i))\in p$ for all $i\in I$.
What about in unstable theories? Here's a silly observation: If $p$ is an $A$-invariant type, then your statement holds. Whether $\varphi(x,b)\in p$ depends only on $\text{tp}(b/A)$, so $\varphi(x,b_i)\in p$ for all $i$.
Now under the assumption of NIP, nonforking is closely related to invariance. To be precise, $p(x)$ does not fork over $A$ if and only if it is Lstp$_A$-invariant. If we replace the use of definability of types with Lascar invariance, we can prove the following weaker form:
Proposition: Let $T$ be NIP, let $p(x)$ be a global type that does not fork over $A$, let $\varphi(x,b)$ be a formula in $p(x)$, and let $\langle b_\alpha \mid \alpha<\lambda\rangle$, with $\lambda$ infinite and larger than the number of Lascar strong types over $A$, such that $b_0=b$ and $b_\alpha \equiv_A b$ for all $\alpha$. Then there is an infinite subset $I\subseteq \lambda$ and $f\in\text{Aut}(\mathcal{U}/A)$ such that $p(x)$ contains $\varphi(x,f(b_i))$ for all $i\in I$.
Proof: By the choice of $\lambda$, there is some infinite subset $B$ of the $b_\alpha$ which all have the same Lascar strong type over $A$. Let $b'\in B$, and let $f\in \text{Aut}(\mathcal{U}/A)$ move $b'$ to $b$. Then for all $b_\alpha\in B_0$, $f(b_\alpha)$ has the same Lascar strong type as $f(b') = b$ over $A$, so by Lascar-invariance of $p$, $\varphi(x,f(b_\alpha))\in p$ for all $b_\alpha\in B$.
Note that we can take $\lambda = \omega$ as you wanted if $A$ is a model, or more generally if $\text{bdd}(A) = A$ (since Lascar strong type = Kim-Pillay strong type in NIP theories), as then there is only one Lascar strong type over $A$. In any case, there are at most $2^{|A|+|T|}$ Lascar strong types over $A$, so $\lambda = (2^{|A|+|T|})^+$ always works.
Outside the NIP world, nonforking need not have any relation to invariance. Here's a counterexample over a model in the simplest theory with IP, the random graph:
Let $M$ be a small model, and let $A$ and $B$ be countably infinite subgraphs of $\mathcal{U}$ outside $M$, such that $A$ is complete, $B$ is co-complete (no edges), and there are no edges between $A$, $B$, and $M$. Let $p(x)$ be the global type determined by $\{x\neq c\mid c\in\mathcal{U}\}\cup\{xEc\mid c\in A\}\cup\{\lnot xEc\mid c\notin A\}$. $p$ is consistent and does not fork over $M$.
Now let $\langle b_i\mid i\in\omega\rangle$ be a sequence such that $b_0\in A$ and $\langle b_i\mid i>0\rangle$ enumerates $B$. Note that all the $b_i$ have the same type over $M$ (no edges to $M$). Also $xE b_0$ is in $p$, but $\lnot xE b_i$ is in $p$ for all $i>0$. Take $k = 2$. For any pair $(b_i, b_j)$, there is no edge between $b_i$ and $b_j$, so there is no automorphism of $\mathcal{U}$ over $M$ moving both $b_i$ and $b_j$ into $A$ (since $A$ is complete). Hence there is no $f$ such that $x E f(b_i)$ and $x E f(b_j)$ are both in $p(x)$.
