@@ -1,13 +1,36 @@
 #select
-| BadMacUse.java:60:42:60:50 | plaintext | BadMacUse.java:54:28:54:53 | doFinal(...) : byte[] | BadMacUse.java:60:42:60:50 | plaintext | MAC order potentially wrong: observed a potential decrypt operation output to MAC implying the MAC is on plaintext, and not a cipher. |
+| BadMacUse.java:56:42:56:50 | plaintext | BadMacUse.java:50:28:50:53 | doFinal(...) : byte[] | BadMacUse.java:56:42:56:50 | plaintext | MAC order potentially wrong: observed a potential decrypt operation output to MAC implying the MAC is on plaintext, and not a cipher. |
+| BadMacUse.java:124:42:124:51 | ciphertext | BadMacUse.java:92:16:92:36 | doFinal(...) : byte[] | BadMacUse.java:124:42:124:51 | ciphertext | MAC order potentially wrong: observed a potential decrypt operation output to MAC implying the MAC is on plaintext, and not a cipher. |
 edges
-| BadMacUse.java:30:29:30:53 | doFinal(...) : byte[] | BadMacUse.java:35:42:35:51 | ciphertext | provenance |  |
-| BadMacUse.java:54:28:54:53 | doFinal(...) : byte[] | BadMacUse.java:60:42:60:50 | plaintext | provenance |  |
+| BadMacUse.java:27:29:27:53 | doFinal(...) : byte[] | BadMacUse.java:32:42:32:51 | ciphertext | provenance |  |
+| BadMacUse.java:50:28:50:53 | doFinal(...) : byte[] | BadMacUse.java:56:42:56:50 | plaintext | provenance |  |
+| BadMacUse.java:84:83:84:91 | iv : byte[] | BadMacUse.java:90:63:90:64 | iv : byte[] | provenance |  |
+| BadMacUse.java:90:43:90:65 | new IvParameterSpec(...) : IvParameterSpec | BadMacUse.java:91:42:91:56 | ivParameterSpec | provenance | Sink:MaD:1 |
+| BadMacUse.java:90:63:90:64 | iv : byte[] | BadMacUse.java:90:43:90:65 | new IvParameterSpec(...) : IvParameterSpec | provenance | Config |
+| BadMacUse.java:90:63:90:64 | iv : byte[] | BadMacUse.java:90:43:90:65 | new IvParameterSpec(...) : IvParameterSpec | provenance | MaD:2 |
+| BadMacUse.java:92:16:92:36 | doFinal(...) : byte[] | BadMacUse.java:118:29:118:106 | cipherOperationWrapper(...) : byte[] | provenance |  |
+| BadMacUse.java:117:38:117:39 | iv : byte[] | BadMacUse.java:118:83:118:84 | iv : byte[] | provenance |  |
+| BadMacUse.java:118:29:118:106 | cipherOperationWrapper(...) : byte[] | BadMacUse.java:124:42:124:51 | ciphertext | provenance |  |
+| BadMacUse.java:118:83:118:84 | iv : byte[] | BadMacUse.java:84:83:84:91 | iv : byte[] | provenance |  |
+models
+| 1 | Sink: javax.crypto; Cipher; true; init; (int,Key,AlgorithmParameterSpec); ; Argument[2]; encryption-iv; manual |
+| 2 | Summary: javax.crypto.spec; IvParameterSpec; true; IvParameterSpec; ; ; Argument[0]; Argument[this]; taint; manual |
 nodes
-| BadMacUse.java:30:29:30:53 | doFinal(...) : byte[] | semmle.label | doFinal(...) : byte[] |
-| BadMacUse.java:35:42:35:51 | ciphertext | semmle.label | ciphertext |
-| BadMacUse.java:54:28:54:53 | doFinal(...) : byte[] | semmle.label | doFinal(...) : byte[] |
-| BadMacUse.java:60:42:60:50 | plaintext | semmle.label | plaintext |
+| BadMacUse.java:27:29:27:53 | doFinal(...) : byte[] | semmle.label | doFinal(...) : byte[] |
+| BadMacUse.java:32:42:32:51 | ciphertext | semmle.label | ciphertext |
+| BadMacUse.java:50:28:50:53 | doFinal(...) : byte[] | semmle.label | doFinal(...) : byte[] |
+| BadMacUse.java:56:42:56:50 | plaintext | semmle.label | plaintext |
+| BadMacUse.java:84:83:84:91 | iv : byte[] | semmle.label | iv : byte[] |
+| BadMacUse.java:90:43:90:65 | new IvParameterSpec(...) : IvParameterSpec | semmle.label | new IvParameterSpec(...) : IvParameterSpec |
+| BadMacUse.java:90:63:90:64 | iv : byte[] | semmle.label | iv : byte[] |
+| BadMacUse.java:91:42:91:56 | ivParameterSpec | semmle.label | ivParameterSpec |
+| BadMacUse.java:92:16:92:36 | doFinal(...) : byte[] | semmle.label | doFinal(...) : byte[] |
+| BadMacUse.java:117:38:117:39 | iv : byte[] | semmle.label | iv : byte[] |
+| BadMacUse.java:118:29:118:106 | cipherOperationWrapper(...) : byte[] | semmle.label | cipherOperationWrapper(...) : byte[] |
+| BadMacUse.java:118:83:118:84 | iv : byte[] | semmle.label | iv : byte[] |
+| BadMacUse.java:124:42:124:51 | ciphertext | semmle.label | ciphertext |
 subpaths
 testFailures
