diff --git a/README.md b/README.md
index 65f21a4..a923765 100644
--- a/README.md
+++ b/README.md
@@ -5,7 +5,7 @@ The material in this directory is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 
 
 ## Preliminaries
diff --git a/common.dhkem.ocvl b/common.dhkem.ocvl
index c319cf6..ae19d6f 100644
--- a/common.dhkem.ocvl
+++ b/common.dhkem.ocvl
@@ -7,7 +7,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 
diff --git a/common.hpke.ocvl b/common.hpke.ocvl
index 01eebe7..a90f970 100644
--- a/common.hpke.ocvl
+++ b/common.hpke.ocvl
@@ -7,7 +7,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 type key_t [large,fixed].
diff --git a/dhkem.auth.insider-cca-lr.m4.ocv b/dhkem.auth.insider-cca-lr.m4.ocv
index 66c92f1..c322c21 100644
--- a/dhkem.auth.insider-cca-lr.m4.ocv
+++ b/dhkem.auth.insider-cca-lr.m4.ocv
@@ -7,7 +7,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 proof {
diff --git a/dhkem.auth.insider-cca-lr.ocv b/dhkem.auth.insider-cca-lr.ocv
index 61653f5..325d497 100644
--- a/dhkem.auth.insider-cca-lr.ocv
+++ b/dhkem.auth.insider-cca-lr.ocv
@@ -7,7 +7,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 proof {
@@ -127,7 +127,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 
diff --git a/dhkem.auth.outsider-auth-lr.m4.ocv b/dhkem.auth.outsider-auth-lr.m4.ocv
index e10896c..f3ce850 100644
--- a/dhkem.auth.outsider-auth-lr.m4.ocv
+++ b/dhkem.auth.outsider-auth-lr.m4.ocv
@@ -7,7 +7,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 proof {
diff --git a/dhkem.auth.outsider-auth-lr.ocv b/dhkem.auth.outsider-auth-lr.ocv
index f4afb04..5e34eed 100644
--- a/dhkem.auth.outsider-auth-lr.ocv
+++ b/dhkem.auth.outsider-auth-lr.ocv
@@ -7,7 +7,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 proof {
@@ -153,7 +153,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 
diff --git a/dhkem.auth.outsider-cca-lr.m4.ocv b/dhkem.auth.outsider-cca-lr.m4.ocv
index ed72ea2..596f98f 100644
--- a/dhkem.auth.outsider-cca-lr.m4.ocv
+++ b/dhkem.auth.outsider-cca-lr.m4.ocv
@@ -7,7 +7,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 proof {
diff --git a/dhkem.auth.outsider-cca-lr.ocv b/dhkem.auth.outsider-cca-lr.ocv
index e3b3d88..b8ac765 100644
--- a/dhkem.auth.outsider-cca-lr.ocv
+++ b/dhkem.auth.outsider-cca-lr.ocv
@@ -7,7 +7,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 proof {
@@ -112,7 +112,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 
diff --git a/hpke.auth.insider-cca.m4.ocv b/hpke.auth.insider-cca.m4.ocv
index 188d096..02ea2b6 100644
--- a/hpke.auth.insider-cca.m4.ocv
+++ b/hpke.auth.insider-cca.m4.ocv
@@ -7,7 +7,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 proof {
diff --git a/hpke.auth.insider-cca.ocv b/hpke.auth.insider-cca.ocv
index c43fb69..7e9f785 100644
--- a/hpke.auth.insider-cca.ocv
+++ b/hpke.auth.insider-cca.ocv
@@ -7,7 +7,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 proof {
@@ -52,7 +52,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 type key_t [large,fixed].
diff --git a/hpke.auth.outsider-auth.m4.ocv b/hpke.auth.outsider-auth.m4.ocv
index e63bec2..7321404 100644
--- a/hpke.auth.outsider-auth.m4.ocv
+++ b/hpke.auth.outsider-auth.m4.ocv
@@ -7,7 +7,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 proof {
diff --git a/hpke.auth.outsider-auth.ocv b/hpke.auth.outsider-auth.ocv
index de699a1..ab2619d 100644
--- a/hpke.auth.outsider-auth.ocv
+++ b/hpke.auth.outsider-auth.ocv
@@ -7,7 +7,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 proof {
@@ -58,7 +58,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 type key_t [large,fixed].
diff --git a/hpke.auth.outsider-cca.m4.ocv b/hpke.auth.outsider-cca.m4.ocv
index 39e9eb2..699df87 100644
--- a/hpke.auth.outsider-cca.m4.ocv
+++ b/hpke.auth.outsider-cca.m4.ocv
@@ -7,7 +7,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 proof {
diff --git a/hpke.auth.outsider-cca.ocv b/hpke.auth.outsider-cca.ocv
index 1ca402c..460c181 100644
--- a/hpke.auth.outsider-cca.ocv
+++ b/hpke.auth.outsider-cca.ocv
@@ -7,7 +7,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 proof {
@@ -55,7 +55,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 type key_t [large,fixed].
diff --git a/keyschedule.auth.prf.ocv b/keyschedule.auth.prf.ocv
index e3e6b8e..77c6d79 100644
--- a/keyschedule.auth.prf.ocv
+++ b/keyschedule.auth.prf.ocv
@@ -7,7 +7,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 (* This type denotes the two-byte indication of length used
diff --git a/lib.aead.ocvl b/lib.aead.ocvl
index 7da725b..2753e3b 100644
--- a/lib.aead.ocvl
+++ b/lib.aead.ocvl
@@ -7,7 +7,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 (* AEAD (authenticated encryption with additional data) with a random nonce.
diff --git a/lib.authkem.ocvl b/lib.authkem.ocvl
index 0e34ff2..e336162 100644
--- a/lib.authkem.ocvl
+++ b/lib.authkem.ocvl
@@ -7,7 +7,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 (* The following macros define security properties of AKEM, which
diff --git a/lib.choice.ocvl b/lib.choice.ocvl
index dbb7c89..3556f6e 100644
--- a/lib.choice.ocvl
+++ b/lib.choice.ocvl
@@ -7,7 +7,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 def boolean_choice(value_t, test) {
diff --git a/lib.gdh.ocvl b/lib.gdh.ocvl
index 582f7cc..7dfd55c 100644
--- a/lib.gdh.ocvl
+++ b/lib.gdh.ocvl
@@ -7,7 +7,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 (* DH_proba_collision_minimal says that 
diff --git a/lib.ocvl b/lib.ocvl
index af60fa2..652bc90 100644
--- a/lib.ocvl
+++ b/lib.ocvl
@@ -8575,7 +8575,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 (* The types input_t and output_t MUST be fixed. *)
@@ -8604,7 +8604,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 def OptionType_1(option, option_Some, option_None, input) {
@@ -8631,7 +8631,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 def boolean_choice(value_t, test) {
@@ -8666,7 +8666,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 (* DH_proba_collision_minimal says that 
@@ -8818,7 +8818,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 (* The following macros define security properties of AKEM, which
@@ -9080,7 +9080,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 (* AEAD (authenticated encryption with additional data) with a random nonce.
@@ -9186,7 +9186,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 (* Pseudo random function (PRF) 
diff --git a/lib.option.ocvl b/lib.option.ocvl
index bb16d4d..60acbd3 100644
--- a/lib.option.ocvl
+++ b/lib.option.ocvl
@@ -7,7 +7,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 def OptionType_1(option, option_Some, option_None, input) {
diff --git a/lib.prf.ocvl b/lib.prf.ocvl
index 5343fdf..95a1ad0 100644
--- a/lib.prf.ocvl
+++ b/lib.prf.ocvl
@@ -7,7 +7,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 (* Pseudo random function (PRF) 
diff --git a/lib.truncate.ocvl b/lib.truncate.ocvl
index a259551..1b1a983 100644
--- a/lib.truncate.ocvl
+++ b/lib.truncate.ocvl
@@ -7,7 +7,7 @@ This is supplementary material accompanying the paper:
 Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
 and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
 Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
-Computer Science, Zagreb, Croatia, October 2021. Springer. To appear.
+Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
 Long version: https://eprint.iacr.org/2020/1499 *)
 
 (* The types input_t and output_t MUST be fixed. *)