diff --git a/etc/theory/compression_security.tex b/etc/theory/compression_security.tex
index 2302e2aa..3111663e 100644
--- a/etc/theory/compression_security.tex
+++ b/etc/theory/compression_security.tex
@@ -21,7 +21,7 @@
 \newcommand\defeq{\stackrel{\mathclap{\normalfont\mbox{def}}}{=}}
 
 \begin{document}
-\title{On the (in)security of encryption over compression in TLS} % TODO: replace with your title
+\title{On the (in)security of encryption over compression in TLS}
 
 \input{sections/abstract.tex}
 
@@ -37,7 +37,7 @@
 
 \ccsdesc[500]{Security and privacy~Web application security}
 
-\keywords{compression, BREACH, CRIME, web security, defense, reflection security} % TODO: replace with your keywords
+\keywords{compression, BREACH, CRIME, web security, defense, reflection security}
 
 \maketitle
 
diff --git a/etc/theory/sections/reflection_security.tex b/etc/theory/sections/reflection_security.tex
index 20064f1d..e12bfb66 100644
--- a/etc/theory/sections/reflection_security.tex
+++ b/etc/theory/sections/reflection_security.tex
@@ -8,14 +8,20 @@ \section{Reflection security}\label{sec:refsec}
 
 \subsection{The reflection game}\label{subsec:refsecgame}
 
-Let $\mathcal{SE} = (Gen, \mathcal{E}, \mathcal{D})$ be a private-key encryption
-scheme, $\mathcal{A}$ be an adversary and $\mathcal{S}$ be a simulator. Also let
-some function $f(\cdot, \cdot)$, some function
-$g$ of the plaintext, some function $Com(\cdot)$, and a distribution of secrets
-$\mathcal{M}$. We call $f$ a rendering function and require that it
-is polynomially computable and reversible. We call $Com$ the compression
-function and require that it is a deterministic polynomially computable and
-reversible bijection.
+Let $\mathcal{T} = (Gen, K, \mathcal{D})$ be a triplet of algorithms. In this
+triplet, $Gen$ is a key generation algorithm which, given a security parameter
+$1^\lambda$ returns some key $\kappa$. The function $K$ is an encryption
+function with three parameters: The key $\kappa$ and two plaintexts $s$ and $r$,
+which we call the \textit{secret} and \textit{reflection} specifically. For now,
+we leave the question of how these plaintexts are combined to be encrypted
+together undefined; this will be instantiated into a concrete function when we
+discuss the security of particular schemes.
+
+Let $\mathcal{A}$ be an adversary and $\mathcal{S}$ be a simulator. Also let
+$\mathcal{M}$ be a distribution of plaintexts and $g$ a function defined on its
+support, as well as some function $Com(\cdot)$ defined on the domain of $K$. We
+call $Com$ the compression function and require that it is a deterministic
+polynomially computable and reversible bijection.
 
 The game $\text{Game}_{\text{REF-SEC}}^{\mathcal{SE},\mathcal{A}}(\lambda)$ is
 parameterized with the security parameter $\lambda$. The challenger produces a
@@ -25,9 +31,8 @@ \subsection{The reflection game}\label{subsec:refsecgame}
 The adversary is then allowed to run and make arbitrary calls to a reflection
 oracle. The oracle is parameterized by $s$, the secret unknown to the adversary.
 For the reflection oracle call, the adversary chooses a reflection string $r$
-and sends it to the oracle. The oracle computes $m = f(s, r)$. Subsequently $m$
-is encrypted as $c = \mathcal{E}_\kappa(m)$, and $c$ is sent back to the
-adversary.
+and sends it to the oracle. The oracle computes $c = K_\kappa(s, r)$.
+Subsequently $c$ is sent back to the adversary.
 
 When the adversary decides to complete the game, they output a guess $y$. The
 adversary is successful if $g(s) = y$. In the case of Rupture, a successful
@@ -51,8 +56,7 @@ \subsection{The reflection game}\label{subsec:refsecgame}
 
 \begin{lstlisting}[texcl,mathescape,basicstyle=\small]
 def $\text{Reflect}^{k}_s(r)$:
-    $m = f(s, r)$
-    $c \leftarrow \mathcal{E}_{k}(m)$
+    $c \leftarrow K_{k}(s, r)$
     return $c$
 \end{lstlisting}
 
@@ -62,7 +66,7 @@ \subsection{The reflection game}\label{subsec:refsecgame}
 def $\text{Game}_{\text{REF-SIM}}^{\mathcal{SE},\mathcal{S}}(\lambda)$:
     $s \leftarrow \mathcal{M}$
     $s' = 0^{|s|}$
-    $y \leftarrow \mathcal{S}^{\text{Reflect}^{k}_s(r)}(1^\lambda, {|Com(s)|})$
+    $y \leftarrow \mathcal{S}^{\text{Reflect}^{k}_{s'}(r)}(1^\lambda, {|Com(s)|})$
     if $y = g(s)$:
         return 1
     else:
@@ -73,8 +77,7 @@ \subsection{The reflection game}\label{subsec:refsecgame}
 
 \begin{lstlisting}[texcl,mathescape,basicstyle=\small]
 def $\text{Reflect}^{k}_{s'}(r)$:
-    $m = f(s', r)$
-    $c \leftarrow \mathcal{E}_{k}(m)$
+    $c \leftarrow \mathcal{K}_{k}(s', r)$
     return $c$
 \end{lstlisting}
 
@@ -101,8 +104,9 @@ \subsection{Adversarial advantage}\label{subsec:refsecadv}
 
 \subsection{Adaptive reflection security}\label{subsec:adaptiverefsec}
 
-Given a rendering function $f(\cdot, \cdot)$, a private-key encryption
-scheme $\mathcal{SE}$ is \textit{reflection-secure} if:
+Given a rendering function $f(\cdot, \cdot)$, a private-key encryption scheme
+$\mathcal{SE}$ composed with a rendering function $f$ is
+\textit{reflection-secure} if:
 \begin{align*}
     \forall \mathcal{M}:
     \forall g:
@@ -112,7 +116,7 @@ \subsection{Adaptive reflection security}\label{subsec:adaptiverefsec}
 \end{align*}
 
 \begin{lemma}[Semantic security]
-    Let $(Gen, K, D)$ be a length-preserving reflection-secure encryption
+    Let $(Gen, E, D)$ be a length-preserving reflection-secure encryption
     scheme. Then it is also semantically secure.
 \end{lemma}
 
diff --git a/etc/theory/sections/security_of_compression.tex b/etc/theory/sections/security_of_compression.tex
index 20d04662..00b1ef0c 100644
--- a/etc/theory/sections/security_of_compression.tex
+++ b/etc/theory/sections/security_of_compression.tex
@@ -197,7 +197,7 @@ \subsection{Good compression allows predicate detection}
 
 We now move on to show that all good compression functions exhibit
 compression-detectability of some predicate. In intuitive terms, this means
-that if a compression function compresses well enough, it will necessarilly
+that if a compression function compresses well enough, it will necessarily
 allow one part of the plaintext to affect how another part of the plaintext
 compresses. An attacker that is able to measure how well a string compresses
 can use this to detect a predicate on the second part of the plaintext by