		Search-engine friendly clone of the ACL2 documentation.

Interfaces

Aes-128-interface

AES-128 is specified in the FIPS PUB 197 standard.

According to FIPS PUB 197, AES-128 has a key size of 128 bits and a block size of 128 bits.

Definitions and Theorems

Theorem: bit-list-of-aes-128-encrypt-bits

(defthm bit-list-of-aes-128-encrypt-bits
  (bit-listp (aes-128-encrypt-bits key block)))

Theorem: bit-list-of-aes-128-decrypt-bits

(defthm bit-list-of-aes-128-decrypt-bits
  (bit-listp (aes-128-decrypt-bits key block)))

Theorem: byte-list-of-aes-128-encrypt-bytes

(defthm byte-list-of-aes-128-encrypt-bytes
  (byte-listp (aes-128-encrypt-bytes key block)))

Theorem: byte-list-of-aes-128-decrypt-bytes

(defthm byte-list-of-aes-128-decrypt-bytes
  (byte-listp (aes-128-decrypt-bytes key block)))

Theorem: len-of-aes-128-encrypt-bits

(defthm len-of-aes-128-encrypt-bits
  (equal (len (aes-128-encrypt-bits key block))
         128))

Theorem: len-of-aes-128-decrypt-bits

(defthm len-of-aes-128-decrypt-bits
  (equal (len (aes-128-decrypt-bits key block))
         128))

Theorem: len-of-aes-128-encrypt-bytes

(defthm len-of-aes-128-encrypt-bytes
  (equal (len (aes-128-encrypt-bytes key block))
         16))

Theorem: len-of-aes-128-decrypt-bytes

(defthm len-of-aes-128-decrypt-bytes
  (equal (len (aes-128-decrypt-bytes key block))
         16))

Theorem: aes-128-encrypt-bits-of-bit-list-fix-key

(defthm aes-128-encrypt-bits-of-bit-list-fix-key
  (equal (aes-128-encrypt-bits (acl2::bit-list-fix key)
                               block)
         (aes-128-encrypt-bits key block)))

Theorem: aes-128-encrypt-bits-bit-list-equiv-congruence-on-key

(defthm aes-128-encrypt-bits-bit-list-equiv-congruence-on-key
  (implies (acl2::bit-list-equiv key key-equiv)
           (equal (aes-128-encrypt-bits key block)
                  (aes-128-encrypt-bits key-equiv block)))
  :rule-classes :congruence)

Theorem: aes-128-encrypt-bits-of-bit-list-fix-block

(defthm aes-128-encrypt-bits-of-bit-list-fix-block
  (equal (aes-128-encrypt-bits key (acl2::bit-list-fix block))
         (aes-128-encrypt-bits key block)))

Theorem: aes-128-encrypt-bits-bit-list-equiv-congruence-on-block

(defthm aes-128-encrypt-bits-bit-list-equiv-congruence-on-block
  (implies (acl2::bit-list-equiv block block-equiv)
           (equal (aes-128-encrypt-bits key block)
                  (aes-128-encrypt-bits key block-equiv)))
  :rule-classes :congruence)

Theorem: aes-128-decrypt-bits-of-bit-list-fix-key

(defthm aes-128-decrypt-bits-of-bit-list-fix-key
  (equal (aes-128-decrypt-bits (acl2::bit-list-fix key)
                               block)
         (aes-128-decrypt-bits key block)))

Theorem: aes-128-decrypt-bits-bit-list-equiv-congruence-on-key

(defthm aes-128-decrypt-bits-bit-list-equiv-congruence-on-key
  (implies (acl2::bit-list-equiv key key-equiv)
           (equal (aes-128-decrypt-bits key block)
                  (aes-128-decrypt-bits key-equiv block)))
  :rule-classes :congruence)

Theorem: aes-128-decrypt-bits-of-bit-list-fix-block

(defthm aes-128-decrypt-bits-of-bit-list-fix-block
  (equal (aes-128-decrypt-bits key (acl2::bit-list-fix block))
         (aes-128-decrypt-bits key block)))

Theorem: aes-128-decrypt-bits-bit-list-equiv-congruence-on-block

(defthm aes-128-decrypt-bits-bit-list-equiv-congruence-on-block
  (implies (acl2::bit-list-equiv block block-equiv)
           (equal (aes-128-decrypt-bits key block)
                  (aes-128-decrypt-bits key block-equiv)))
  :rule-classes :congruence)

