Tweaks to kerberos

secure-foundations · Apr 14, 2023 · dea44c9 · dea44c9
1 parent d2f5be1
commit dea44c9
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 2 deletions.
diff --git a/src/Typing.hs b/src/Typing.hs
@@ -1521,7 +1521,7 @@ checkExpr ot e = do
         (_, b) <- SMT.smtTypingQuery $ SMT.symAssert $ mkSpanned PFalse
         if b then getOutTy ot tAdmit else checkExpr ot e
       (ECorrCase n e) -> do
-          _ <- local (set tcScope Ghost) $ getNameType n
+          _ <- local (set tcScope Ghost) $ getNameTypeOpt n
           x <- freshVar
           t1 <- withVars [(s2n x, (ignore x, tLemma (pFlow (nameLbl n) advLbl)))] $ do
               (_, b) <- SMT.smtTypingQuery $ SMT.symAssert $ mkSpanned PFalse

diff --git a/tests/success/kerberos/kerberos.owli b/tests/success/kerberos/kerberos.owli
@@ -97,5 +97,7 @@ struct client_to_service_msg {
 name K // : enckey Name(AK) @ authserver
 
 def client_kerberos (ak: if sec(K) then Name(AK) else Data<adv>, tgt : Data<adv>
-|cipherlen(|enckey|)|, username : Data<adv> ||nonce||) @ client : Unit
+|cipherlen(|enckey|)|, username : Data<adv> ||nonce||) @ client 
+    requires [AK] <= [K]
+: Unit
 
diff --git a/tests/success/kerberos/kerberos_2_3.owl b/tests/success/kerberos/kerberos_2_3.owl
@@ -43,6 +43,7 @@ def service_main () @ service
 // called by the respective client_main() functions for the two versions of kerberos
 def client_kerberos (ak: if sec(K) then Name(AK) else Data<adv>, tgt : Data<adv>
 |cipherlen(|enckey|)|, username : Data<adv> ||nonce||) @ client
+    requires [AK] <= [K]
     : Unit = 
     corr_case AK in
     corr_case K in