fix: crypto typechecking

tnelson · Feb 21, 2025 · 580e068 · 580e068
1 parent 4e859b8
commit 580e068
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 4 deletions.
diff --git a/forge/domains/crypto/base.frg b/forge/domains/crypto/base.frg
@@ -44,11 +44,13 @@ fun getLTK[name_a: name, name_b: name]: lone skey {
   (KeyPairs.ltks)[name_a][name_b]
 }
 
-/** Get the inverse key for a given key (if any) */
+/** Get the inverse key for a given key (if any). The structure of this predicate 
+    is due to Forge's typechecking as of January 2025. The (none & Key) is a workaround
+    to give Key type to none, which has univ type by default.  */
 fun getInv[k: Key]: one Key {
   (k in PublicKey => ((KeyPairs.pairs).k) else (k.(KeyPairs.pairs)))
   +
-  (k in skey => k else none)
+  (k in skey => k else (none & Key))
 }
 
 

diff --git a/forge/domains/crypto/examples/ns.frg b/forge/domains/crypto/examples/ns.frg
@@ -19,7 +19,7 @@ pred attack_exists {
 // Proxy for the concrete attack, used to debug and check the model:
 //   some message is sent encrypted with the attacker's public key
 pred proxy_shape {
-    some m: Message | {
+    some m: mesg | {
         // getInv[m.data.encryptionKey] in (KeyPairs.owners.Attacker)
         getInv[m.data.encryptionKey] in (KeyPairs.owners.(ns_init.agent))
     }

diff --git a/forge/domains/crypto/examples/ns_fixed.frg b/forge/domains/crypto/examples/ns_fixed.frg
@@ -22,7 +22,7 @@ pred attack_exists {
 // Proxy for the concrete attack, used to debug and check the model:
 //   some message is sent encrypted with the attacker's public key
 pred proxy_shape {
-    some m: Message | {
+    some m: mesg | {
         // getInv[m.data.encryptionKey] in (KeyPairs.owners.Attacker)
         getInv[m.data.encryptionKey] in (KeyPairs.owners.(ns_init.agent))
     }