This is done solely for the purpose of clear comparison of the real and the ideal cases, and does not affect the results of the security evaluation. Now, having set the stage, we can state our main theorem.

(0,-3) node\[draw,minimum width=6.5cm\] (z) [${\mathcal{Z}}$]{}; (-2.6,0) node\[fill=black!10,minimum width=2cm,minimum height=.8cm\]; (2.6,0) node\[fill=black!10,minimum width=2cm,minimum height=.8cm\]; (-3,0) node\[draw,minimum width=1cm,fill=white\](a) [Alice]{}; (3,0)node\[draw,minimum width=1cm,fill=white\](b) [Bob]{}; (0,-1.5)node\[draw,minimum width=3cm\](s) [${\mathcal{S}}$]{}; (0, 0)node\[draw,minimum width=3cm,fill=white\](f) [${\mathcal{F}}$]{}; (-2.8, -1.5)node\[draw,rounded rectangle, minimum width=1.3cm\](k) [Key]{}; (z.west) to\[bend left=40\] node\[right\][$m$]{} (a.west); (a) to node\[above\][$m$]{} (f); (k) to node\[above\][$k$]{} (s); ($(f.south)+(-1,0)$) to node\[left\][$m$]{} ($(s.north)+(-1,0)$); ($(s.south)+(-1,0)$) to node\[left\][$(m,t)$]{} ($(z.north)+(-1,0)$); ($(z.north)+(1,0)$) to node\[right\][$(m',t')$]{} ($(s.south)+(1,0)$); ($(s.north)+(1,0)$) to node\[right\][$m'$]{} ($(f.south)+(1,0)$); (f) to node\[above\][$m,\bot$]{} (b); (b.east) to\[bend left=40\] node\[left\] [$m',\bot$]{} (z.east);

(0,-3) node\[draw,minimum width=6cm\] (z) [${\mathcal{Z}}$]{}; (-2,0) node\[fill=black!10,minimum width=3cm,minimum height=.8cm\]; (2,0) node\[fill=black!10,minimum width=3.1cm,minimum height=.8cm\]; (-3,0) node\[draw,minimum width=1cm,fill=white\](a) [Alice]{}; (3,0)node\[draw,minimum width=1cm,fill=white\](b) [Bob]{}; (0,-1.5)node\[draw,minimum width=3cm\](e) [${\mathcal{A}}$]{}; (0, 1)node\[draw,rounded rectangle, minimum width=1.3cm\](k) [Key]{}; (-1,0)node\[draw,rectangle,minimum width=1cm,fill=white\](T) [TAG]{}; (1,0)node\[draw,rectangle,minimum width=1cm,fill=white\](V) [VRFY]{}; (0,.5) node\[draw,dotted,minimum width=3cm,minimum height=1.7cm\] +(1.2,.75)node[WCA]{}; (z.west) to\[bend left=40\] node\[right\][$m$]{} (a.west); (a) to node\[above\][$m$]{} (T); (T.south) to node\[left\][$(m,t)$]{} ($(e.north)+(-1,0)$); ($(e.south)+(-1,0)$) to node\[left\][$(m,t)$]{} ($(z.north)+(-1,0)$); ($(z.north)+(1,0)$) to node\[right\][$(m',t')$]{} ($(e.south)+(1,0)$); ($(e.north)+(1,0)$) to node\[right\][$(m',t')$]{} (V.south); (V) to node\[above\][$m',\bot$]{} (b); (b.east) to\[bend left=40\] node\[left\] [$m',\bot$]{} (z.east); (k.south) to node\[above right,at end\][$k$]{} (T.north); (k.south) to node\[above left,at end\][$k$]{} (V.north);

\[thm-WCA-uc\] *(Indistinguishability)* No 