diff --git a/Primitive/Symmetric/Cipher/Authenticated/AES_GCM_SIV.cry b/Primitive/Symmetric/Cipher/Authenticated/AES_GCM_SIV.cry
index a7f58016..8114cfd6 100644
--- a/Primitive/Symmetric/Cipher/Authenticated/AES_GCM_SIV.cry
+++ b/Primitive/Symmetric/Cipher/Authenticated/AES_GCM_SIV.cry
@@ -33,7 +33,7 @@ type Mode = KeySize / 128 - 1
 type K  = 128 + 128 * Mode
 import Primitive::Symmetric::Cipher::Block::AES_specification as AES where
   type KeySize' = KeySize
-type KS = AES::EncryptionKey
+type KS = AES::ExpandedKey
 
 
 /** Note the weird byte-swapping business (also in `blockify` and `unblockify`)
@@ -58,7 +58,7 @@ aes : KS -> [128] -> [128]
 aes ks v = byteSwap (AES::encryptWithSchedule ks (byteSwap v))
 
 expandKey : [K] -> KS
-expandKey k = AES::expandKeyEnc (byteSwap k)
+expandKey k = AES::keyExpansion (byteSwap k)
 
 /** See Figure 2 in Section 4 */
 derive_key : [K] -> [96] -> ([128], KS)
diff --git a/Primitive/Symmetric/Cipher/Block/AES/Algorithm.cry b/Primitive/Symmetric/Cipher/Block/AES/Algorithm.cry
index c1b43f37..17721cbb 100644
--- a/Primitive/Symmetric/Cipher/Block/AES/Algorithm.cry
+++ b/Primitive/Symmetric/Cipher/Block/AES/Algorithm.cry
@@ -1,54 +1,78 @@
 // Cryptol AES Implementation
-// Copyright (c) 2010-2018, Galois Inc.
+//
+// @copyright Galois Inc.
+// @author Nichole Shimanski <nls@galois.com>
+// @author Marcella Hastings <marcella@galois.com>
 // www.cryptol.net
-
-// This is a fairly close implementation of the FIPS-197 standard:
-//   http://csrc.nist.gov/publications/fips/fips197/fips-197.pdf
+//
+//
+// References
+// [FIPS-197u1]: Morris J. Dworkin, Elaine B. Barker, James R. Nechvatal,
+// James Foti, Lawrence E. Bassham, E. Roback, and James F. Dray Jr.
+// Advanced Encryption Standard (AES). Federal Inf. Process. Stds. (NIST FIPS)
+// 197, update 1. May 2023.
+//
 
 module Primitive::Symmetric::Cipher::Block::AES::Algorithm where
 
 import Primitive::Symmetric::Cipher::Block::AES::State (State, RoundKey, msgToState, stateToMsg)
-import Primitive::Symmetric::Cipher::Block::AES::Round (AESFinalRound, AESFinalInvRound)
+import Primitive::Symmetric::Cipher::Block::AES::Round as Round
 
 parameter
   /** 0: AES128, 1: AES192, 2: AES256 */
   type Mode : #
-
   type constraint (2 >= Mode)
 
-  encRound     : RoundKey -> State -> State
-  decRound     : RoundKey -> State -> State
+/* The following section encodes [FIPS-197u1] Section 5, Table 3
+ * The table is described in terms of the `Mode`.
+ */
 
-
-/** Number of 32 bit words in the key */
+/** Key length: number of 32 bit words in the key */
 type Nk = 4 + 2 * Mode
 
 /** Number of rounds */
 type Nr = 6 + Nk
 
-/** Key size in bits */
-type AESKeySize  = 32 * Nk
-
 /** The keys for all the rounds */
 type KeySchedule = (RoundKey, [Nr-1]RoundKey, RoundKey)
 
-/** AES Encryption with an expanded key.
-This is useful if many things will be encrypted with the same key. */
-encrypt : KeySchedule -> [128] -> [128]
-encrypt (kInit,ks,kFinal) pt =
-                            stateToMsg (AESFinalRound kFinal (rounds ! 0))
+/**
+ * The general function for executing AES with 128-, 192-, or 256-bit keys.
+ *
+ * Corresponds to [FIPS-197u1] Section 5.1, Algorithm 1.
+ *
+ * In the spec, the three inputs to `Cipher` are the input data, the number of
+ * rounds `Nr`, and the round keys. In this implementation, we don't explicitly
+ * pass `Nr` as a parameter; instead it's defined as a type above. We also
+ * switch the order of the input and keys.
+ */
+cipher: KeySchedule -> [128] -> [128]
+cipher (kInit,ks,kFinal) pt =
+    // Lines 10-13
+    stateToMsg (Round::AESFinalRound kFinal (rounds ! 0))
   where