Theorem: aes-128-encrypt-bytes-of-byte-list-fix-key

(defthm aes-128-encrypt-bytes-of-byte-list-fix-key
  (equal (aes-128-encrypt-bytes (byte-list-fix key)
                                block)
         (aes-128-encrypt-bytes key block)))

Theorem: aes-128-encrypt-bytes-byte-list-equiv-congruence-on-key

(defthm aes-128-encrypt-bytes-byte-list-equiv-congruence-on-key
  (implies (byte-list-equiv key key-equiv)
           (equal (aes-128-encrypt-bytes key block)
                  (aes-128-encrypt-bytes key-equiv block)))
  :rule-classes :congruence)

Theorem: aes-128-encrypt-bytes-of-byte-list-fix-block

(defthm aes-128-encrypt-bytes-of-byte-list-fix-block
  (equal (aes-128-encrypt-bytes key (byte-list-fix block))
         (aes-128-encrypt-bytes key block)))

Theorem: aes-128-encrypt-bytes-byte-list-equiv-congruence-on-block

(defthm aes-128-encrypt-bytes-byte-list-equiv-congruence-on-block
  (implies (byte-list-equiv block block-equiv)
           (equal (aes-128-encrypt-bytes key block)
                  (aes-128-encrypt-bytes key block-equiv)))
  :rule-classes :congruence)

Theorem: aes-128-decrypt-bytes-of-byte-list-fix-key

(defthm aes-128-decrypt-bytes-of-byte-list-fix-key
  (equal (aes-128-decrypt-bytes (byte-list-fix key)
                                block)
         (aes-128-decrypt-bytes key block)))

Theorem: aes-128-decrypt-bytes-byte-list-equiv-congruence-on-key

(defthm aes-128-decrypt-bytes-byte-list-equiv-congruence-on-key
  (implies (byte-list-equiv key key-equiv)
           (equal (aes-128-decrypt-bytes key block)
                  (aes-128-decrypt-bytes key-equiv block)))
  :rule-classes :congruence)

Theorem: aes-128-decrypt-bytes-of-byte-list-fix-block

(defthm aes-128-decrypt-bytes-of-byte-list-fix-block
  (equal (aes-128-decrypt-bytes key (byte-list-fix block))
         (aes-128-decrypt-bytes key block)))

Theorem: aes-128-decrypt-bytes-byte-list-equiv-congruence-on-block

(defthm aes-128-decrypt-bytes-byte-list-equiv-congruence-on-block
  (implies (byte-list-equiv block block-equiv)
           (equal (aes-128-decrypt-bytes key block)
                  (aes-128-decrypt-bytes key block-equiv)))
  :rule-classes :congruence)

Theorem: true-listp-of-aes-128-encrypt-bits

(defthm true-listp-of-aes-128-encrypt-bits
  (true-listp (aes-128-encrypt-bits key block))
  :rule-classes :type-prescription)

Theorem: true-listp-of-aes-128-decrypt-bits

(defthm true-listp-of-aes-128-decrypt-bits
  (true-listp (aes-128-decrypt-bits key block))
  :rule-classes :type-prescription)

Theorem: true-listp-of-aes-128-encrypt-bytes

(defthm true-listp-of-aes-128-encrypt-bytes
  (true-listp (aes-128-encrypt-bytes key block))
  :rule-classes :type-prescription)

Theorem: true-listp-of-aes-128-decrypt-bytes

(defthm true-listp-of-aes-128-decrypt-bytes
  (true-listp (aes-128-decrypt-bytes key block))
  :rule-classes :type-prescription)

Theorem: consp-of-aes-128-encrypt-bits

(defthm consp-of-aes-128-encrypt-bits
  (consp (aes-128-encrypt-bits key block))
  :rule-classes :type-prescription)

Theorem: consp-of-aes-128-decrypt-bits

(defthm consp-of-aes-128-decrypt-bits
  (consp (aes-128-decrypt-bits key block))
  :rule-classes :type-prescription)

Theorem: consp-of-aes-128-encrypt-bytes

(defthm consp-of-aes-128-encrypt-bytes
  (consp (aes-128-encrypt-bytes key block))
  :rule-classes :type-prescription)

Theorem: consp-of-aes-128-decrypt-bytes

(defthm consp-of-aes-128-decrypt-bytes
  (consp (aes-128-decrypt-bytes key block))
  :rule-classes :type-prescription)