Addressing PR comments, and adding explainations for AESEncryption ha…

…ndles authentication tags
aws · Oct 4, 2019 · c3a39bb · c3a39bb
1 parent e00db9f
commit c3a39bb
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 7 deletions.
diff --git a/src/Crypto/AESEncryption.dfy b/src/Crypto/AESEncryption.dfy
@@ -14,14 +14,16 @@ module {:extern "AESEncryption"} AESEncryption {
   export
     provides AESDecrypt, AESEncrypt, AESUtils, StandardLibrary, UInt
 
-  //FIXME: Ensure that these methods correctly handle authenticaition tags, see #36
+  //Note: AESDecrypt expects the message authentication tag (also known as MAC) to be present as the last n bytes of ctxt.
+  //      n = params.tagLen
   method AESDecrypt(params: AESUtils.Params, key: seq<uint8>, ctxt: seq<uint8>, iv: seq<uint8>, aad: seq<uint8>)
     returns (res: Result<seq<uint8>>)
     requires |key| == params.keyLen as int
   {
     res := AES.AESDecrypt(params, key, ctxt, iv, aad);
   }
 
+  //Note: The return value of AESEncrypt is the encrypted message, concatenated with the authentication tag.
   method AESEncrypt(params: AESUtils.Params, iv: seq<uint8>, key: seq<uint8>, msg: seq<uint8>, aad: seq<uint8>)
     returns (res : Result<seq<uint8>>)
     requires |iv| == params.ivLen as int

diff --git a/src/Crypto/AESUtils.dfy b/src/Crypto/AESUtils.dfy
@@ -14,8 +14,8 @@ module {:extern "AESUtils"} AESUtils {
 
   function method KeyLengthOfCipher(m: Mode): uint8 {
     match m
-    case AES256 => 32 as uint8
-    case AES192 => 24 as uint8
-    case AES128 => 16 as uint8
+    case AES256 => 32
+    case AES192 => 24
+    case AES128 => 16
   }
 }
diff --git a/src/Crypto/EncryptionExtern.cs b/src/Crypto/EncryptionExtern.cs
@@ -23,7 +23,6 @@ namespace AESEncryption {
     //TODO This code has yet to be reviewed. See issue #36
     public partial class AES_GCM {
 
-        //FIXME: Ensure that these methods correctly handle authenticaition tags, see #36
         public static STL.Result<byteseq> AESEncrypt(AESUtils.Params p,
                                                       byteseq iv,
                                                       byteseq key,
@@ -36,7 +35,7 @@ public static STL.Result<byteseq> AESEncrypt(AESUtils.Params p,
 
                 byte[] c = new byte[cipher.GetOutputSize(msg.Elements.Length)];
                 var len = cipher.ProcessBytes(msg.Elements, 0, msg.Elements.Length, c, 0);
-                cipher.DoFinal(c, len);
+                cipher.DoFinal(c, len); //Append authentication tag to `c`
                 return new STL.Result_Success<byteseq>(new byteseq(c));
             }
             catch {
@@ -51,7 +50,7 @@ public static STL.Result<byteseq> AESDecrypt(AESUtils.Params p, byteseq key, byt
                 cipher.Init(false, param);
                 var pt = new byte[cipher.GetOutputSize(ctx.Elements.Length)];
                 var len = cipher.ProcessBytes(ctx.Elements, 0, ctx.Elements.Length, pt, 0);
-                cipher.DoFinal(pt, len);
+                cipher.DoFinal(pt, len); //Check message authentication tag
                 return new STL.Result_Success<byteseq>(new byteseq(pt));
             }
             catch {