-  state0 = kInit ^ msgToState pt
-  rounds = [state0] # [ encRound rk s | rk <- ks | s <- rounds ]
-
-/** AES decryption with an expanded key.
-This is useful if many things will be decrypted with the same key. */
-decrypt : KeySchedule -> [128] -> [128]
-decrypt (kInit, ks, kFinal) ct =
-                          stateToMsg (AESFinalInvRound kFinal (rounds ! 0))
+    // Lines 2-3
+    state0 = kInit ^ msgToState pt
+    // Lines 4-9
+    rounds = [state0] # [ Round::AESRound rk s | rk <- ks | s <- rounds ]
+
+/**
+ * The general function for inverting AES with 128-, 192-, or 256-bit keys.
+ *
+ * This inverts and reverses the order of the transformations in `cipher`.
+ * Corresponds to [FIPS-197u1] Section 5.3, Algorithm 3.
+ *
+ * In the spec, the three inputs to `InvCipher` are the input data, the number of
+ * rounds `Nr`, and the round keys. In this implementation, we don't explicitly
+ * pass `Nr` as a parameter; instead it's defined as a type above. We also
+ * switch the order of the input and keys.
+ */
+invCipher: KeySchedule -> [128] -> [128]
+invCipher (kInit, ks, kFinal) ct =
+    // Lines 10-13
+    stateToMsg (Round::AESFinalInvRound kInit (rounds ! 0))
   where
-  state0 = kInit ^ msgToState ct
-  rounds = [state0] # [ decRound rk s | rk <- ks | s <- rounds ]
-
-
-
+    // Lines 2-3
+    state0 = kFinal ^ msgToState ct
+    // Lines 4-9
+    rounds = [state0] # [ Round::AESInvRound rk s | rk <- (reverse ks) | s <- rounds ]
diff --git a/Primitive/Symmetric/Cipher/Block/AES/SubBytePlain.cry b/Primitive/Symmetric/Cipher/Block/AES/SubBytePlain.cry
index 45bcb749..943c1170 100644
--- a/Primitive/Symmetric/Cipher/Block/AES/SubBytePlain.cry
+++ b/Primitive/Symmetric/Cipher/Block/AES/SubBytePlain.cry
@@ -1,20 +1,20 @@
 module Primitive::Symmetric::Cipher::Block::AES::SubBytePlain where
 
-import Common::GF28 as GF28'
-private type GF28 = GF28'::GF28
+import Common::GF28 as GF28
+private type GF28 = GF28::GF28
 
 // The SubBytes transform and its inverse
 SubByte : GF28 -> GF28
