diff --git a/proofs/KeyEncapsulationMechanisms.eca b/proofs/KeyEncapsulationMechanisms.eca
index 294e9b2..ffba4fc 100644
--- a/proofs/KeyEncapsulationMechanisms.eca
+++ b/proofs/KeyEncapsulationMechanisms.eca
@@ -74,7 +74,7 @@ module Correctness (S : Scheme) = {
   non-adaptive Chosen-Ciphertext Attacks (CCA1)
   The adversary is given the considered public key and access to a decryption oracle
   *before* the stage in which it is expected to distinguish/return a break.
-  Hence, the adversary is able to is able to produce encapsulations
+  Hence, the adversary is able to produce encapsulations
   *and* query for decryptions of chosen ciphertexts.
 *)
 (* Oracles *)
@@ -106,18 +106,26 @@ module O_CCA1_Default (S : Scheme) : Oracles_CCA1i = {
 }.
 
 (* 
-  adaptive Chosen-Ciphertext Attacks (CCA2) 
+  adaptive Chosen-Ciphertext Attacks (Traditional: CCA2, Modern : CCA)
   The adversary is given the considered public key and access to a decryption oracle throughout.  
   Hence, the adversary is able to produce encapsulations
   *and* query for decryptions of chosen ciphertexts (potentially barring ciphertexts
   that are part of the challenge).
+  Traditionally, this was analogous to CCA2 security for PKE schemes, meaning there were
+  two adversary stages: one before receiving the challenge (given a public key and access to a 
+  non-restricted decapsulation oracle), and one after receiving the challenge (given access to a
+  restricted decapsulation oracle, i.e., one that prohibited querying the challenge).
+  Over time, the formalization shifted toward only considering the second adversary stage 
+  (provding the public key(s) to this stage as well).
+  Here, we denote the traditional one by CCA2 (as we do for PKE schemes), and the modern one by CCA.
 *)
