Secure MAC when the adversary has a verification oracle A message authentication code (MAC) is defined by a triple of efficient algorithms $(\mathsf{Gen}, \mathsf{MAC}, \mathsf{Verif})$, which satisfy the following (the definition is taken from section 4.3 of the Katz-Lindell book):


On input $1^n$, the algorithm $\mathsf{Gen}$ generates a key $k \ge n$.
On input $k$ generated by $\mathsf{Gen}$, and some message $m \in \{0,1\}^*$, the algorithm $\mathsf{MAC}$ generates a tag $t$. We write $t \gets \mathsf{MAC}_k(m)$.
On input a triple $(k,m,t)$, the algorithm $\mathsf{Verif}$ generates a single bit $b$. We write $b \gets \mathsf{Verif}_k(m,t)$.


It is required that for all $k$ output by $\mathsf{Gen}$ and all $m \in \{0,1\}^*$, we have $\mathsf{Verif}_k(m, \mathsf{MAC}_k(m)) = 1$.

The security requirement is defined via the following experiment, between the challenger and the adversary $A$:


$k \gets \mathsf{Gen}(1^n)$.
$(m,t) \gets A^{\mathsf{MAC}_k(\cdot)}(1^n)$.
Let $Q$ denote the set of all queries that $A$ asked to its oracle.
The output of the experiment is defined to be 1 if and only if:

$\mathsf{Verif}_k(m, t) = 1$, and
$m \notin Q$.



The MAC is considered secure if the probability that the experiment outputs 1 is negligible in $n$.



The experiment above resembles a "chosen plaintext" experiment against a symmetric encryption scheme, where the adversary can obtain ciphertexts corresponding to messages of his choice. In a more powerful attack, called "chosen ciphertext" attack, the adversary is allowed access to a decryption oracle as well.

So, my question is:


  What happens if we allow the MAC-adversary to access a verification oracle as well? In other words, what if line 2 of the experiment is replaced with the following:
  
  $(m,t) \gets A^{\mathsf{MAC}_k(\cdot),\ \ \mathsf{Verif}_k(\cdot, \cdot)}(1^n)$.
  
  Notice that in the new experiment, $Q$ only includes queries $A$ asks from the $\mathsf{MAC}_k$ oracle.
If there is a secure message authentication code according to either definition,
  
  then there is a system that the book's definition classifies as a secure
  
  message authentication code and your definition classifies as insecure.


Let $\:\langle \operatorname{Gen}\hspace{.02 in},\hspace{-0.02 in}\operatorname{MAC}\hspace{.02 in},\hspace{-0.05 in}\operatorname{Verif}\hspace{.02 in}\rangle\:$ be secure according to either definition. $\;\;$ Since the book's definition

is weaker than your definition, it is in particular secure according to the book's definition.

Fix some efficiently-computable and efficiently-invertable coding of

ordered pairs, for example, concatenating an efficiently-computable and

efficiently-invertible prefix-free representation  of the left entry to the right entry.

Let $\operatorname{MAC}_k\hspace{-0.09 in}'$ work by pairing the output of $\operatorname{MAC}_k$ with the empty string.

Let $\operatorname{Verif}_k\hspace{-0.09 in}'$ accept if and only if [[$\operatorname{Verif}_k$ would accept the message and the left entry

of the tag] and [the right entry of the input is a prefix of $k$]]. $\;\;$ $\:\langle \operatorname{Gen}\hspace{.02 in},\hspace{-0.02 in}\operatorname{MAC}\hspace{.01 in}\hspace{-0.03 in}'\hspace{-0.02 in},\hspace{-0.04 in}\operatorname{Verif}\hspace{.01 in}\hspace{-0.03 in}'\hspace{.02 in}\rangle\:$ is clearly efficient and satisfies the requirement. $\;\;\;$ Since [pairing the tags with the empty string for]

and [taking the left entry of the output of] a feasible adversary attacking the book's

definition of the security of $\:\langle \operatorname{Gen}\hspace{.02 in},\hspace{-0.02 in}\operatorname{MAC}\hspace{.01 in}\hspace{-0.03 in}'\hspace{-0.02 in},\hspace{-0.04 in}\operatorname{Verif}\hspace{.01 in}\hspace{-0.03 in}'\hspace{.02 in}\rangle\:$ cannot have a non-negligible probability

of breaking the book's definition of security for $\:\langle \operatorname{Gen}\hspace{.02 in},\hspace{-0.02 in}\operatorname{MAC}\hspace{.02 in},\hspace{-0.05 in}\operatorname{Verif}\hspace{.03 in}\rangle\:$, $\:$ the book's

definition also classifies $\:\langle \operatorname{Gen}\hspace{.02 in},\hspace{-0.02 in}\operatorname{MAC}\hspace{.01 in}\hspace{-0.03 in}'\hspace{-0.02 in},\hspace{-0.04 in}\operatorname{Verif}\hspace{-0.01 in}\hspace{-0.03 in}'\hspace{.02 in}\rangle\:$ as a secure message authentication code.

However, once an adversary gets any valid message-tag pair for $k$, $\:2\hspace{-0.03 in}\cdot \hspace{-0.03 in}(\operatorname{length}(k)\hspace{-0.04 in}+\hspace{-0.05 in}1)\:$ 

adaptive queries to $\operatorname{Verif}_k\hspace{-0.09 in}'$ is sufficient to learn $k\hspace{.01 in}$, which would allow forgeries on any message.

