In general, you don't really have to redefine the notation or definition of security. You can just add a verification oracle for the adversary in the experiment used by the security definition. To understand that better, let's go a bit into detail about what security is.
Security is in general the combination of an adversary model and a security goal against/for a cryptographic scheme. Most cryptographers don't really like saying "that is secure", they want a specification of what secure means and the combination mentioned above will most likely satisfy them.
A security definition now formally describes this combination and also describes the context (e.g. what category of security, computation, perfect or quantum, what negl is, and so on). But how does the security definition evaluate whether an adversary is able to break the stated security notation or not?
The definition needs to simulate the scheme and the adversary on an abstract and formal level. This makes it possible to evaluate the success probability of an adversary and state whether security is archived or not. This simulation is mostly referred to as the experiment. In the experiment, everything for the simulation must formally be described. The experiment can generally be imagined as a game between an adversary and a challenger, where the challenger computes the administrative part and the adversary tries to break the scheme using the oracles, which simulate the extended power of the adversary.
A proof of security finally puts everything together in a nutshell and tells us, whether security is archived or not for an analysed scheme.
Back to your original question. A definition may look like this:
A message authentication code $\Pi= (gen, mac, verify)$ is existentially unforgeable under an adaptive chosen-message attack with verification access, if for all PPT adversaries $A$, there exists a negligible function $negl$ such that
$$
\Pr[Game_{A,\Pi}(1^n)=1] \le negl
$$
where negl is a negligible function and $n$ is the security parameter.
The corresponding experiment (Game) may look like this:
$
k \gets gen(1^n)\\
(m^*,t^*) \gets A^{mac_k(\cdot), vrfy_k(\cdot)}(1^n)\\
\text{Let $Q$ be the set of all queries.} \\
\text{if } verify_k(m^*,t^*)=1 \ \mathbf{ and } \ m^* \notin Q \\
\ \ \ \ \text{return } 1 \\
\text{return } 0
$
Of course, now you could go into detail by describing the oracles formally, too.
