Added fixes in Client.Encrypt

* aes_encrypt returns the authTag, so don't try to compute it outside the routine

* Store verification key, not signature key, under "aws-crypto-public-key" in
  encryption context.

* Add function to compute StringToByteSeq(Base64.Encode(_)). In the future, the
  Base64 module may offer routines that operate directly on seq<uint8> instead of
  just seq<char>.

* Use ENDFRAME_SEQUENCE_NUMBER constant instead of numeric literal

* Fix spelling mistake in comment

Author: RustanLeino

src/SDK/CMM/DefaultCMM.dfy

@@ -61,7 +61,7 @@ module DefaultCMMDef {
             case None => return Failure("Keygen error");
             case Some(ab) =>
               enc_sk := Some(ab.1);
-              enc_ec := [(Materials.EC_PUBLIC_KEY_FIELD, StringToByteSeq(Base64.Encode(ab.1)))] + enc_ec;
+              enc_ec := [(Materials.EC_PUBLIC_KEY_FIELD, Base64.EncodeToByteSeq(ab.0))] + enc_ec;
       }
 
       var in_enc_mat := new Materials.EncryptionMaterials(id, [], enc_ec, None, enc_sk);

src/SDK/Client.dfy

@@ -69,7 +69,10 @@ module ESDKClient {
     var unauthenticatedHeader := wr.data;
 
     var iv: seq<uint8> := seq(encMat.algorithmSuiteID.IVLength(), _ => 0);
-    var authTag :- MessageBody.Encrypt(encMat.algorithmSuiteID, iv, derivedDataKey, [], unauthenticatedHeader);
+    var pair :- MessageBody.Encrypt(encMat.algorithmSuiteID, iv, derivedDataKey, [], unauthenticatedHeader);
+    assert |pair.0| == 0;
+    var headerAuthentication := Msg.HeaderAuthentication(iv, pair.1);
+    var _ :- Serialize.SerializeHeaderAuthentication(wr, headerAuthentication, encMat.algorithmSuiteID);
 
     /*
      * Encrypt the given plaintext into the message body.
@@ -81,7 +84,7 @@ module ESDKClient {
      * Add footer with signature, if required.
      */
 
-    var msg := unauthenticatedHeader + authTag + body;
+    var msg := wr.data + body;
 
     match encMat.algorithmSuiteID.SignatureType() {
       case None =>

src/SDK/MessageBody.dfy

@@ -23,9 +23,9 @@ module MessageBody {
     var n, sequenceNumber := 0, 1;
     while n + frameLength <= |plaintext|
       invariant 0 <= n <= |plaintext|
-      invariant sequenceNumber <= 0xFFFF_FFFF
+      invariant sequenceNumber <= ENDFRAME_SEQUENCE_NUMBER
     {
-      if sequenceNumber == 0xFFFF_FFFF {
+      if sequenceNumber == ENDFRAME_SEQUENCE_NUMBER {
         return Failure("too many frames");
       }
       var plaintextFrame := plaintext[n..n + frameLength];
@@ -39,16 +39,16 @@ module MessageBody {
   }
 
   method EncryptFrame(algorithmSuiteID: AlgorithmSuite.ID, key: seq<uint8>, frameLength: int, messageID: Msg.MessageID,
-                      plaintext: seq<uint8>, sequenceNumber: int, final: bool)
+                      plaintext: seq<uint8>, sequenceNumber: uint32, final: bool)
       returns (res: Result<seq<uint8>>)
     requires |key| == algorithmSuiteID.KeyLength()
-    requires 0 < frameLength && 0 < sequenceNumber <= 0xFFFF_FFFF
+    requires 0 < frameLength && 0 < sequenceNumber <= ENDFRAME_SEQUENCE_NUMBER
     requires |plaintext| < UINT32_LIMIT
-    requires !final ==> |plaintext| == frameLength && sequenceNumber != 0xFFFF_FFFF
+    requires !final ==> |plaintext| == frameLength && sequenceNumber != ENDFRAME_SEQUENCE_NUMBER
     requires final ==> |plaintext| < frameLength
     requires 4 <= algorithmSuiteID.IVLength()
   {
-    var unauthenticatedFrame := if final then UInt32ToSeq(0xFFFF_FFFF) else [];
+    var unauthenticatedFrame := if final then UInt32ToSeq(ENDFRAME_SEQUENCE_NUMBER) else [];
     var seqNumSeq := UInt32ToSeq(sequenceNumber as uint32);
     unauthenticatedFrame := unauthenticatedFrame + seqNumSeq;
 
@@ -63,21 +63,33 @@ module MessageBody {
     var contentAAD := if final then BODY_AAD_CONTENT_FINAL_FRAME else BODY_AAD_CONTENT_REGULAR_FRAME;
     var aad := messageID + contentAAD + seqNumSeq + UInt64ToSeq(|plaintext| as uint64);
 
-    var encryptedContents :- Encrypt(algorithmSuiteID, iv, key, plaintext, aad);
-    unauthenticatedFrame := unauthenticatedFrame + encryptedContents;
+    var pair :- Encrypt(algorithmSuiteID, iv, key, plaintext, aad);
+    var (encryptedContents, authTag) := pair;
+    unauthenticatedFrame := unauthenticatedFrame + encryptedContents + authTag;
 
-    var authTag :- Encrypt(algorithmSuiteID, iv, key, unauthenticatedFrame, aad);
-    return Success(unauthenticatedFrame + authTag);
+    return Success(unauthenticatedFrame);
   }
 
   const BODY_AAD_CONTENT_REGULAR_FRAME := StringToByteSeq("AWSKMSEncryptionClient Frame");
   const BODY_AAD_CONTENT_FINAL_FRAME := StringToByteSeq("AWSKMSEncryptionClient Final Frame");
 
-  method Encrypt(algorithmSuiteID: AlgorithmSuite.ID, iv: seq<uint8>, key: seq<uint8>, plaintext: seq<uint8>, aad: seq<uint8>) returns (res: Result<seq<uint8>>)
+  const ENDFRAME_SEQUENCE_NUMBER: uint32 := 0xFFFF_FFFF
+
+  method Encrypt(algorithmSuiteID: AlgorithmSuite.ID, iv: seq<uint8>, key: seq<uint8>, plaintext: seq<uint8>, aad: seq<uint8>) returns (res: Result<(seq<uint8>,seq<uint8>)>)
     requires |iv| == algorithmSuiteID.IVLength()
     requires |key| == algorithmSuiteID.KeyLength()
+    ensures match res
+      case Success((ciphertext, authTag)) =>
+        |ciphertext| == |plaintext| &&
+        |authTag| == algorithmSuiteID.TagLength()
+      case Failure(_) => true
   {
     var cipher := AlgorithmSuite.Suite[algorithmSuiteID].params;
-    res := AESEncryption.AES.aes_encrypt(cipher, iv, key, plaintext, aad);
+    var bytes :- AESEncryption.AES.aes_encrypt(cipher, iv, key, plaintext, aad);
+    var n := |plaintext|;
+    if |bytes| != n + algorithmSuiteID.TagLength() {
+      return Failure("unexpected AES encryption result");
+    }
+    return Success((bytes[..n], bytes[n..]));
   }
 }

src/StandardLibrary/Base64.dfy

@@ -231,6 +231,14 @@ module Base64 {
         res
     }
 
+    function method DecodeFromByteSeq(s: seq<uint8>): Result<seq<uint8>> {
+      Decode(ByteSeqToString(s))
+    }
+
+    function method EncodeToByteSeq(b: seq<uint8>): seq<uint8> {
+      StringToByteSeq(Encode(b))
+    }
+
     method TestBase64(msg: string, expected: string)
         requires forall k :: 0 <= k < |msg| ==> 0 <= msg[k] as int < 0x100
     {

src/extern/dotnet/EncryptionExtern.cs

@@ -222,7 +222,7 @@ public static STL.Option<byteseq> Sign(ECDSAParams x, byteseq sk, byteseq msg) {
                 byte[] bytes = SignatureToByteArray(sig[0], sig[1]);
                 if (bytes.Length != x.SignatureLength()) {
                     // Most of the time, a signature of the wrong length can be fixed
-                    // be negating s in the signature relative to the group order.
+                    // by negating s in the signature relative to the group order.
                     bytes = SignatureToByteArray(sig[0], p.N.Subtract(sig[1]));
                     if (bytes.Length != x.SignatureLength()) {
                         // We give up. :(