Thus your definition classifies $\:\langle \operatorname{Gen}\hspace{.02 in},\hspace{-0.02 in}\operatorname{MAC}\hspace{.01 in}\hspace{-0.03 in}'\hspace{-0.02 in},\hspace{-0.04 in}\operatorname{Verif}\hspace{-0.01 in}\hspace{-0.03 in}'\hspace{.02 in}\rangle\:$ as insecure. $\;\;\;$ QED




  The strong unforgeability versions of the two definitions are equivalent.



(The "strong unforgeability" versions are obtained by replacing $Q$ with

the set $Q^+$ given in my next sentence, and that is needed to make the 

encrypt-then-mac construction provide ciphertext integrity and be IND-CCA2.)

Initialize $\:Q^+\:$ as the empty set, and put $\: \langle m,\hspace{-0.03 in}t\rangle \:$ into $\:Q^+$

each time $\operatorname{MAC}_k$ outputs $t$ on a query of $m$ .

Define a query to be trying if and only if it is submitting

to $\:\operatorname{Verif}_{\hspace{-0.02 in}k}\:$ a pair that was already put in $\:Q^+\:$.

Define a query to be early-trying if and only if it is trying and

did not come after any trying query that $\:\operatorname{Verif}_{\hspace{-0.02 in}k}\:$ accepted.

$B^{\hspace{.02 in}\operatorname{MAC}_k(\cdot)}\hspace{-0.02 in}\left(\hspace{-0.03 in}1^n,\hspace{-0.02 in}q,\hspace{.02 in}j\hspace{-0.01 in}\right) \;$ interacts with $A$ as follows:

Using less than $\hspace{.02 in}j$ random bits, choose $\;\; r \: \in \: \left\{\hspace{-0.03 in}1,\hspace{-0.03 in}2\hspace{.02 in},\hspace{-0.03 in}3,...,\hspace{-0.02 in}q\hspace{-0.04 in}-\hspace{-0.04 in}2\hspace{.02 in},\hspace{-0.02 in}q\hspace{-0.04 in}-\hspace{-0.05 in}1,\hspace{-0.02 in}q\hspace{-0.02 in}\right\} \;\;$ almost uniformly.

"Forward" all of $A$'s $\:\operatorname{MAC}_k(\cdot)\:$ queries to $\:\operatorname{MAC}_k(\cdot)\:$ and give that oracle's

(actual) output to $A$, give $0$ as the outputs on the first up to $r\hspace{-0.04 in}-\hspace{-0.05 in}1$ trying queries,

and give $1$ as the outputs of $\:\operatorname{Verif}_{\hspace{-0.02 in}k}\:$ on queries to it that are not trying.

If $\:A^{\operatorname{MAC}_k(\cdot),\operatorname{Verif}_k(\cdot,\cdot)}\hspace{-0.03 in}\left(\hspace{-0.03 in}1^n\hspace{-0.02 in}\right)\:$ makes an $r$-th trying query, then output what that query was.

If $\:A^{\operatorname{MAC}_k(\cdot),\operatorname{Verif}_k(\cdot,\cdot)}\hspace{-0.03 in}\left(\hspace{-0.03 in}1^n\hspace{-0.02 in}\right)\:$ gives output, then give that same output.

With everything's randomness fixed, if $\:A^{\operatorname{MAC}_k(\cdot),\operatorname{Verif}_k(\cdot,\cdot)}\hspace{-0.03 in}\left(\hspace{-0.03 in}1^n\hspace{-0.02 in}\right)\:$ makes exactly $\:r\hspace{-0.03 in}-\hspace{-0.04 in}1\:$ early-trying queries and succeeds in the strong unforgeability version of your experiment, then

$B^{\hspace{.02 in}A,\operatorname{MAC}_k(\cdot)}\hspace{-0.03 in}\left(\hspace{-0.03 in}1^n,\hspace{-0.02 in}q,\hspace{.02 in}j\hspace{-0.01 in}\right)\:$ succeeds in the strong unforgeability version book's experiment.


  Therefore $B$ is a constructive straight-line reduction from succeeding in the strong unforgeability version of your experiment with probability at least $\epsilon$ in a way that
  
  makes less than $q$ early-trying queries, to succeeding in the strong unforgeability
  
  version of the book's experiment with probability greater than $\;\; \left(\hspace{-0.03 in}\frac1q\hspace{-0.03 in}-\hspace{-0.03 in}\frac{q}{2\text{^}j}\hspace{-0.04 in}\right)\cdot \epsilon \;\;\;$.
  
  $B$ uses less than $\hspace{.02 in}j$ random bits, has to handle insertions into and membership
  
  testing for [a set with less than $q$ elements, each of which is an ordered pair whose
  
  left entry is one of the inner algorithm's queries to $\:\operatorname{MAC}_k\:$ and whose right entry is
  
  $\operatorname{MAC}_k\hspace{-0.02 in}$'s$\:$ response to that query], and has only trivial additional complexity beyond that.


Clearly, "ignore the $\operatorname{Verif}_k$ oracle" is a constructive straight-line reduction from succeeding

in the strong unforgeability version of the book's experiment to succeeding in the strong unforgeability version your experiment, and that reduction is almost perfectly tight.

Therefore the strong unforgeability version of your definition gives the same

asymptotic MACs as the strong unforgeability version the book's experiment.