-| BadMacUse.java:67:118:67:128 | // $Source | Missing result: Source |
+| BadMacUse.java:63:118:63:128 | // $Source | Missing result: Source |
+| BadMacUse.java:92:16:92:36 | doFinal(...) : byte[] | Unexpected result: Source |
+| BadMacUse.java:124:42:124:51 | ciphertext | Unexpected result: Alert |
@@ -1,23 +1,20 @@
+
 import java.security.*;
 import java.util.Arrays;
-import java.util.Base64;
 import javax.crypto.Cipher;
-import javax.crypto.KeyGenerator;
 import javax.crypto.Mac;
 import javax.crypto.SecretKey;
-import javax.crypto.SecretKeyFactory;
-import javax.crypto.spec.PBEKeySpec;
+import javax.crypto.spec.IvParameterSpec;
 import javax.crypto.spec.SecretKeySpec;
 
-
 class BadMacUse {
 
     private byte[] generateSalt(int length) {
         byte[] salt = new byte[length];
         new SecureRandom().nextBytes(salt);
         return salt;
     }
-   
+
     public void CipherThenMac(byte[] encryptionKeyBytes, byte[] macKeyBytes) throws Exception {
         // Create keys directly from provided byte arrays
         SecretKey encryptionKey = new SecretKeySpec(encryptionKeyBytes, "AES");
@@ -40,7 +37,6 @@ public void CipherThenMac(byte[] encryptionKeyBytes, byte[] macKeyBytes) throws
         System.arraycopy(computedMac, 0, output, ciphertext.length, computedMac.length);
     }
 
-
     public void BadDecryptThenMacOnPlaintextVerify(byte[] encryptionKeyBytes, byte[] macKeyBytes, byte[] input) throws Exception {
         // Split input into ciphertext and MAC
         int macLength = 32; // HMAC-SHA256 output length
@@ -84,4 +80,53 @@ public void BadMacOnPlaintext(byte[] encryptionKeyBytes, byte[] macKeyBytes, byt
         System.arraycopy(ciphertext, 0, output, 0, ciphertext.length);
         System.arraycopy(computedMac, 0, output, ciphertext.length, computedMac.length);
     }
-}
+
+    public byte[] cipherOperationWrapper(byte[] bytes, byte[] encryptionKeyBytes, byte[] iv, int mode)
+            throws Exception {
+
+        Cipher cipher = Cipher.getInstance("AES/CBC/PKCS5Padding");
+        SecretKeySpec secretKeySpec = new SecretKeySpec(encryptionKeyBytes, "AES");
+
+        IvParameterSpec ivParameterSpec = new IvParameterSpec(iv);
+        cipher.init(mode, secretKeySpec, ivParameterSpec);
+        return cipher.doFinal(bytes);
+    }
+
+    /**
+     * A use of the cipher operation wrapper for decryption to throw off the
+     * analysis
+     */
+    public byte[] decryptUsingWrapper(byte[] ciphertext, byte[] encryptionKeyBytes, byte[] iv) throws Exception {
+        return cipherOperationWrapper(ciphertext, encryptionKeyBytes, iv, Cipher.DECRYPT_MODE);
+    }
+
+    /**
+     * A use of the cipher operation wrapper for encryption to throw off the
+     * analysis
+     */
+    public byte[] encryptUsingWrapper(byte[] plaintext, byte[] encryptionKeyBytes, byte[] iv) throws Exception {
+        return cipherOperationWrapper(plaintext, encryptionKeyBytes, iv, Cipher.ENCRYPT_MODE);
+    }
+
+    /**
+     * Encrypt then mac using the wrapper function
+     */
+    public byte[] falsePositiveDecryptToMac(byte[] encryptionKeyBytes, byte[] macKeyBytes, byte[] plaintext) throws Exception {
+        // Encrypt the plaintext
+        byte[] iv = new byte[16];
+        new SecureRandom().nextBytes(iv);
+        byte[] ciphertext = cipherOperationWrapper(plaintext, encryptionKeyBytes, iv, Cipher.ENCRYPT_MODE);
+
+        // Compute HMAC over the ciphertext using the MAC key
+        SecretKey macKey = new SecretKeySpec(macKeyBytes, "HmacSHA256");
+        Mac mac = Mac.getInstance("HmacSHA256");
+        mac.init(macKey);
+        byte[] computedMac = mac.doFinal(ciphertext); // False Positive
+
+        // Concatenate ciphertext and MAC
+        byte[] output = new byte[ciphertext.length + computedMac.length];
+        System.arraycopy(ciphertext, 0, output, 0, ciphertext.length);
+        System.arraycopy(computedMac, 0, output, ciphertext.length, computedMac.length);
+        return output;
+    }
+}