+(** Interface for oracles employed in CCA2 (CCA) security games **)
 module type Oracles_CCA2i = {
   proc init(sk_init : sk_t, c'_init : ctxt_t) : unit
   proc decaps(c : ctxt_t) : key_t option
 }.
 
-(** A default implementation for the oracles employed in (the second stage of) CCA2 security games **)
+(** A default implementation for the oracles employed in (the second stage of) CCA2 (CCA) security games **)
 module O_CCA2_Default (S : Scheme) : Oracles_CCA2i = {
   var sk : sk_t
   var c' : ctxt_t 
@@ -144,7 +152,10 @@ module O_CCA2_Default (S : Scheme) : Oracles_CCA2i = {
   }
 }.
 
-(** Interface for oracles given to the adversary in CCA security games **)
+(**
+  Interface for oracles given to the adversary in any CCA security games 
+  (i.e., CCA1, traditional CCA2, and modern CCA2) 
+**)
 module type Oracles_CCA = {
   include Oracles_CCA2i [-init]
 }.
@@ -218,8 +229,8 @@ module OW_CCA1 (S : Scheme, O : Oracles_CCA1i, A : Adv_OWCCA1) = {
 
 
 (*
-  One-Wayness under adaptive Chosen-Ciphertext Attacks (OW-CCA2).
-  In a CCA1 setting, the adversary is asked to produce the (symmetric) key
+  One-Wayness under (traditional) adaptive Chosen-Ciphertext Attacks (OW-CCA2).
+  In a (traditional) CCA2 setting, the adversary is asked to produce the (symmetric) key
   encapsulated by a given ciphertext.
 *)
 (** Adversary class considered for OW-CCA2 **)
@@ -251,6 +262,36 @@ module OW_CCA2 (S : Scheme, O1 : Oracles_CCA1i, O2 : Oracles_CCA2i, A : Adv_OWCC
 }.
 
 
+(*
+  One-Wayness under (modern) adaptive Chosen-Ciphertext Attacks (OW-CCA).
+  In a (modern) CCA2 setting, the adversary is asked to produce the (symmetric) key
+  encapsulated by a given ciphertext.
+*)
+(** Adversary class considered for OW-CCA (i.e., modern OW-CCA2) **)
+module type Adv_OWCCA (O : Oracles_CCA) = { 
+  proc find(pk : pk_t, c : ctxt_t) : key_t
+}.
+
+(** OW-CCA (i.e., modern OW-CCA2) security game **)
+module OW_CCA (S : Scheme, O : Oracles_CCA2i, A : Adv_OWCCA) = {
+  proc main() : bool = {
+    var pk : pk_t;
+    var sk : sk_t;
+    var k, k' : key_t;
+    var c : ctxt_t;
+    
+    (pk, sk) <@ S.keygen();
+    
+    (k, c) <@ S.encaps(pk);
+    O.init(sk, c);
+    
+    k' <@ A(O).find(pk, c);
+    
+    return k' = k; 
+  }
+}.
+
+
 (**
   (ciphertext) INDistinguishability (IND). 
   The adversary is asked to determine whether a given
@@ -379,8 +420,8 @@ module IND_CCA1_P (S : Scheme, O : Oracles_CCA1i, A : Adv_INDCCA1) = {
 
 
 (*
-  (ciphertext) INDistinguishability under adaptive Chosen-Ciphertext Attacks (IND-CCA2).
-  In a CCA2 setting, the adversary is asked to determine whether a given
+  (ciphertext) INDistinguishability under (traditional) adaptive Chosen-Ciphertext Attacks (IND-CCA2).
+  In a (traditional) CCA2 setting, the adversary is asked to determine whether a given
   (symmetric) key is (1) encapsulated by a given ciphertext or (2) independently
   sampled at random (from dkey).
 *)
@@ -440,6 +481,62 @@ module IND_CCA2_P (S : Scheme, O1 : Oracles_CCA1i, O2 : Oracles_CCA2i, A : Adv_I
   }
 }.
 
+
+(*
+  (ciphertext) INDistinguishability under (modern) adaptive Chosen-Ciphertext Attacks (IND-CCA2).
+  In a (modern) CCA2 setting, the adversary is asked to determine whether a given
+  (symmetric) key is (1) encapsulated by a given ciphertext or (2) independently
+  sampled at random (from dkey).
+*)
+(** Adversary class considered for IND-CCA (i.e., modern IND-CCA2) **)
+module type Adv_INDCCA (O : Oracles_CCA) = {
+  proc distinguish(pk : pk_t, k : key_t, c : ctxt_t) : bool
+}.
+
+(** IND-CCA (i.e., modern IND-CCA2) security game (sampled bit) **)
+module IND_CCA (S : Scheme, O : Oracles_CCA2i, A : Adv_INDCCA) = {
+  proc main() : bool = {
+    var pk : pk_t;
+    var sk : sk_t;
+    var b, b' : bool;
+    var k, k' : key_t;
+    var c : ctxt_t;
+    
+    (pk, sk) <@ S.keygen();
+    
+    (k, c) <@ S.encaps(pk);
+    k' <$ dkey;
+    O.init(sk, c);
+    
+    b <$ {0,1};
+    
+    b' <@ A(O).distinguish(pk, if b then k' else k, c);
+    
+    return b' = b; 
+  }
+}.
+
+(** IND-CCA (i.e., modern IND-CCA2) security game (provided bit) **)
+module IND_CCA_P (S : Scheme, O : Oracles_CCA2i, A : Adv_INDCCA) = {
+  proc main(b : bool) : bool = {
+    var pk : pk_t;
+    var sk : sk_t;
+    var b' : bool;
+    var k, k' : key_t;
+    var c : ctxt_t;
+    
+    (pk, sk) <@ S.keygen();
+    
+    (k, c) <@ S.encaps(pk);
+    k' <$ dkey;
+    O.init(sk, c);
+    
+    b' <@ A(O).distinguish(pk, if b then k' else k, c);
+    
+    return b' = b; 
+  }
+}.
+
 end IND.
 
 
@@ -779,8 +876,8 @@ module SNM_CCA1_P (S : Scheme, O : Oracles_CCA1i, A : Adv_SNMCCA1) = {
 
 
 (*
-  (ciphertext) Non-Malleability under adaptive Chosen-Ciphertext Attacks (NM-CCA2).
-  In a CCA2 setting, given a ciphertext (encapsulating some key K), the adversary is 
+  (ciphertext) Non-Malleability under (traditional) adaptive Chosen-Ciphertext Attacks (NM-CCA2).
+  In a (traditional) CCA2 setting, given a ciphertext (encapsulating some key K), the adversary is 
   asked to provide a relation R and a list of ciphertexts such that the (symmetric) keys 
   resulting from decapsulating the ciphertexts (in the list) are related (through R) with
   K (significantly) more often than with a (symmetric) key that is independently sampled
@@ -814,7 +911,7 @@ module NM_CCA2 (S : Scheme, O1 : Oracles_CCA1i, O2 : Oracles_CCA2i, A : Adv_NMCC
     k' <$ dkey;
     O2.init(sk, c);
     
-    (rel, cl) <@ A(O1).find(c);
+    (rel, cl) <@ A(O2).find(c);
     
     kol <- [];
     while (size kol < size cl) {
@@ -862,7 +959,7 @@ module NM_CCA2_P (S : Scheme, O1 : Oracles_CCA1i, O2 : Oracles_CCA2i, A : Adv_NM
 }.
 
 (*
-  (ciphertext) Strong Non-Malleability under adaptive Chosen-Ciphertext Attacks (SNM-CCA2).
+  (ciphertext) Strong Non-Malleability under (traditional) adaptive Chosen-Ciphertext Attacks (SNM-CCA2).
   As NM-CCA2, but the adversary is additionally given a pair of (symmetric) keys of
   which one is independently sampled at random, and the other is the one
   encapsulated by the given ciphertext. (The order in which they appear in the pair
@@ -946,6 +1043,161 @@ module SNM_CCA2_P (S : Scheme, O1 : Oracles_CCA1i, O2 : Oracles_CCA2i, A : Adv_S
   }
 }.
 
+
+(*
+  (ciphertext) Non-Malleability under (modern) adaptive Chosen-Ciphertext Attacks (NM-CCA).
+  In a (modern) CCA2 setting, given a ciphertext (encapsulating some key K), the adversary is 
+  asked to provide a relation R and a list of ciphertexts such that the (symmetric) keys 
+  resulting from decapsulating the ciphertexts (in the list) are related (through R) with
+  K (significantly) more often than with a (symmetric) key that is independently sampled
+  at random.
+*)
+(** Adversary class considered for NM-CCA (i.e., modern NM-CCA2) **)
+module type Adv_NMCCA (O : Oracles_CCA) = {
+  proc find(pk : pk_t, c : ctxt_t) : (key_t -> key_t option list -> bool) * ctxt_t list
+}.
+
+(** NM-CCA (i.e., modern NM-CCA2) security game (sampled bit) **)
+module NM_CCA (S : Scheme, O : Oracles_CCA2i, A : Adv_NMCCA) = {
+  proc main() = {
+    var pk : pk_t;
+    var sk : sk_t;
+    var k, k' : key_t;
+    var c : ctxt_t;
+    var rel : key_t -> key_t option list -> bool;
+    var cl : ctxt_t list;
+    var ko : key_t option;
+    var kol : key_t option list;
+    var b : bool;
+    
+    (pk, sk) <@ S.keygen();
+    
+    (k, c) <@ S.encaps(pk);
+    k' <$ dkey;
+    O.init(sk, c);
+    
+    (rel, cl) <@ A(O).find(pk, c);
+    
+    kol <- [];
+    while (size kol < size cl) {
+      ko <@ S.decaps(sk, nth witness cl (size kol));
+      kol <- rcons kol ko;
+    }
+    
+    b <$ {0,1};
+    
+    return !(c \in cl) /\ rel (if b then k' else k) kol;
+  }
+}.
+
+(** NM-CCA (i.e., modern NM-CCA2) security game (provided bit) **)
+module NM_CCA_P (S : Scheme, O : Oracles_CCA2i, A : Adv_NMCCA) = {
+  proc main(b : bool) = {
+    var pk : pk_t;
+    var sk : sk_t;
+    var k, k' : key_t;
+    var c : ctxt_t;
+    var rel : key_t -> key_t option list -> bool;
+    var cl : ctxt_t list;
+    var ko : key_t option;
+    var kol : key_t option list;
+        
+    (pk, sk) <@ S.keygen();
+    
+    (k, c) <@ S.encaps(pk);
+    k' <$ dkey;
+    O.init(sk, c);
+    
+    (rel, cl) <@ A(O).find(pk, c);
+    
+    kol <- [];
+    while (size kol < size cl) {
+      ko <@ S.decaps(sk, nth witness cl (size kol));
+      kol <- rcons kol ko;
+    }
+    
+    return !(c \in cl) /\ rel (if b then k' else k) kol;
+  }
+}.
+
+(*
+  (ciphertext) Strong Non-Malleability under (modern) adaptive Chosen-Ciphertext Attacks (SNM-CCA).
+  As NM-CCA, but the adversary is additionally given a pair of (symmetric) keys of
+  which one is independently sampled at random, and the other is the one
+  encapsulated by the given ciphertext. (The order in which they appear in the pair
+  is (uniformly) random).
+*)
+(** Adversary class considered for SNM-CCA (i.e., modern SNM-CCA2) **)
+module type Adv_SNMCCA (O : Oracles_CCA) = {
+  proc find(pk : pk_t, c : ctxt_t, kk : key_t * key_t) : (key_t -> key_t option list -> bool) * ctxt_t list
+}.
+
+(** SNM-CCA (i.e., modern SNM-CCA2) security game **)
+module SNM_CCA (S : Scheme, O : Oracles_CCA2i, A : Adv_SNMCCA) = {
+  proc main() = {
+    var pk : pk_t;
+    var sk : sk_t;
+    var k, k' : key_t;
+    var c : ctxt_t;
+    var rel : key_t -> key_t option list -> bool;
+    var cl : ctxt_t list;
+    var ko : key_t option;
+    var kol : key_t option list;
+    var b, o : bool;
+    
+    (pk, sk) <@ S.keygen();
+    
+    (k, c) <@ S.encaps(pk);
+    k' <$ dkey;
+    O.init(sk, c);
+
+    o <$ {0,1};
+    (rel, cl) <@ A(O).find(pk, c, if o then (k', k) else (k, k'));
+    
+    kol <- [];
+    while (size kol < size cl) {
+      ko <@ S.decaps(sk, nth witness cl (size kol));
+      kol <- rcons kol ko;
+    }
+    
+    b <$ {0,1};
+    
+    return !(c \in cl) /\ rel (if b then k' else k) kol;
+  }
+}.
+
+(** SNM-CCA (i.e., modern SNM-CCA2) security game **)
+module SNM_CCA_P (S : Scheme, O : Oracles_CCA2i, A : Adv_SNMCCA) = {
+  proc main(b : bool) = {
+    var pk : pk_t;
+    var sk : sk_t;
+    var k, k' : key_t;
+    var c : ctxt_t;
+    var rel : key_t -> key_t option list -> bool;
+    var cl : ctxt_t list;
+    var ko : key_t option;
+    var kol : key_t option list;
+    var o : bool;
+    
+    (pk, sk) <@ S.keygen();
+    
+    (k, c) <@ S.encaps(pk);
+    k' <$ dkey;
+    O.init(sk, c);
+
+    o <$ {0,1};
+    (rel, cl) <@ A(O).find(pk, c, if o then (k', k) else (k, k'));
+    
+    kol <- [];
+    while (size kol < size cl) {
+      ko <@ S.decaps(sk, nth witness cl (size kol));
+      kol <- rcons kol ko;
+    }
+    
+    return !(c \in cl) /\ rel (if b then k' else k) kol;
+  }
+}.
+
 end NM.
 
 
@@ -1070,11 +1322,11 @@ module ANO_CCA1_P (S : Scheme, O0 : Oracles_CCA1i, O1 : Oracles_CCA1i, A : Adv_A
 }.
 
 
-
 (*
-  ANOnymity under adaptive Chosen-Plaintext attack (ANO-CCA2).
-  In a CCA2 setting, the adversary is given (in the first stage) two (honestly generated) public keys 
-  and (in the second stage) an encapsulation (i.e., key/ciphertext pair), and is 
+  ANOnymity under (traditional) adaptive Chosen-Plaintext attack (ANO-CCA2).
+  In a (traditional) CCA2 setting, the adversary is given (in the first stage) two 
+  (honestly generated) public keys and (in the second stage) an encapsulation 
+  (i.e., key/ciphertext pair), and is 
   asked to determine which public key was used to create the encapsulation.
 *)
 (** Adversary class considerd for ANO-CCA2 **)
@@ -1114,7 +1366,7 @@ module ANO_CCA2 (S : Scheme)
   }
 }.
 
-(** ANO-CCA2 security game (sampled bit) **)
+(** ANO-CCA2 security game (provided bit) **)
 module ANO_CCA2_P (S : Scheme)
                   (O01 : Oracles_CCA1i, O11 : Oracles_CCA1i)
                   (O02 : Oracles_CCA2i, O12 : Oracles_CCA2i)
@@ -1144,6 +1396,69 @@ module ANO_CCA2_P (S : Scheme)
 }.
 
 
+(*
+  ANOnymity under (modern) adaptive Chosen-Plaintext attack (ANO-CCA).
+  In a (modern) CCA setting, the adversary is given (in the first stage) two 
+  (honestly generated) public keys and (in the second stage) an encapsulation 
+  (i.e., key/ciphertext pair), and is 
+  asked to determine which public key was used to create the encapsulation.
+*)
+(** Adversary class considerd for ANO-CCA (i.e., modern ANO-CCA2) **)
+module type Adv_ANOCCA (O0 : Oracles_CCA, O1 : Oracles_CCA) = {
+  proc distinguish(pk0 : pk_t, pk1 : pk_t, kc : key_t * ctxt_t) : bool
+}.
+
+(** ANO-CCA (i.e., modern ANO-CCA2) security game (sampled bit) **)
+module ANO_CCA (S : Scheme)
+               (O0 : Oracles_CCA2i, O1 : Oracles_CCA2i)
+               (A : Adv_ANOCCA) = {
+  proc main() = {
+    var pk0, pk1 : pk_t;
+    var sk0, sk1 : sk_t;
+    var b, b' : bool;
+    var k : key_t;
+    var c : ctxt_t;
+    
+    (pk0, sk0) <@ S.keygen();
+    (pk1, sk1) <@ S.keygen();
+    
+    b <$ {0,1};
+    
+    (k, c) <@ S.encaps(if b then pk1 else pk0);
+    O0.init(sk0, c);
+    O1.init(sk1, c);
+    
+    b' <@ A(O0, O1).distinguish(pk0, pk1, (k, c));
+    
+    return b' = b;
+  }
+}.
+
+(** ANO-CCA (i.e., modern ANO-CCA2) security game (provided bit) **)
+module ANO_CCA_P (S : Scheme)
+                 (O0 : Oracles_CCA2i, O1 : Oracles_CCA2i)
+                 (A : Adv_ANOCCA) = {
+  proc main(b : bool) = {
+    var pk0, pk1 : pk_t;
+    var sk0, sk1 : sk_t;
+    var b' : bool;
+    var k : key_t;
+    var c : ctxt_t;
+    
+    (pk0, sk0) <@ S.keygen();
+    (pk1, sk1) <@ S.keygen();
+    
+    (k, c) <@ S.encaps(if b then pk1 else pk0);
+    O0.init(sk0, c);
+    O1.init(sk1, c);
+    
+    b' <@ A(O0, O1).distinguish(pk0, pk1, (k, c));
+    
+    return b' = b;
+  }
+}.
+
+
 (*
   BINDing (BIND).
   Intuitively, binding properties capture to which extent certain artifacts (in a