-SubByte b = xformByte (GF28'::inverse b)
+SubByte b = xformByte (GF28::inverse b)
 
 InvSubByte : GF28 -> GF28
-InvSubByte b = GF28'::inverse (xformByte' b)
+InvSubByte b = GF28::inverse (xformByte' b)
 
 
 // The affine transform and its inverse
 xformByte : GF28 -> GF28
-xformByte b = GF28'::add [b, (b >>> 4), (b >>> 5), (b >>> 6), (b >>> 7), c]
+xformByte b = GF28::add [b, (b >>> 4), (b >>> 5), (b >>> 6), (b >>> 7), c]
    where c = 0x63
 
 xformByte' : GF28 -> GF28
-xformByte' b = GF28'::add [(b >>> 2), (b >>> 5), (b >>> 7), d] where d = 0x05
+xformByte' b = GF28::add [(b >>> 2), (b >>> 5), (b >>> 7), d] where d = 0x05
diff --git a/Primitive/Symmetric/Cipher/Block/AES/TBox.cry b/Primitive/Symmetric/Cipher/Block/AES/TBox.cry
index 4f029bca..75cc365c 100644
--- a/Primitive/Symmetric/Cipher/Block/AES/TBox.cry
+++ b/Primitive/Symmetric/Cipher/Block/AES/TBox.cry
@@ -1,7 +1,7 @@
 module Primitive::Symmetric::Cipher::Block::AES::TBox where
 
-import Common::GF28 as GF28'
-private type GF28 = GF28'::GF28
+import Common::GF28 as GF28
+private type GF28 = GF28::GF28
 import Primitive::Symmetric::Cipher::Block::AES::State
 import Primitive::Symmetric::Cipher::Block::AES::SBox
 import Primitive::Symmetric::Cipher::Block::AES::Round
@@ -11,9 +11,6 @@ AESRound    rk st = genRound ShiftRows    tbox    rk st
 // AESInvRound rk st = genRound InvShiftRows tboxInv (InvMixColumns rk) st
 AESInvRound rk st = genRound InvShiftRows tboxInv rk st
 
-
-makeDecKey (a,xs,b) = (b, [ InvMixColumns rk | rk <- reverse xs ], a)
-
 genRound : (State -> State) -> TBox -> RoundKey -> State -> State
 genRound shift boxes rk st =
   rk ^ transpose [ add [ box @ i | box <- boxes | i <- col ]
@@ -34,4 +31,4 @@ tboxInv = mkTBox [ 0x0e, 0x09, 0x0d, 0x0b ] sboxInv
 mkTBox : [4]GF28 -> SBox -> TBox
 mkTBox seed box = [ [ a >>> i | a <- t0 ] | i <- [0 .. 3] ]
   where
-  t0 = [ [ GF28'::mult c s | c <- seed ] | s <- box ]
+  t0 = [ [ GF28::mult c s | c <- seed ] | s <- box ]
diff --git a/Primitive/Symmetric/Cipher/Block/AES_specification.cry b/Primitive/Symmetric/Cipher/Block/AES_specification.cry
index 6e393a0a..a74fb340 100644
--- a/Primitive/Symmetric/Cipher/Block/AES_specification.cry
+++ b/Primitive/Symmetric/Cipher/Block/AES_specification.cry
@@ -8,6 +8,11 @@
    It operates over 128-bit blocks. To use AES with any practical application,
    use it with a mode of operation, like CTR or GCM-SIV.
 
+   References
+   [FIPS-197u1]: Morris J. Dworkin, Elaine B. Barker, James R. Nechvatal,
+   James Foti, Lawrence E. Bassham, E. Roback, and James F. Dray Jr.
+   Advanced Encryption Standard (AES). Federal Inf. Process. Stds. (NIST FIPS)
+   197, update 1. May 2023.
 */
 
 module Primitive::Symmetric::Cipher::Block::AES_specification where
@@ -33,10 +38,10 @@ type KeySize = KeySize'
 type BlockSize = 128
 
 encrypt : [KeySize] -> [BlockSize] -> [BlockSize]
-encrypt k = encryptWithSchedule (expandKeyEnc k)
+encrypt k = encryptWithSchedule (keyExpansion k)
 
 decrypt : [KeySize] -> [BlockSize] -> [BlockSize]
-decrypt k = decryptWithSchedule (expandKeyDec k)
+decrypt k = decryptWithSchedule (keyExpansion k)
 
 // This property must be true. It should be proven for each instantiation.
 // With high probability, it will be extremely slow to prove and should be `:check`ed.
@@ -45,23 +50,17 @@ property aesIsCorrect k pt = decrypt k (encrypt k pt) == pt
 // The following methods should not be used in general. They are public
 // to support a confusing endianness issue in the implementation of
 // AES-GCM-SIV.
-type EncryptionKey = AES::KeySchedule Mode
-type DecryptionKey = AES::KeySchedule Mode
+type ExpandedKey = AES::KeySchedule Mode
 
-expandKeyEnc : [KeySize] -> EncryptionKey
-expandKeyEnc = expandKey`{Nk = AES::Nk Mode, Nr = AES::Nr Mode}
+keyExpansion: [KeySize] -> ExpandedKey
+keyExpansion = expandKey`{Nk = AES::Nk Mode, Nr = AES::Nr Mode}
 
-encryptWithSchedule : EncryptionKey -> [BlockSize] -> [BlockSize]
-encryptWithSchedule = AES::encrypt params
+encryptWithSchedule :  ExpandedKey -> [BlockSize] -> [BlockSize]
+encryptWithSchedule = AES::cipher
 
 private
-   expandKeyDec : [KeySize] -> EncryptionKey
-   expandKeyDec k = makeDecKey (expandKey`{Nk = AES::Nk Mode, Nr = AES::Nr Mode} k)
+   decryptWithSchedule : ExpandedKey -> [BlockSize] -> [BlockSize]
+   decryptWithSchedule = AES::invCipher
 
-   // AES decryption with a specified KeySchedule
-   decryptWithSchedule : DecryptionKey -> [BlockSize] -> [BlockSize]
-   decryptWithSchedule = AES::decrypt params
-
-   params = { encRound = AESRound, decRound = AESInvRound }