Add notes.

sandbox-quantum · Jan 9, 2025 · c7d5396 · c7d5396
1 parent 8cb63a5
commit c7d5396
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 1 deletion.
diff --git a/Notes.txt b/Notes.txt
@@ -1,3 +1,14 @@
+ML-KEM Binding propertiers to prove:
+- BIND-K-X are big ones
+- BIND-K,PK-CT?
+- BIND-K,CT-PK?
+
+
+RSA-KEM/'RSASVE' used in protocol vulnerable to binding-related attack (https://csrc.nist.gov/pubs/sp/800/227/ipd), show lack of binding properties?
+- See also: https://nvlpubs.nist.gov/nistpubs/SpecialPublications/NIST.SP.800-56Br2.pdf
+
+
+
 (Comments on) Changes to KeyEncapsulationMechanisms[ROM].eca:
 > For the oracle module types, stick with functor types for now.
   Seems to be the most reasonable option with current features.

diff --git a/formosa-mlkem b/formosa-mlkem
+4 −4		easycrypt.project
+9 −6		proof/security/FO_MLKEM.ec
+5 −7		proof/security/FO_TT.ec
+4 −4		proof/security/FO_UU.ec
+7 −7		proof/security/MLWE.ec
+6 −4		proof/security/MLWE_PKE.ec
+1 −1		proof/security/MLWE_PKE_Basic.ec
+1 −1		proof/security/MLWE_PKE_Hash.ec