Modifications of CBC-MAC I'm preparing myself to exam, but I have a lot of troubles with rigorous proofs. This post is very long, but this is because I remind here 2 long definitions.


  At the beginning I want to remind the definicion of CBC-MAC.
  
  Let $F$ be a pseudo-random function. We define the CBC-MAC as $(Gen,Mac,Vrfy)$ as follows:
  
  (a) $Gen$ on input $1^n$ outputs a key $(k_1,k_2) \in \lbrace 0,1 \rbrace^n \times \lbrace 0,1 \rbrace^n$ selected uniformly at random.
  
  (b) $Mac$ on input a key $(k_1,k_2) \in \lbrace 0,1 \rbrace^n \times \lbrace 0,1 \rbrace^n$ and message $m \in \lbrace 0,1 \rbrace^*$ does the following.
  
  
  It first unambiguously pads the message $m$ to $m^{pad}=m|1|0^l$, where $l \in \lbrace 0,\ldots,n-1 \rbrace$ and $||m^{pad}|| \equiv 0 \mod n$.
  Then it splits $m^{pad}$ into $r$ blocks of $n$-bit: $m^{pad}=m_1^{pad}|m_2^{pad}|\ldots|m_r^{pad}$.
  Let $t_0=0^n$. For $i=1,\ldots,r$, it computes $t_i=F_{k_1} \left( t_{i-1} \oplus m_i^{pad} \right)$.
  Mac outputs $F_{k_2}(t_r)$.
  
  
  (c) $Vrfy$ on input key $k_1,k_2 \in \lbrace 0,1 \rbrace^n$, a message $m \in \lbrace 0,1 \rbrace^*$ and tag $t \in \lbrace 0,1 \rbrace^n$ outputs $1$ if $Mac_{k_1,k_2}(m)=t$ and $0$ otherwise.


Now I have some exam from previous year, and I don't know at all how to prove this facts (and, it should be done in rigorous way).


  Consider the modification CBC-MAC' of the CBC-MAC where the algorithm $Mac'_{k_1,k_2}(m)$
  
  
  selects $t_0$ uniformly at random,
  computes $t_1, \ldots, t_r$ as in CBC-MAC,
  and outputs $\left( t_0,F_{k_2}(t_r) \right)$.
  
  
  The verification algorithm given tag $(t_0,s)$ performs the same computation as $Mac'_{k_1,k_2}(m)$ using the given value $t_0$ and outputs $1$ if $s=F_{k_2}(t_r)$ and $0$ otherwise.
  
  1) Prove that CBC-MAC' is not strongly existentially unforgeable under an adaptive chosen-message attack (definition is below this exercise).
  
  Consider the simplification CBC-MAC'' of the CBC-MAC where the algorithm $Mac''_{k_1,k_2}(m)$ outputs $t_r$ instead of $F_{k_2}(t_r)$.
  
  2) Prove that CBC-MAC'' is not strongly existentially unforgeable under an adaptive chosen-message attack.
  
  3) Is there a condition on the message space of CBC-MAC'' such that your proof does not hold? Explain your answer.


Reminder:


  An efficient MAC is strongly existentially unforgeable under an adaptive chosen-message attack if for all PPT adversaries $\mathcal{A}$ it holds that $Pr[MACforge_{\mathcal{A}}(n)=1]$ is negligible function, where $MACforge_{\mathcal{A}}(n)$ denotes the outcome of the following experiment:
  
  (a) A key $k \leftarrow Gen(1^n) \in \lbrace 0,1 \rbrace^n$ is generated.
  
  (b) The adversary $\mathcal{A}$ is given oracle access to $Mac_k(\cdot)$ and outputs a pair $(m,t)$. Formally: $(m,t) \leftarrow \mathcal{A}^{Mac_k(\cdot)}(1^n)$. Let $Q$ denote the set of query/response-pairs $(m',t')$ for all the queries $m'$ asked by $\mathcal{A}$ during its execution.
  
  (c) The output of the experiment is $1$ if and only if $(m,t) \not\in Q$ and $Vrfy_k(m,t)=1$.


If you could help me with the rigorous proof, I'd be really grateful for your time.

Thanks, Ben.
1) The adversary queries the oracle (with some randomly chosen message $m$) and gets as a result a message $m=m_1|m_2|...$ and its tag $t=(t_0,F_{k_2}(t_r))$. She then draws $\rho$ uniformly at random in $\{0,1\}^n$ and outputs the message $m=\rho\oplus m_1|m_2|...$ and its (valid) tag $t=(\rho\oplus t_0,F_{k_2}(t_r))$.

2) The adversary queries the oracle (with some randomly chosen message $M$) and gets as a result the padded message $M|1|0^l$ and its tag $t=t_r$. She then queries the oracle with the message $t_r$ and gets the corresponding tag $T$.  She eventually outputs the (unpadded) message $M|1|0^l|0^n$ and its valid tag $T$.

3) The message space consists of the set of $\{\mbox{bit_length}(S)|S\}$ where S runs through all possible bit strings of length less than $2^n$.