mirror of
https://github.com/NationalSecurityAgency/Foundation.git
synced 2026-11-07 06:06:00 -10:00
initial commit
This commit is contained in:
weaversa committed
commit
7d0528bd99
241 files changed
+15594
No files matched your search
Executable
+6
@@ -0,0 +1,6 @@
|
||||
#! /bin/sh
|
||||
|
||||
# Run `cargo build --release` on all Rust projects.
|
||||
set -e
|
||||
CARGO_TOML_FILES=`find . -name "Cargo.toml"`
|
||||
for f in $CARGO_TOML_FILES; do cargo build --manifest-path $f --release; done;
|
||||
Executable
+9
@@ -0,0 +1,9 @@
|
||||
#! /bin/sh
|
||||
|
||||
# Run `cargo saw-build` on all Rust projects.
|
||||
set -e
|
||||
CARGO_TOML_FILES=`find . -name "Cargo.toml"`
|
||||
for f in $CARGO_TOML_FILES; do cargo saw-build --manifest-path $f --release; done
|
||||
|
||||
# Rename mir json files and move them next to associated `Cargo.toml`.
|
||||
find . -name "*.linked-mir.json" -exec sh -c "mv '{}' \$(dirname '{}')/../../../../linked-mir.json" \;
|
||||
@@ -0,0 +1,14 @@
|
||||
import glob
|
||||
import cryptol
|
||||
|
||||
# Create a list of all `.cry` files.
|
||||
cryptol_files = glob.glob(r"**/*.cry", recursive=True)
|
||||
|
||||
# Connect to `cryptol-remote-api`.
|
||||
c = cryptol.connect()
|
||||
|
||||
# Attempt to load all `.cry` files. This will raise an exception if a
|
||||
# file does not exist or load properly.
|
||||
for f in cryptol_files:
|
||||
print(f'Loading {f}')
|
||||
c.load_file(f).result()
|
||||
Executable
+8
@@ -0,0 +1,8 @@
|
||||
#! /bin/sh
|
||||
|
||||
# Run all `saw.py` files in virtual environment for SAW Remote API.
|
||||
set -e
|
||||
export SAW_SOLVER_CACHE_PATH=${SAW_SOLVER_CACHE_PATH:=$(pwd)/saw-cache}
|
||||
export VENV_SAW=${VENV_SAW:=/opt/venv/saw-remote-api}
|
||||
SAWFILES=`find . -name "saw.py"`
|
||||
for f in $SAWFILES; do $VENV_SAW/bin/python3 $f; done;
|
||||
Executable
+7
@@ -0,0 +1,7 @@
|
||||
#! /bin/sh
|
||||
|
||||
# Run `saw` on all `all.saw` files.
|
||||
set -e
|
||||
export SAW_SOLVER_CACHE_PATH=${SAW_SOLVER_CACHE_PATH:=$(pwd)/saw-cache}
|
||||
SAWFILES=`find . -name "all.saw"`
|
||||
for f in $SAWFILES; do saw $f; done;
|
||||
@@ -0,0 +1 @@
|
||||
{"image":"ghcr.io/nationalsecurityagency/foundation/cryptol-dev:latest"}
|
||||
@@ -0,0 +1 @@
|
||||
{"image":"ghcr.io/nationalsecurityagency/foundation/saw-dev:latest"}
|
||||
@@ -0,0 +1,17 @@
|
||||
# See https://docs.github.com/code-security/dependabot/dependabot-version-updates/configuration-options-for-the-dependabot.yml-file
|
||||
|
||||
version: 2
|
||||
|
||||
updates:
|
||||
- package-ecosystem: "cargo"
|
||||
directories:
|
||||
- "algorithms/AES/rust/KeyExpansion/"
|
||||
- "algorithms/AES/rust/Cipher/"
|
||||
- "shared/rust/ffi_utils/"
|
||||
schedule:
|
||||
interval: "daily"
|
||||
|
||||
- package-ecosystem: "github-actions"
|
||||
directory: ".github/workflows"
|
||||
schedule:
|
||||
interval: "daily"
|
||||
@@ -0,0 +1,44 @@
|
||||
FROM public.ecr.aws/lts/ubuntu:24.04_stable
|
||||
|
||||
USER root
|
||||
|
||||
RUN apt-get update \
|
||||
&& DEBIAN_FRONTEND="noninteractive" apt-get dist-upgrade --yes \
|
||||
&& DEBIAN_FRONTEND="noninteractive" apt-get install --yes ca-certificates curl gnupg lsb-release \
|
||||
&& mkdir -p /etc/apt/keyrings \
|
||||
&& curl -fsSL https://download.docker.com/linux/ubuntu/gpg | gpg --dearmor -o /etc/apt/keyrings/docker.gpg \
|
||||
&& chmod a+r /etc/apt/keyrings/docker.gpg \
|
||||
&& echo "deb [arch=$(dpkg --print-architecture) signed-by=/etc/apt/keyrings/docker.gpg] https://download.docker.com/linux/ubuntu $(lsb_release -cs) stable" | tee /etc/apt/sources.list.d/docker.list > /dev/null \
|
||||
&& DEBIAN_FRONTEND="noninteractive" apt-get update \
|
||||
&& DEBIAN_FRONTEND="noninteractive" apt-get install --yes \
|
||||
bash \
|
||||
build-essential \
|
||||
containerd.io \
|
||||
docker-ce \
|
||||
docker-ce-cli \
|
||||
docker-compose-plugin \
|
||||
dos2unix \
|
||||
exiftool \
|
||||
libx11-6 \
|
||||
locales \
|
||||
m4 \
|
||||
pkg-config \
|
||||
python3 \
|
||||
python3-pip \
|
||||
python3-venv \
|
||||
software-properties-common \
|
||||
sudo \
|
||||
unzip \
|
||||
wget \
|
||||
zip \
|
||||
# Install latest Git using their official PPA
|
||||
&& add-apt-repository ppa:git-core/ppa \
|
||||
&& DEBIAN_FRONTEND="noninteractive" apt-get install --yes git \
|
||||
&& apt-get clean && rm -rf /var/lib/apt/lists/*
|
||||
|
||||
# Enables Docker starting with systemd
|
||||
RUN systemctl enable docker
|
||||
|
||||
# Make typing unicode characters in the terminal work.
|
||||
ENV LANG=C.UTF-8 \
|
||||
LC_ALL=C.UTF-8
|
||||
@@ -0,0 +1,11 @@
|
||||
FROM ghcr.io/nationalsecurityagency/foundation/base:latest
|
||||
|
||||
COPY --from=ghcr.io/galoisinc/crux-mir:latest --chown=root:root /home/crux-mir/.cargo/* /usr/local/bin/
|
||||
COPY --from=ghcr.io/galoisinc/crux-mir:latest --chown=root:root /home/crux-mir/.rustup /usr/local/rustup
|
||||
COPY --from=ghcr.io/galoisinc/crux-mir:latest /usr/local/bin/* /usr/local/bin/
|
||||
COPY --from=ghcr.io/galoisinc/crux-mir:latest /crux-mir/rlibs /crux-mir/rlibs
|
||||
|
||||
ENV CARGO_HOME=/usr/local/cargo \
|
||||
RUSTUP_HOME=/usr/local/rustup \
|
||||
CRUX_RUST_LIBRARY_PATH=/crux-mir/rlibs \
|
||||
LD_LIBRARY_PATH=/usr/local/lib:/usr/local/rustup/lib
|
||||
@@ -0,0 +1,21 @@
|
||||
FROM ghcr.io/nationalsecurityagency/foundation/base:latest
|
||||
|
||||
# Setup global install for cargo, rustup, and kani.
|
||||
RUN mkdir /usr/local/share/.rustup
|
||||
ENV RUSTUP_HOME=/usr/local/share/.rustup
|
||||
|
||||
RUN mkdir /usr/local/share/.cargo
|
||||
ENV CARGO_HOME=/usr/local/share/.cargo
|
||||
|
||||
RUN mkdir /usr/local/share/.kani
|
||||
ENV KANI_HOME=/usr/local/share/.kani
|
||||
|
||||
# Add various bins to PATH
|
||||
ENV PATH="${CARGO_HOME}/bin:${RUSTUP_HOME}/bin:${KANI_HOME}/bin:${PATH}"
|
||||
|
||||
# Get Rust, Kani, and Bolero
|
||||
RUN curl https://sh.rustup.rs -sSf | bash -s -- -y \
|
||||
&& cargo install --locked kani-verifier \
|
||||
&& cargo kani setup \
|
||||
&& cargo install cargo-bolero \
|
||||
&& chmod a+rw -R /usr/local/share/.cargo /usr/local/share/.rustup /usr/local/share/.kani
|
||||
@@ -0,0 +1,20 @@
|
||||
FROM ghcr.io/nationalsecurityagency/foundation/base:latest
|
||||
|
||||
RUN apt-get update -y \
|
||||
&& DEBIAN_FRONTEND="noninteractive" apt-get install -y \
|
||||
make \
|
||||
cmake \
|
||||
libgmp-dev \
|
||||
libssl-dev \
|
||||
libgomp1 \
|
||||
libnuma-dev \
|
||||
autoconf \
|
||||
build-essential \
|
||||
clang-18 \
|
||||
clang-tools-18 \
|
||||
clang-format-18 \
|
||||
&& apt-get clean && rm -rf /var/lib/apt/lists/*
|
||||
|
||||
# Link clang-18 utils
|
||||
|
||||
RUN find /usr/bin/ -name "*-18" -exec basename {} \; | sed "s/\-18//" | xargs -I{} ln -s /usr/bin/'{}'-18 /usr/bin/'{}'
|
||||
@@ -0,0 +1,48 @@
|
||||
FROM ghcr.io/nationalsecurityagency/foundation/cryptol-tools:latest
|
||||
|
||||
# Install some tools to assist with development.
|
||||
RUN apt-get update -y \
|
||||
&& DEBIAN_FRONTEND="noninteractive" apt-get install -y \
|
||||
vim \
|
||||
openssh-client \
|
||||
bash-completion \
|
||||
htop \
|
||||
man \
|
||||
graphviz \
|
||||
make \
|
||||
cmake \
|
||||
libgmp-dev \
|
||||
libssl-dev \
|
||||
libgomp1 \
|
||||
libnuma-dev \
|
||||
autoconf \
|
||||
build-essential \
|
||||
clang-18 \
|
||||
clang-tools-18 \
|
||||
clang-format-18 \
|
||||
emacs \
|
||||
&& apt-get clean && rm -rf /var/lib/apt/lists/*
|
||||
|
||||
# Link clang-18 utils
|
||||
|
||||
RUN find /usr/bin/ -name "*-18" -exec basename {} \; | sed "s/\-18//" | xargs -I{} ln -s /usr/bin/'{}'-18 /usr/bin/'{}'
|
||||
|
||||
# Setup global install for cargo, rustup, and kani.
|
||||
RUN mkdir /usr/local/share/.rustup
|
||||
ENV RUSTUP_HOME=/usr/local/share/.rustup
|
||||
|
||||
RUN mkdir /usr/local/share/.cargo
|
||||
ENV CARGO_HOME=/usr/local/share/.cargo
|
||||
|
||||
RUN mkdir /usr/local/share/.kani
|
||||
ENV KANI_HOME=/usr/local/share/.kani
|
||||
|
||||
# Add various bins to PATH
|
||||
ENV PATH="${CARGO_HOME}/bin:${RUSTUP_HOME}/bin:${KANI_HOME}/bin:${PATH}"
|
||||
|
||||
# Get Rust, Kani, and Bolero
|
||||
RUN curl https://sh.rustup.rs -sSf | bash -s -- -y \
|
||||
&& cargo install --locked kani-verifier \
|
||||
&& cargo kani setup \
|
||||
&& cargo install cargo-bolero \
|
||||
&& chmod a+rw -R /usr/local/share/.cargo /usr/local/share/.rustup /usr/local/share/.kani
|
||||
@@ -0,0 +1,10 @@
|
||||
FROM ghcr.io/nationalsecurityagency/foundation/base:latest
|
||||
|
||||
# Install Python client for Cryptol in a virtual environment
|
||||
ENV VENV_CRYPTOL=/opt/venv/cryptol-remote-api
|
||||
RUN python3 -m venv $VENV_CRYPTOL \
|
||||
&& $VENV_CRYPTOL/bin/pip --no-cache-dir install pyparsing tabulate numpy scipy "https://github.com/GaloisInc/cryptol/archive/refs/heads/master.tar.gz#subdirectory=cryptol-remote-api/python"
|
||||
|
||||
RUN useradd -m cryptol && chown -R cryptol:cryptol /home/cryptol
|
||||
USER cryptol
|
||||
WORKDIR /home/cryptol
|
||||
@@ -0,0 +1,5 @@
|
||||
FROM ghcr.io/galoisinc/cryptol-remote-api:latest
|
||||
|
||||
CMD ["--max-occupancy", "10", "http", "--host", "0.0.0.0", "--port", "8080", "/"]
|
||||
|
||||
EXPOSE 8080
|
||||
@@ -0,0 +1,56 @@
|
||||
FROM ghcr.io/nationalsecurityagency/foundation/base:latest
|
||||
|
||||
RUN apt-get update \
|
||||
&& DEBIAN_FRONTEND="noninteractive" apt-get install --yes \
|
||||
# cryptol and saw deps
|
||||
libgmp-dev \
|
||||
libssl-dev \
|
||||
libgomp1 \
|
||||
libffi8 \
|
||||
libncurses6 \
|
||||
libtinfo6 \
|
||||
libreadline8 \
|
||||
libnuma-dev \
|
||||
openssl \
|
||||
openjdk-11-jdk-headless \
|
||||
# qbf-tools
|
||||
libglpk40 \
|
||||
libboost-iostreams1.74.0 \
|
||||
libboost-program-options1.74.0 \
|
||||
libreadline8 \
|
||||
&& apt-get clean && rm -rf /var/lib/apt/lists/*
|
||||
|
||||
# Install SAW and saw-remote-api
|
||||
COPY --from=ghcr.io/galoisinc/saw:latest /usr/local/bin /usr/local/bin
|
||||
COPY --from=ghcr.io/galoisinc/saw-remote-api:latest /usr/local/bin/saw-remote-api /usr/local/bin/saw-remote-api
|
||||
ENV SAW_SERVER_URL=http://0.0.0.0:36691
|
||||
RUN echo 'saw-remote-api --read-only http --host 0.0.0.0 --port 36691 / &' >> /usr/local/bin/start-saw-remote-api-read-only \
|
||||
&& echo 'saw-remote-api http --host 0.0.0.0 --port 36691 / &' >> /usr/local/bin/start-saw-remote-api \
|
||||
&& chmod a+x /usr/local/bin/start-saw-remote-api /usr/local/bin/start-saw-remote-api-read-only
|
||||
|
||||
# Install Cryptol and cryptol-remote-api
|
||||
COPY --from=ghcr.io/galoisinc/cryptol:latest /usr/local/bin /usr/local/bin
|
||||
COPY --from=ghcr.io/galoisinc/cryptol-remote-api:latest /usr/local/bin/cryptol-remote-api /usr/local/bin/cryptol-remote-api
|
||||
ENV CRYPTOL_SERVER_URL=http://0.0.0.0:36681
|
||||
RUN echo 'cryptol-remote-api --read-only --max-occupancy 10 http --host 0.0.0.0 --port 36681 / &' >> /usr/local/bin/start-cryptol-remote-api-read-only \
|
||||
&& echo 'cryptol-remote-api --max-occupancy 10 http --host 0.0.0.0 --port 36681 / &' >> /usr/local/bin/start-cryptol-remote-api \
|
||||
&& chmod a+x /usr/local/bin/start-cryptol-remote-api /usr/local/bin/start-cryptol-remote-api-read-only
|
||||
|
||||
# Add --no-call-stacks option to cryptol interpreter
|
||||
RUN mv /usr/local/bin/cryptol /usr/local/bin/_cryptol \
|
||||
&& echo '/usr/local/bin/_cryptol --no-call-stacks $@' > /usr/local/bin/cryptol \
|
||||
&& chmod a+x /usr/local/bin/cryptol
|
||||
|
||||
# Get latest what4-solvers compiled for ubuntu
|
||||
RUN wget https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20260622/ubuntu-24.04-X64-bin.zip \
|
||||
&& unzip -o ubuntu-24.04-X64-bin.zip -d /usr/local/bin \
|
||||
&& rm -rf ubuntu-24.04-X64-bin.zip \
|
||||
&& chmod a+x /usr/local/bin/*
|
||||
|
||||
# Install Python clients for Cryptol and SAW in virtual environments
|
||||
ENV VENV_CRYPTOL=/opt/venv/cryptol-remote-api
|
||||
ENV VENV_SAW=/opt/venv/saw-remote-api
|
||||
RUN python3 -m venv $VENV_CRYPTOL \
|
||||
&& $VENV_CRYPTOL/bin/pip --no-cache-dir install pyparsing tabulate numpy scipy "https://github.com/GaloisInc/cryptol/archive/refs/heads/master.tar.gz#subdirectory=cryptol-remote-api/python" \
|
||||
&& python3 -m venv $VENV_SAW \
|
||||
&& $VENV_SAW/bin/pip --no-cache-dir install pyparsing tabulate numpy scipy "https://github.com/GaloisInc/saw-script/archive/refs/heads/master.tar.gz#subdirectory=saw-python"
|
||||
@@ -0,0 +1,25 @@
|
||||
FROM ghcr.io/nationalsecurityagency/foundation/base:latest
|
||||
|
||||
RUN apt-get update \
|
||||
&& DEBIAN_FRONTEND="noninteractive" apt-get install --yes \
|
||||
libgmp10 \
|
||||
libgomp1 \
|
||||
libffi8 \
|
||||
wget \
|
||||
libncurses6 \
|
||||
unzip \
|
||||
libreadline-dev \
|
||||
openjdk-11-jdk-headless \
|
||||
&& apt-get clean && rm -rf /var/lib/apt/lists/*
|
||||
|
||||
COPY --from=ghcr.io/galoisinc/saw:latest /usr/local/bin /usr/local/bin
|
||||
COPY --from=ghcr.io/galoisinc/saw-remote-api:latest /usr/local/bin/saw-remote-api /usr/local/bin/saw-remote-api
|
||||
|
||||
# Install Python client for SAW in a virtual environment
|
||||
ENV VENV_SAW=/opt/venv/saw-remote-api
|
||||
RUN python3 -m venv $VENV_SAW \
|
||||
&& $VENV_SAW/bin/pip --no-cache-dir install pyparsing tabulate numpy scipy "https://github.com/GaloisInc/saw-script/archive/refs/heads/master.tar.gz#subdirectory=saw-python"
|
||||
|
||||
RUN useradd -m saw && chown -R saw:saw /home/saw
|
||||
USER saw
|
||||
WORKDIR /home/saw
|
||||
@@ -0,0 +1,3 @@
|
||||
FROM ghcr.io/nationalsecurityagency/foundation/foundation-saw-base:latest
|
||||
|
||||
ADD foundation.tar .
|
||||
@@ -0,0 +1,3 @@
|
||||
FROM ghcr.io/nationalsecurityagency/foundation/cryptol-remote-api:latest
|
||||
|
||||
ADD foundation.tar .
|
||||
@@ -0,0 +1,38 @@
|
||||
FROM ghcr.io/nationalsecurityagency/foundation/cryptol-tools:latest
|
||||
|
||||
# Install some tools to assist with development.
|
||||
RUN apt-get update -y \
|
||||
&& DEBIAN_FRONTEND="noninteractive" apt-get install -y \
|
||||
vim \
|
||||
openssh-client \
|
||||
bash-completion \
|
||||
htop \
|
||||
man \
|
||||
graphviz \
|
||||
make \
|
||||
cmake \
|
||||
libgmp-dev \
|
||||
libssl-dev \
|
||||
libgomp1 \
|
||||
libnuma-dev \
|
||||
autoconf \
|
||||
build-essential \
|
||||
clang-18 \
|
||||
clang-tools-18 \
|
||||
clang-format-18 \
|
||||
emacs \
|
||||
&& apt-get clean && rm -rf /var/lib/apt/lists/*
|
||||
|
||||
# Link clang-18 utils
|
||||
|
||||
RUN find /usr/bin/ -name "*-18" -exec basename {} \; | sed "s/\-18//" | xargs -I{} ln -s /usr/bin/'{}'-18 /usr/bin/'{}'
|
||||
|
||||
COPY --from=ghcr.io/galoisinc/crux-mir:latest --chown=root:root /home/crux-mir/.cargo/* /usr/local/bin/
|
||||
COPY --from=ghcr.io/galoisinc/crux-mir:latest --chown=root:root /home/crux-mir/.rustup /usr/local/rustup
|
||||
COPY --from=ghcr.io/galoisinc/crux-mir:latest /usr/local/bin/* /usr/local/bin/
|
||||
COPY --from=ghcr.io/galoisinc/crux-mir:latest /crux-mir/rlibs /crux-mir/rlibs
|
||||
|
||||
ENV CARGO_HOME=/usr/local/cargo \
|
||||
RUSTUP_HOME=/usr/local/rustup \
|
||||
CRUX_RUST_LIBRARY_PATH=/crux-mir/rlibs \
|
||||
LD_LIBRARY_PATH=/usr/local/lib:/usr/local/rustup/lib
|
||||
@@ -0,0 +1,10 @@
|
||||
FROM ghcr.io/nationalsecurityagency/foundation/base:latest
|
||||
|
||||
# Install Python client for SAW in a virtual environment
|
||||
ENV VENV_SAW=/opt/venv/saw-remote-api
|
||||
RUN python3 -m venv $VENV_SAW \
|
||||
&& $VENV_SAW/bin/pip --no-cache-dir install pyparsing tabulate numpy scipy "https://github.com/GaloisInc/saw-script/archive/refs/heads/master.tar.gz#subdirectory=saw-python"
|
||||
|
||||
RUN useradd -m saw && chown -R saw:saw /home/saw
|
||||
USER saw
|
||||
WORKDIR /home/saw
|
||||
@@ -0,0 +1,5 @@
|
||||
FROM ghcr.io/galoisinc/saw-remote-api:latest
|
||||
|
||||
CMD ["http", "--host", "0.0.0.0", "--port", "8080", "/"]
|
||||
|
||||
EXPOSE 8080
|
||||
@@ -0,0 +1 @@
|
||||
FROM ghcr.io/galoisinc/saw:latest
|
||||
@@ -0,0 +1,41 @@
|
||||
# GitHub Workflows
|
||||
|
||||
## Infrastructure
|
||||
|
||||
Workflows prefixed with `infrastructure` contain GitHub Actions for
|
||||
building the suite of Docker images needed to maintain assurance of
|
||||
the various components of this repository (specifications, reference
|
||||
implementations, etc.). Also included here are workflows for building
|
||||
a development Docker image suitable for use with a containerized
|
||||
development environment.
|
||||
|
||||
### Updating the Infrastructure
|
||||
|
||||
These workflows may be started manually, for example, when a new
|
||||
version of some tool (such as Cryptol) is released. Before running
|
||||
these workflows on the `main` branch, they should first be tested in a
|
||||
new branch and any issues resolved in a pull request to the point that
|
||||
all CI tests pass.
|
||||
|
||||
## Release
|
||||
|
||||
Workflows prefixed with `release` contain GitHub Actions for building
|
||||
Docker images containing the `foundation` project as well as tooling
|
||||
needed to interact with the project in the various workflows here that
|
||||
create assurance artifacts.
|
||||
|
||||
## Assurance
|
||||
|
||||
Workflows prefixed with `assurance` contain GitHub Actions that levy
|
||||
invariants on and create assurance artifacts from the project.
|
||||
|
||||
## Cleanup
|
||||
|
||||
Workflows prefixed with `cleanup` contain GitHub Actions for cleaning
|
||||
up the repository.
|
||||
|
||||
### Registry
|
||||
|
||||
All images built here are stored in [GitHub's container registry for
|
||||
this `foundation`
|
||||
project](https://github.com/orgs/NationalSecurityAgency/packages?tab=packages&q=foundation).
|
||||
@@ -0,0 +1,86 @@
|
||||
name: Create assurance artifacts
|
||||
|
||||
on:
|
||||
pull_request:
|
||||
push:
|
||||
branches:
|
||||
- 'main'
|
||||
schedule:
|
||||
- cron: '0 22 * * *'
|
||||
|
||||
env:
|
||||
CRYPTOL_SERVER_URL: 'http://foundation:8080'
|
||||
SAW_SERVER_URL: 'http://localhost:8080'
|
||||
SAW_SOLVER_CACHE_PATH: 'saw-cache'
|
||||
VENV_CRYPTOL: '/opt/venv/cryptol-remote-api'
|
||||
VENV_SAW: '/opt/venv/saw-remote-api'
|
||||
|
||||
jobs:
|
||||
|
||||
# This job builds the foundation image for this pipeline.
|
||||
build-foundation-image:
|
||||
uses: ./.github/workflows/release-build-foundation-image.yml
|
||||
with:
|
||||
sha: ${{ github.sha }}
|
||||
|
||||
# This job attempts to load all Cryptol files in foundation.
|
||||
load-all-cry-files:
|
||||
needs: build-foundation-image
|
||||
runs-on: ubuntu-latest
|
||||
container: ghcr.io/nationalsecurityagency/foundation/cryptol-remote-api-client:latest
|
||||
services:
|
||||
foundation:
|
||||
image: ghcr.io/nationalsecurityagency/foundation/foundation:${{ github.sha }}
|
||||
ports:
|
||||
- 8080:8080
|
||||
steps:
|
||||
- name: Check out code
|
||||
uses: actions/checkout@v7
|
||||
- name: Run python script to load all Cryptol files in virtual environment for Cryptol Remote API
|
||||
run: $VENV_CRYPTOL/bin/python3 .ci/load-all-cry-files.py
|
||||
|
||||
# This job attempts to run top-level SAW files in foundation.
|
||||
load-top-level-SAW-files:
|
||||
needs: build-foundation-image
|
||||
runs-on: ubuntu-latest
|
||||
container: ghcr.io/nationalsecurityagency/foundation/foundation-saw:${{ github.sha }}
|
||||
steps:
|
||||
- name: Prefix 'pwd' onto SAW_SOLVER_CACHE_PATH
|
||||
run: echo "SAW_SOLVER_CACHE_PATH=/home/saw/$SAW_SOLVER_CACHE_PATH" >> $GITHUB_ENV
|
||||
- name: Restore SAW proof cache
|
||||
uses: actions/cache/restore@v6
|
||||
with:
|
||||
path: ${{ env.SAW_SOLVER_CACHE_PATH }}
|
||||
key: ${{ github.ref_name }}-saw-cache-${{ github.sha }}
|
||||
restore-keys: |
|
||||
${{ github.ref_name }}-saw-cache-
|
||||
main-saw-cache-
|
||||
- name: Clean SAW proof cache
|
||||
run: saw --clean-mismatched-versions-solver-cache
|
||||
- name: Run top-level SAW files.
|
||||
working-directory: /home/saw
|
||||
run: .ci/run-top-level-saw-files.sh
|
||||
|
||||
# This job attempts to run top-level SAW python files in foundation.
|
||||
load-top-level-SAW-python-files:
|
||||
needs: build-foundation-image
|
||||
runs-on: ubuntu-latest
|
||||
container: ghcr.io/nationalsecurityagency/foundation/foundation-saw:${{ github.sha }}
|
||||
steps:
|
||||
- name: Prefix 'pwd' onto SAW_SOLVER_CACHE_PATH
|
||||
run: echo "SAW_SOLVER_CACHE_PATH=/home/saw/$SAW_SOLVER_CACHE_PATH" >> $GITHUB_ENV
|
||||
- name: Restore SAW proof cache
|
||||
uses: actions/cache/restore@v6
|
||||
with:
|
||||
path: ${{ env.SAW_SOLVER_CACHE_PATH }}
|
||||
key: ${{ github.ref_name }}-saw-rust-cache-${{ github.sha }}
|
||||
restore-keys: |
|
||||
${{ github.ref_name }}-saw-rust-cache-
|
||||
main-saw-rust-cache-
|
||||
- name: Clean SAW proof cache
|
||||
run: saw --clean-mismatched-versions-solver-cache
|
||||
- name: Run top-level SAW python files.
|
||||
working-directory: /home/saw
|
||||
run: |
|
||||
saw-remote-api http --host 0.0.0.0 --port 8080 / &
|
||||
.ci/run-saw-python-files.sh
|
||||
@@ -0,0 +1,33 @@
|
||||
name: Cleanup caches when a branch is closed
|
||||
on:
|
||||
pull_request:
|
||||
types:
|
||||
- closed
|
||||
|
||||
jobs:
|
||||
cleanup:
|
||||
runs-on: ubuntu-latest
|
||||
steps:
|
||||
- name: Check out code
|
||||
uses: actions/checkout@v7
|
||||
|
||||
- name: Cleanup
|
||||
run: |
|
||||
gh extension install actions/gh-actions-cache
|
||||
|
||||
REPO=${{ github.repository }}
|
||||
BRANCH="refs/pull/${{ github.event.pull_request.number }}/merge"
|
||||
|
||||
echo "Fetching list of cache key"
|
||||
cacheKeysForPR=$(gh actions-cache list -R $REPO -B $BRANCH -L 100 | cut -f 1 )
|
||||
|
||||
## Setting this to not fail the workflow while deleting cache keys.
|
||||
set +e
|
||||
echo "Deleting caches..."
|
||||
for cacheKey in $cacheKeysForPR
|
||||
do
|
||||
gh actions-cache delete $cacheKey -R $REPO -B $BRANCH --confirm
|
||||
done
|
||||
echo "Done"
|
||||
env:
|
||||
GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
|
||||
@@ -0,0 +1,42 @@
|
||||
name: Build image template
|
||||
on:
|
||||
workflow_call:
|
||||
inputs:
|
||||
dockerfile:
|
||||
type: string
|
||||
required: true
|
||||
|
||||
jobs:
|
||||
build-layer:
|
||||
runs-on: ubuntu-latest
|
||||
steps:
|
||||
- name: Checkout
|
||||
uses: actions/checkout@v7
|
||||
- name: Set up Docker Buildx
|
||||
uses: docker/setup-buildx-action@v4
|
||||
- name: Login to ghcr.io
|
||||
uses: docker/[email protected]
|
||||
with:
|
||||
registry: ghcr.io
|
||||
username: ${{ github.repository_owner }}
|
||||
password: ${{ secrets.GITHUB_TOKEN }}
|
||||
- name: Build and push to branch
|
||||
uses: docker/build-push-action@v7
|
||||
if: github.ref_name != 'main'
|
||||
with:
|
||||
context: .
|
||||
push: true
|
||||
file: .github/dockerfiles/${{ inputs.dockerfile }}.Dockerfile
|
||||
tags: ghcr.io/nationalsecurityagency/foundation/${{ inputs.dockerfile }}:${{ github.sha }}
|
||||
cache-from: type=gha
|
||||
cache-to: type=gha,mode=min
|
||||
- name: Build and push to main
|
||||
uses: docker/build-push-action@v7
|
||||
if: github.ref_name == 'main'
|
||||
with:
|
||||
context: .
|
||||
push: true
|
||||
file: .github/dockerfiles/${{ inputs.dockerfile }}.Dockerfile
|
||||
tags: ghcr.io/nationalsecurityagency/foundation/${{ inputs.dockerfile }}:latest
|
||||
cache-from: type=gha
|
||||
cache-to: type=gha,mode=min
|
||||
@@ -0,0 +1,80 @@
|
||||
name: Build images
|
||||
|
||||
on:
|
||||
workflow_dispatch:
|
||||
|
||||
jobs:
|
||||
|
||||
base:
|
||||
uses: ./.github/workflows/infrastructure-build-image-template.yml
|
||||
with:
|
||||
dockerfile: "base"
|
||||
|
||||
cryptol-remote-api:
|
||||
uses: ./.github/workflows/infrastructure-build-image-template.yml
|
||||
with:
|
||||
dockerfile: "cryptol-remote-api"
|
||||
|
||||
saw:
|
||||
uses: ./.github/workflows/infrastructure-build-image-template.yml
|
||||
with:
|
||||
dockerfile: "saw"
|
||||
|
||||
saw-remote-api:
|
||||
uses: ./.github/workflows/infrastructure-build-image-template.yml
|
||||
with:
|
||||
dockerfile: "saw-remote-api"
|
||||
|
||||
cryptol-remote-api-client:
|
||||
needs: base
|
||||
uses: ./.github/workflows/infrastructure-build-image-template.yml
|
||||
with:
|
||||
dockerfile: "cryptol-remote-api-client"
|
||||
|
||||
saw-remote-api-client:
|
||||
needs: base
|
||||
uses: ./.github/workflows/infrastructure-build-image-template.yml
|
||||
with:
|
||||
dockerfile: "saw-remote-api-client"
|
||||
|
||||
foundation-saw-base:
|
||||
needs: base
|
||||
uses: ./.github/workflows/infrastructure-build-image-template.yml
|
||||
with:
|
||||
dockerfile: "foundation-saw-base"
|
||||
|
||||
cargo:
|
||||
needs: base
|
||||
uses: ./.github/workflows/infrastructure-build-image-template.yml
|
||||
with:
|
||||
dockerfile: "cargo"
|
||||
|
||||
cargo-saw-build:
|
||||
needs: base
|
||||
uses: ./.github/workflows/infrastructure-build-image-template.yml
|
||||
with:
|
||||
dockerfile: "cargo-saw-build"
|
||||
|
||||
clang:
|
||||
needs: base
|
||||
uses: ./.github/workflows/infrastructure-build-image-template.yml
|
||||
with:
|
||||
dockerfile: "clang"
|
||||
|
||||
cryptol-tools:
|
||||
needs: base
|
||||
uses: ./.github/workflows/infrastructure-build-image-template.yml
|
||||
with:
|
||||
dockerfile: "cryptol-tools"
|
||||
|
||||
cryptol-dev:
|
||||
needs: cryptol-tools
|
||||
uses: ./.github/workflows/infrastructure-build-image-template.yml
|
||||
with:
|
||||
dockerfile: "cryptol-dev"
|
||||
|
||||
saw-dev:
|
||||
needs: cryptol-tools
|
||||
uses: ./.github/workflows/infrastructure-build-image-template.yml
|
||||
with:
|
||||
dockerfile: "saw-dev"
|
||||
@@ -0,0 +1,67 @@
|
||||
name: Build foundation container template
|
||||
|
||||
on:
|
||||
workflow_call:
|
||||
inputs:
|
||||
sha:
|
||||
type: string
|
||||
required: true
|
||||
|
||||
jobs:
|
||||
build-foundation-saw-container:
|
||||
runs-on: ubuntu-latest
|
||||
container:
|
||||
image: ghcr.io/nationalsecurityagency/foundation/cargo-saw-build:latest
|
||||
steps:
|
||||
- name: Check out code
|
||||
uses: actions/checkout@v7
|
||||
- name: Build Rust artifacts for SAW
|
||||
run: .ci/build-rust-saw-artifacts.sh
|
||||
- name: Tar all `.cry`, `.saw`, `linked-mir.json`, and `saw.py` files
|
||||
run: find . -name "*.cry" -or -name "*.saw" -or -name "linked-mir.json" -or -name "saw.py" -or -name "*.sh" | tar -cf foundation.tar -T -
|
||||
- name: Set up Docker Buildx
|
||||
uses: docker/setup-buildx-action@v4
|
||||
- name: Login to ghcr.io
|
||||
uses: docker/[email protected]
|
||||
with:
|
||||
registry: ghcr.io
|
||||
username: ${{ github.repository_owner }}
|
||||
password: ${{ secrets.GITHUB_TOKEN }}
|
||||
- name: Build and push to branch
|
||||
uses: docker/build-push-action@v7
|
||||
with:
|
||||
context: .
|
||||
push: true
|
||||
file: .github/dockerfiles/foundation-saw.Dockerfile
|
||||
tags: ghcr.io/nationalsecurityagency/foundation/foundation-saw:${{ inputs.sha }}
|
||||
cache-from: type=gha
|
||||
cache-to: type=gha,mode=min
|
||||
|
||||
build-foundation-container:
|
||||
runs-on: ubuntu-latest
|
||||
container:
|
||||
image: ghcr.io/nationalsecurityagency/foundation/cargo:latest
|
||||
steps:
|
||||
- name: Check out code
|
||||
uses: actions/checkout@v7
|
||||
- name: Build release Rust for Cryptol FFIs
|
||||
run: .ci/build-rust-ffi.sh
|
||||
- name: Tar all `.cry` and `.so` files
|
||||
run: find . -name "*.cry" -or -name "*.so" | tar -cf foundation.tar -T -
|
||||
- name: Set up Docker Buildx
|
||||
uses: docker/setup-buildx-action@v4
|
||||
- name: Login to ghcr.io
|
||||
uses: docker/[email protected]
|
||||
with:
|
||||
registry: ghcr.io
|
||||
username: ${{ github.repository_owner }}
|
||||
password: ${{ secrets.GITHUB_TOKEN }}
|
||||
- name: Build and push to branch
|
||||
uses: docker/build-push-action@v7
|
||||
with:
|
||||
context: .
|
||||
push: true
|
||||
file: .github/dockerfiles/foundation.Dockerfile
|
||||
tags: ghcr.io/nationalsecurityagency/foundation/foundation:${{ inputs.sha }}
|
||||
cache-from: type=gha
|
||||
cache-to: type=gha,mode=min
|
||||
@@ -0,0 +1,54 @@
|
||||
name: Light-weight Rust checking
|
||||
|
||||
on:
|
||||
pull_request:
|
||||
push:
|
||||
branches:
|
||||
- 'main'
|
||||
|
||||
jobs:
|
||||
|
||||
# This job runs `cargo fmt` on included Rust.
|
||||
cargo-fmt:
|
||||
runs-on: ubuntu-latest
|
||||
container:
|
||||
image: ghcr.io/nationalsecurityagency/foundation/cargo:latest
|
||||
steps:
|
||||
- name: Check out code
|
||||
uses: actions/checkout@v7
|
||||
- name: cargo fmt
|
||||
run: |
|
||||
set -e
|
||||
CARGO_TOML_FILES=`find . -name "Cargo.toml"`
|
||||
for f in $CARGO_TOML_FILES; do cargo fmt --manifest-path $f --all -- --check; done;
|
||||
|
||||
# This job runs `cargo clippy` on included Rust.
|
||||
cargo-clippy:
|
||||
runs-on: ubuntu-latest
|
||||
container:
|
||||
image: ghcr.io/nationalsecurityagency/foundation/cargo:latest
|
||||
steps:
|
||||
- name: Check out code
|
||||
uses: actions/checkout@v7
|
||||
- name: cargo clippy
|
||||
run: |
|
||||
set -e
|
||||
CARGO_TOML_FILES=`find . -name "Cargo.toml"`
|
||||
for f in $CARGO_TOML_FILES; do cargo clippy --manifest-path $f --all-targets --all-features -- -Dclippy::all -Dclippy::pedantic; done;
|
||||
|
||||
# This job runs `cargo test` and `cargo kani` on included Rust.
|
||||
cargo-test:
|
||||
runs-on: ubuntu-latest
|
||||
container:
|
||||
image: ghcr.io/nationalsecurityagency/foundation/cargo:latest
|
||||
steps:
|
||||
- name: Check out code
|
||||
uses: actions/checkout@v7
|
||||
- name: cargo test
|
||||
run: |
|
||||
set -e
|
||||
CARGO_TOML_FILES=`find . -name "Cargo.toml"`
|
||||
for f in $CARGO_TOML_FILES; do cargo test --manifest-path $f --all-targets; \
|
||||
cargo test --manifest-path $f --doc; \
|
||||
# cargo kani --manifest-path $f --output-format=terse; \
|
||||
done;
|
||||
@@ -0,0 +1,3 @@
|
||||
*~
|
||||
\#*\#
|
||||
**/rust/**/target/
|
||||
+164
@@ -0,0 +1,164 @@
|
||||
# Contributors Guide
|
||||
|
||||
Foundation is an open source project. If you are interested in making
|
||||
it better, there are many ways you can contribute. For example, you
|
||||
can:
|
||||
|
||||
- Submit a bug report
|
||||
- Suggest a new feature
|
||||
- Provide feedback by commenting on feature requests/proposals
|
||||
- Propose a patch by submitting a pull request
|
||||
- Suggest or submit documentation improvements
|
||||
- Review outstanding pull requests
|
||||
- Answer questions from other users
|
||||
- Share the software with other users who are interested
|
||||
- Teach others to use the software
|
||||
- Package and distribute the software in a downstream community (such
|
||||
as your preferred Linux distribution)
|
||||
|
||||
## Bugs and Feature Requests
|
||||
|
||||
If you believe that you have found a bug or wish to propose a new
|
||||
feature, please first search the existing [issues] to see if it has
|
||||
already been reported. If you are unable to find an existing issue,
|
||||
consider using one of the provided templates to create a new issue and
|
||||
provide as many details as you can to assist in reproducing the bug or
|
||||
explaining your proposed feature.
|
||||
|
||||
## Patch Submission tips
|
||||
|
||||
Patches should be submitted in the form of Pull Requests to the
|
||||
Foundation [repository] on GitHub. But first, consider the following
|
||||
tips to ensure a smooth process when submitting a patch:
|
||||
|
||||
- Ensure that the patch does not break any continuous integration
|
||||
tests.
|
||||
- Be understanding, patient, and friendly; developers may need time to
|
||||
review your submissions before they can take action or respond. This
|
||||
does not mean your contribution is not valued. If your contribution
|
||||
has not received a response in a reasonable time, consider
|
||||
commenting with a polite inquiry for an update.
|
||||
- Limit your patches to the smallest reasonable change to achieve your
|
||||
intended goal. For example, do not make unnecessary indentation
|
||||
changes; but don't go out of your way to make the patch so minimal
|
||||
that it isn't easy to read, either. Consider the reviewer's
|
||||
perspective.
|
||||
- Unless previously authorized by the Foundation team, repackaging,
|
||||
renaming, and other refactoring should not be part of any pull
|
||||
request. These types of changes are difficult to review, pollute the
|
||||
git history making it harder to do git forensics on regressions, and
|
||||
will likely conflict with other changes that the Foundation team is
|
||||
making internally.
|
||||
- Avoid "find and replace" changes in your pull request. While it may
|
||||
be tempting to globally replace calls to deprecated methods or
|
||||
change the style of the code to fit your personal preference, these
|
||||
types of seemingly trivial changes have likely not already been
|
||||
performed by the Foundation team for good reason.
|
||||
- Focus your patches on bug fixes that were discovered through
|
||||
real-world usage and testing, and on improvements that clearly
|
||||
satisfy a need in Foundation. Before you begin implementing,
|
||||
consider first opening a dialogue with the Foundation team to
|
||||
ensure that your efforts will align with the goals of the
|
||||
project. This will significantly improve the odds that your patch
|
||||
gets accepted.
|
||||
- Unless it addresses a critical security update, avoid pull requests
|
||||
that update the continuous integration pipeline or 3rd party
|
||||
libraries. It is preferred that these changes are made internally by
|
||||
the team. If you have a need for an updated library, please submit
|
||||
an issue with your request instead of a pull request.
|
||||
- Before submission, please squash your commits to using a message
|
||||
that starts with the issue number and a description of the changes.
|
||||
- Isolate multiple patches from each other. If you wish to make
|
||||
several independent patches, do so in separate, smaller pull
|
||||
requests that can be reviewed more easily.
|
||||
- Be prepared to answer questions from reviewers. They may have
|
||||
further questions before accepting your patch, and may even propose
|
||||
changes. Please accept this feedback constructively, and not as a
|
||||
rejection of your proposed change.
|
||||
|
||||
## Review
|
||||
|
||||
- We welcome code reviews from anyone. A contributor is required to
|
||||
formally accept and merge the changes.
|
||||
- Reviewers will be looking for things like readability and code
|
||||
style, assurance and performance implications, API design,
|
||||
duplication of existing functionality, avoidance of bloat
|
||||
(scope-creep), etc.
|
||||
- Reviewers will likely ask questions to better understand your
|
||||
change.
|
||||
- Reviewers will make comments about changes to your patch:
|
||||
- MUST means that the change is required
|
||||
- SHOULD means that the change is suggested, further discussion on
|
||||
the subject may be required
|
||||
- COULD means that the change is optional.
|
||||
|
||||
## Getting Started
|
||||
|
||||
Please see the [developer guide][devguide] for instructions to set up
|
||||
a suitable development environment.
|
||||
|
||||
## Timeline and Managing Expectations
|
||||
|
||||
As we continue to engage contributors and learn best practices for
|
||||
running a successful open source project, our processes and guidance
|
||||
will likely evolve. We will try to communicate expectations as we are
|
||||
able and to always be responsive. We hope that the community will
|
||||
share their suggestions for improving this engagement. Based on the
|
||||
level of initial interest we receive and the availability of resources
|
||||
to evaluate contributions, we anticipate the following:
|
||||
|
||||
- We will initially prioritize pull requests that include small bug
|
||||
fixes and code that addresses potential vulnerabilities as well as
|
||||
pull requests that include existing specifications because these
|
||||
require a reasonable amount of effort to evaluate and will help us
|
||||
exercise and revise our process for accepting contributions. In
|
||||
other words, we are going to start small in order to work out the
|
||||
kinks first.
|
||||
- We are committed to maintaining the integrity and security of our
|
||||
code base. In addition to the careful review the maintainers will
|
||||
give to code contributions to make sure they do not introduce new
|
||||
bugs or vulnerabilities, we will be trying to identify best
|
||||
practices to incorporate with our open source project so that
|
||||
contributors can have more control over whether their contributions
|
||||
are accepted. These might include things like style guides and
|
||||
requirements for tests and documentation to accompany some code
|
||||
contributions. As a result, it may take a long time for some
|
||||
contributions to be accepted. This does not mean we are ignoring
|
||||
them.
|
||||
- We are committed to integrating this GitHub project with our team's
|
||||
regular development work flow so that the open source project
|
||||
remains dynamic and relevant. This may affect our responsiveness
|
||||
and ability to accept pull requests quickly. This does not mean we
|
||||
are ignoring them.
|
||||
- Not all innovative ideas need to be accepted as pull requests into
|
||||
this GitHub project to be valuable to the community. There may be
|
||||
times when we recommend that you just share your code for some
|
||||
enhancement to Foundation from your own repository. As we identify
|
||||
and recognize extensions that are of general interest to the
|
||||
cryptographic assurance community, we may seek to incorporate them
|
||||
with our baseline.
|
||||
|
||||
## Legal
|
||||
|
||||
Consistent with Section D.6. of the GitHub Terms of Service as of
|
||||
2019, and Section 5. of the Apache License, Version 2.0, the project
|
||||
maintainer for this project accepts contributions using the
|
||||
inbound=outbound model. When you submit a pull request to this
|
||||
repository (inbound), you are agreeing to license your contribution
|
||||
under the same terms as specified in [LICENSE] (outbound).
|
||||
|
||||
This is an open source project. Contributions you make to this public
|
||||
U.S. Government ("USG") repository are completely voluntary. When you
|
||||
submit an issue, bug report, question, enhancement, pull request,
|
||||
etc., you are offering your contribution without expectation of
|
||||
payment, you expressly waive any future pay claims against the USG
|
||||
related to your contribution, and you acknowledge that this does not
|
||||
create an obligation on the part of the USG of any kind. Furthermore,
|
||||
your contributing to this project does not create an employer-employee
|
||||
relationship between the United States ("U.S.") Government and the
|
||||
contributor.
|
||||
|
||||
[issues]: https://github.com/NationalSecurityAgency/foundation/issues
|
||||
[repository]: https://github.com/NationalSecurityAgency/foundation/
|
||||
[devguide]: docs/DevGuide.md
|
||||
[LICENSE]: LICENSE
|
||||
@@ -0,0 +1,35 @@
|
||||
# Disclaimer of Warranty
|
||||
|
||||
This Work is provided "AS IS." Any express or implied warranties,
|
||||
including but not limited to, the implied warranties of
|
||||
merchantability and fitness for a particular purpose are disclaimed.
|
||||
In no event shall the United States Government be liable for any
|
||||
direct, indirect, incidental, special, exemplary or consequential
|
||||
damages (including, but not limited to, procurement of substitute
|
||||
goods or services, loss of use, data or profits, or business
|
||||
interruption) however caused and on any theory of liability, whether
|
||||
in contract, strict liability, or tort (including negligence or
|
||||
otherwise) arising in any way out of the use of this Work, even if
|
||||
advised of the possibility of such damage.
|
||||
|
||||
The User of this Work agrees to hold harmless and indemnify the United
|
||||
States Government, its agents and employees from every claim or
|
||||
liability (whether in tort or in contract), including attorney's fees,
|
||||
court costs, and expenses, arising in direct consequence of
|
||||
Recipient's use of the item, including, but not limited to, claims or
|
||||
liabilities made for injury to or death of personnel of User or third
|
||||
parties, damage to or destruction of property of User or third
|
||||
parties, and infringement or other violations of intellectual property
|
||||
or technical data rights.
|
||||
|
||||
# Disclaimer of Endorsement
|
||||
|
||||
Nothing in this Work is intended to constitute an endorsement,
|
||||
explicit or implied, by the United States Government of any particular
|
||||
manufacturer's product or service.
|
||||
|
||||
Reference herein to any specific commercial product, process, or
|
||||
service by trade name, trademark, manufacturer, or otherwise, in this
|
||||
Work does not constitute an endorsement, recommendation, or favoring
|
||||
by the United States Government and shall not be used for advertising
|
||||
or product endorsement purposes.
|
||||
@@ -0,0 +1,201 @@
|
||||
Apache License
|
||||
Version 2.0, January 2004
|
||||
http://www.apache.org/licenses/
|
||||
|
||||
TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
|
||||
|
||||
1. Definitions.
|
||||
|
||||
"License" shall mean the terms and conditions for use, reproduction,
|
||||
and distribution as defined by Sections 1 through 9 of this document.
|
||||
|
||||
"Licensor" shall mean the copyright owner or entity authorized by
|
||||
the copyright owner that is granting the License.
|
||||
|
||||
"Legal Entity" shall mean the union of the acting entity and all
|
||||
other entities that control, are controlled by, or are under common
|
||||
control with that entity. For the purposes of this definition,
|
||||
"control" means (i) the power, direct or indirect, to cause the
|
||||
direction or management of such entity, whether by contract or
|
||||
otherwise, or (ii) ownership of fifty percent (50%) or more of the
|
||||
outstanding shares, or (iii) beneficial ownership of such entity.
|
||||
|
||||
"You" (or "Your") shall mean an individual or Legal Entity
|
||||
exercising permissions granted by this License.
|
||||
|
||||
"Source" form shall mean the preferred form for making modifications,
|
||||
including but not limited to software source code, documentation
|
||||
source, and configuration files.
|
||||
|
||||
"Object" form shall mean any form resulting from mechanical
|
||||
transformation or translation of a Source form, including but
|
||||
not limited to compiled object code, generated documentation,
|
||||
and conversions to other media types.
|
||||
|
||||
"Work" shall mean the work of authorship, whether in Source or
|
||||
Object form, made available under the License, as indicated by a
|
||||
copyright notice that is included in or attached to the work
|
||||
(an example is provided in the Appendix below).
|
||||
|
||||
"Derivative Works" shall mean any work, whether in Source or Object
|
||||
form, that is based on (or derived from) the Work and for which the
|
||||
editorial revisions, annotations, elaborations, or other modifications
|
||||
represent, as a whole, an original work of authorship. For the purposes
|
||||
of this License, Derivative Works shall not include works that remain
|
||||
separable from, or merely link (or bind by name) to the interfaces of,
|
||||
the Work and Derivative Works thereof.
|
||||
|
||||
"Contribution" shall mean any work of authorship, including
|
||||
the original version of the Work and any modifications or additions
|
||||
to that Work or Derivative Works thereof, that is intentionally
|
||||
submitted to Licensor for inclusion in the Work by the copyright owner
|
||||
or by an individual or Legal Entity authorized to submit on behalf of
|
||||
the copyright owner. For the purposes of this definition, "submitted"
|
||||
means any form of electronic, verbal, or written communication sent
|
||||
to the Licensor or its representatives, including but not limited to
|
||||
communication on electronic mailing lists, source code control systems,
|
||||
and issue tracking systems that are managed by, or on behalf of, the
|
||||
Licensor for the purpose of discussing and improving the Work, but
|
||||
excluding communication that is conspicuously marked or otherwise
|
||||
designated in writing by the copyright owner as "Not a Contribution."
|
||||
|
||||
"Contributor" shall mean Licensor and any individual or Legal Entity
|
||||
on behalf of whom a Contribution has been received by Licensor and
|
||||
subsequently incorporated within the Work.
|
||||
|
||||
2. Grant of Copyright License. Subject to the terms and conditions of
|
||||
this License, each Contributor hereby grants to You a perpetual,
|
||||
worldwide, non-exclusive, no-charge, royalty-free, irrevocable
|
||||
copyright license to reproduce, prepare Derivative Works of,
|
||||
publicly display, publicly perform, sublicense, and distribute the
|
||||
Work and such Derivative Works in Source or Object form.
|
||||
|
||||
3. Grant of Patent License. Subject to the terms and conditions of
|
||||
this License, each Contributor hereby grants to You a perpetual,
|
||||
worldwide, non-exclusive, no-charge, royalty-free, irrevocable
|
||||
(except as stated in this section) patent license to make, have made,
|
||||
use, offer to sell, sell, import, and otherwise transfer the Work,
|
||||
where such license applies only to those patent claims licensable
|
||||
by such Contributor that are necessarily infringed by their
|
||||
Contribution(s) alone or by combination of their Contribution(s)
|
||||
with the Work to which such Contribution(s) was submitted. If You
|
||||
institute patent litigation against any entity (including a
|
||||
cross-claim or counterclaim in a lawsuit) alleging that the Work
|
||||
or a Contribution incorporated within the Work constitutes direct
|
||||
or contributory patent infringement, then any patent licenses
|
||||
granted to You under this License for that Work shall terminate
|
||||
as of the date such litigation is filed.
|
||||
|
||||
4. Redistribution. You may reproduce and distribute copies of the
|
||||
Work or Derivative Works thereof in any medium, with or without
|
||||
modifications, and in Source or Object form, provided that You
|
||||
meet the following conditions:
|
||||
|
||||
(a) You must give any other recipients of the Work or
|
||||
Derivative Works a copy of this License; and
|
||||
|
||||
(b) You must cause any modified files to carry prominent notices
|
||||
stating that You changed the files; and
|
||||
|
||||
(c) You must retain, in the Source form of any Derivative Works
|
||||
that You distribute, all copyright, patent, trademark, and
|
||||
attribution notices from the Source form of the Work,
|
||||
excluding those notices that do not pertain to any part of
|
||||
the Derivative Works; and
|
||||
|
||||
(d) If the Work includes a "NOTICE" text file as part of its
|
||||
distribution, then any Derivative Works that You distribute must
|
||||
include a readable copy of the attribution notices contained
|
||||
within such NOTICE file, excluding those notices that do not
|
||||
pertain to any part of the Derivative Works, in at least one
|
||||
of the following places: within a NOTICE text file distributed
|
||||
as part of the Derivative Works; within the Source form or
|
||||
documentation, if provided along with the Derivative Works; or,
|
||||
within a display generated by the Derivative Works, if and
|
||||
wherever such third-party notices normally appear. The contents
|
||||
of the NOTICE file are for informational purposes only and
|
||||
do not modify the License. You may add Your own attribution
|
||||
notices within Derivative Works that You distribute, alongside
|
||||
or as an addendum to the NOTICE text from the Work, provided
|
||||
that such additional attribution notices cannot be construed
|
||||
as modifying the License.
|
||||
|
||||
You may add Your own copyright statement to Your modifications and
|
||||
may provide additional or different license terms and conditions
|
||||
for use, reproduction, or distribution of Your modifications, or
|
||||
for any such Derivative Works as a whole, provided Your use,
|
||||
reproduction, and distribution of the Work otherwise complies with
|
||||
the conditions stated in this License.
|
||||
|
||||
5. Submission of Contributions. Unless You explicitly state otherwise,
|
||||
any Contribution intentionally submitted for inclusion in the Work
|
||||
by You to the Licensor shall be under the terms and conditions of
|
||||
this License, without any additional terms or conditions.
|
||||
Notwithstanding the above, nothing herein shall supersede or modify
|
||||
the terms of any separate license agreement you may have executed
|
||||
with Licensor regarding such Contributions.
|
||||
|
||||
6. Trademarks. This License does not grant permission to use the trade
|
||||
names, trademarks, service marks, or product names of the Licensor,
|
||||
except as required for reasonable and customary use in describing the
|
||||
origin of the Work and reproducing the content of the NOTICE file.
|
||||
|
||||
7. Disclaimer of Warranty. Unless required by applicable law or
|
||||
agreed to in writing, Licensor provides the Work (and each
|
||||
Contributor provides its Contributions) on an "AS IS" BASIS,
|
||||
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
|
||||
implied, including, without limitation, any warranties or conditions
|
||||
of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
|
||||
PARTICULAR PURPOSE. You are solely responsible for determining the
|
||||
appropriateness of using or redistributing the Work and assume any
|
||||
risks associated with Your exercise of permissions under this License.
|
||||
|
||||
8. Limitation of Liability. In no event and under no legal theory,
|
||||
whether in tort (including negligence), contract, or otherwise,
|
||||
unless required by applicable law (such as deliberate and grossly
|
||||
negligent acts) or agreed to in writing, shall any Contributor be
|
||||
liable to You for damages, including any direct, indirect, special,
|
||||
incidental, or consequential damages of any character arising as a
|
||||
result of this License or out of the use or inability to use the
|
||||
Work (including but not limited to damages for loss of goodwill,
|
||||
work stoppage, computer failure or malfunction, or any and all
|
||||
other commercial damages or losses), even if such Contributor
|
||||
has been advised of the possibility of such damages.
|
||||
|
||||
9. Accepting Warranty or Additional Liability. While redistributing
|
||||
the Work or Derivative Works thereof, You may choose to offer,
|
||||
and charge a fee for, acceptance of support, warranty, indemnity,
|
||||
or other liability obligations and/or rights consistent with this
|
||||
License. However, in accepting such obligations, You may act only
|
||||
on Your own behalf and on Your sole responsibility, not on behalf
|
||||
of any other Contributor, and only if You agree to indemnify,
|
||||
defend, and hold each Contributor harmless for any liability
|
||||
incurred by, or claims asserted against, such Contributor by reason
|
||||
of your accepting any such warranty or additional liability.
|
||||
|
||||
END OF TERMS AND CONDITIONS
|
||||
|
||||
APPENDIX: How to apply the Apache License to your work.
|
||||
|
||||
To apply the Apache License to your work, attach the following
|
||||
boilerplate notice, with the fields enclosed by brackets "[]"
|
||||
replaced with your own identifying information. (Don't include
|
||||
the brackets!) The text should be enclosed in the appropriate
|
||||
comment syntax for the file format. We also recommend that a
|
||||
file or class name and description of purpose be included on the
|
||||
same "printed page" as the copyright notice for easier
|
||||
identification within third-party archives.
|
||||
|
||||
Copyright [yyyy] [name of copyright owner]
|
||||
|
||||
Licensed under the Apache License, Version 2.0 (the "License");
|
||||
you may not use this file except in compliance with the License.
|
||||
You may obtain a copy of the License at
|
||||
|
||||
http://www.apache.org/licenses/LICENSE-2.0
|
||||
|
||||
Unless required by applicable law or agreed to in writing, software
|
||||
distributed under the License is distributed on an "AS IS" BASIS,
|
||||
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
See the License for the specific language governing permissions and
|
||||
limitations under the License.
|
||||
@@ -0,0 +1,41 @@
|
||||
## Foundation
|
||||
|
||||
This product includes software developed at National Security Agency
|
||||
(https://www.nsa.gov)
|
||||
|
||||
Portions of this product were created by the U.S. Government and not
|
||||
subject to U.S. copyright protections under 17 U.S.C.
|
||||
|
||||
The remaining portions are copyright their respective authors and have
|
||||
been contributed under the terms of one or more open source licenses,
|
||||
and made available to you under the terms of those licenses (see
|
||||
[LICENSE](LICENSE)).
|
||||
|
||||
|
||||
## Licensing Intent
|
||||
|
||||
The intent is that this software and documentation ("Project") should
|
||||
be treated as if it is licensed under the license associated with the
|
||||
Project ("License") in the [LICENSE](LICENSE) file. However, because
|
||||
we are part of the United States (U.S.) Federal Government, it is not
|
||||
that simple.
|
||||
|
||||
The portions of this Project written by U.S. Federal Government
|
||||
employees within the scope of their federal employment are ineligible
|
||||
for copyright protection in the U.S.; this is generally understood to
|
||||
mean that these portions of the Project are placed in the public
|
||||
domain.
|
||||
|
||||
In countries where copyright protection is available (which does not
|
||||
include the U.S.), contributions made by U.S. Federal Government
|
||||
employees are released under the [LICENSE](LICENSE). Merged
|
||||
contributions from private contributors are released under the
|
||||
[LICENSE](LICENSE).
|
||||
|
||||
The Foundation software is released under the Apache License, Version
|
||||
2.0 ("Apache 2.0").
|
||||
|
||||
Consistent with the inbound=outbound model, contributions to any
|
||||
module must be made available, by the contributor, under the
|
||||
[LICENSE](LICENSE). Please read the Legal section of the
|
||||
[CONTRIBUTING.md](CONTRIBUTING.md) guide.
|
||||
@@ -0,0 +1,52 @@
|
||||
# Foundation
|
||||
|
||||
[Foundation][main] is a repository for formal specifications of
|
||||
cryptographic algorithms and functional assurance artifacts created
|
||||
and maintained by the [National Security Agency][nsa] Research
|
||||
Directorate.
|
||||
|
||||
If you are a U.S. citizen interested in projects like this, to develop
|
||||
Foundation and other cybersecurity tools for NSA to help protect our
|
||||
nation and its allies, consider applying for a [career with
|
||||
us][career].
|
||||
|
||||
## Workflow Status
|
||||
|
||||
This repository uses GitHub Actions to add assurance to its
|
||||
artifacts. The badges here provide the status of those actions.
|
||||
|
||||
[](https://github.com/NationalSecurityAgency/foundation/actions/workflows/infrastructure-build-images.yml)
|
||||
[](https://github.com/NationalSecurityAgency/foundation/actions/workflows/assurance-main.yml)
|
||||
|
||||
## Develop
|
||||
|
||||
Two [development container
|
||||
configurations](.devcontainer/) are maintained in this
|
||||
repository and provide the tooling (Cryptol, SAW, supported SAT/SMT
|
||||
solvers, and more) necessary to support its development. These
|
||||
configurations are compatible with GitHub's
|
||||
[Codespaces](https://github.com/codespaces), a service that enables
|
||||
developers to "Spin up fully configured dev environments in the
|
||||
cloud", as well as [Visual Studio Code's Dev Container
|
||||
extension](https://code.visualstudio.com/docs/devcontainers/containers). Using
|
||||
these configurations in a supported development environment (such as
|
||||
those listed above) is the preferred way to develop in this
|
||||
repository.
|
||||
|
||||
Start developing immediately:
|
||||
* [Cryptol Codespace](https://codespaces.new/NationalSecurityAgency/foundation?devcontainer_path=.devcontainer%2Fcryptol-dev%2Fdevcontainer.json)
|
||||
* [SAW Codespace](https://codespaces.new/NationalSecurityAgency/foundation?devcontainer_path=.devcontainer%2Fsaw-dev%2Fdevcontainer.json)
|
||||
|
||||
## Contribute
|
||||
|
||||
If you would like to contribute bug fixes, improvements, and new
|
||||
features back to Foundation, please take a look at our [Contributor
|
||||
Guide][contrib] and [Developer Guide][devguide] to see how you can
|
||||
participate in this open source project.
|
||||
|
||||
[nsa]: https://www.nsa.gov
|
||||
[contrib]: CONTRIBUTING.md
|
||||
[devguide]: docs/DevGuide.md
|
||||
[career]: https://www.intelligencecareers.gov/nsa
|
||||
[releases]: https://github.com/NationalSecurityAgency/foundation/releases
|
||||
[main]: https://github.com/NationalSecurityAgency/foundation/archive/refs/heads/master.zip
|
||||
@@ -0,0 +1,10 @@
|
||||
# Bibliography
|
||||
|
||||
[FIPS-PUB-197], Advanced Encryption Standard (AES), FIPS Publication
|
||||
197, National Institute of Standards and Technology (NIST), May 9,
|
||||
2023. https://doi.org/10.6028/NIST.FIPS.197-upd1
|
||||
|
||||
[AES Test Vectors], National Institute of Standards and
|
||||
Technology. Cryptographic Standards and Guidelines: Examples with
|
||||
Intermediate Values, 2022.
|
||||
https://csrc.nist.gov/projects/cryptographic-standards-and-guidelines/example-values.
|
||||
@@ -0,0 +1,215 @@
|
||||
/*
|
||||
* Description: This is a Cryptol specification of the `Cipher` and
|
||||
* `InvCipher` methods in the Advanced Encryption Standard (AES)
|
||||
* [FIPS-PUB-197].
|
||||
*/
|
||||
|
||||
module algorithms::AES::Cipher where
|
||||
|
||||
import algorithms::AES::Types
|
||||
import algorithms::AES::GF28 ((•))
|
||||
import algorithms::AES::SBox (SBox, InvSBox)
|
||||
|
||||
/**
|
||||
* This function performs one round of AES encryption [FIPS-PUB-197
|
||||
* Section 5.1].
|
||||
*/
|
||||
Round : Block -> Block -> Block
|
||||
Round xs ki = AddRoundKey (MixColumns (ShiftRows (SubBytes xs))) ki
|
||||
|
||||
/**
|
||||
* The `Cipher` function performs AES encryption [FIPS-PUB-197
|
||||
* Section 5.1].
|
||||
*/
|
||||
foreign Cipher : {k} (Key k) => [Nr k + 1]Block -> Block -> Block
|
||||
Cipher ([w0] # ws # [wr]) in = state_final
|
||||
where
|
||||
state_initial = AddRoundKey in w0
|
||||
state_rounds = foldl Round state_initial ws
|
||||
state_final = AddRoundKey (ShiftRows (SubBytes state_rounds)) wr
|
||||
|
||||
/**
|
||||
* This function performs one round of AES decryption [FIPS-PUB-197
|
||||
* Section 5.3].
|
||||
*/
|
||||
InvRound : Block -> Block -> Block
|
||||
InvRound xs ki = InvMixColumns (AddRoundKey (InvSubBytes (InvShiftRows xs)) ki)
|
||||
|
||||
/**
|
||||
* This is an alternate version of the `InvRound` function that is a
|
||||
* proper inverse of `Round`.
|
||||
*/
|
||||
InvRound' : Block -> Block -> Block
|
||||
InvRound' xs ki = InvSubBytes (InvShiftRows (InvMixColumns (AddRoundKey xs ki)))
|
||||
|
||||
/**
|
||||
* This property demonstrates that `Round` and `InvRound'` are
|
||||
* inverses.
|
||||
*/
|
||||
RoundInverts : Block -> Block -> Bool
|
||||
property RoundInverts xs ki = InvRound' (Round xs ki) ki == xs
|
||||
|
||||
/**
|
||||
* The `InvCipher` function performs AES decryption [FIPS-PUB-197
|
||||
* Section 5.3].
|
||||
*/
|
||||
foreign InvCipher : {k} (Key k) => [Nr k + 1]Block -> Block -> Block
|
||||
InvCipher ([w0] # ws # [wr]) in = state_final
|
||||
where
|
||||
state_initial = AddRoundKey in wr
|
||||
state_rounds = foldl InvRound state_initial (reverse ws)
|
||||
state_final = AddRoundKey (InvSubBytes (InvShiftRows state_rounds)) w0
|
||||
|
||||
/**
|
||||
* This is an alternate version of the `InvCipher` function
|
||||
* [FIPS-PUB-197 Section 5.3]. The following deviates from Algorithm 3
|
||||
* but is functionally equivalent and more obviously the inverse of
|
||||
* `Cipher`.
|
||||
*/
|
||||
InvCipher' : {k} (Key k) => [Nr k + 1]Block -> Block -> Block
|
||||
InvCipher' ([w0] # ws # [wr]) in = state_final
|
||||
where
|
||||
state_initial = InvSubBytes (InvShiftRows (AddRoundKey in wr))
|
||||
state_rounds = foldl InvRound' state_initial (reverse ws)
|
||||
state_final = AddRoundKey state_rounds w0
|
||||
|
||||
/**
|
||||
* This property demonstrates that `InvCipher` and `InvCipher` are
|
||||
* functionally equivalent.
|
||||
*/
|
||||
InvCipherEquivalence : {k} (Key k) => [Nr k + 1]Block -> Block -> Bool
|
||||
property InvCipherEquivalence ws state =
|
||||
InvCipher`{k} ws state == InvCipher'`{k} ws state
|
||||
|
||||
/**
|
||||
* This property demonstrates that `Cipher` and `InvCipher` are
|
||||
* inverses.
|
||||
*/
|
||||
CipherInverts : {k} (Key k) => [Nr k + 1]Block -> Block -> Bool
|
||||
property CipherInverts ws state =
|
||||
InvCipher`{k} ws (Cipher`{k} ws state) == state
|
||||
|
||||
/**
|
||||
* This property demonstrates that `Cipher` and `InvCipher'` are
|
||||
* inverses.
|
||||
*/
|
||||
CipherInverts' : {k} (Key k) => [Nr k + 1]Block -> Block -> Bool
|
||||
property CipherInverts' ws state =
|
||||
InvCipher'`{k} ws (Cipher`{k} ws state) == state
|
||||
|
||||
/**
|
||||
* This function performs the `SubBytes` transformation [FIPS-PUB-197
|
||||
* Section 5.1.1].
|
||||
*/
|
||||
SubBytes : Block -> Block
|
||||
SubBytes bs = SBox @@ bs
|
||||
|
||||
/**
|
||||
* This function performs the `InvSubBytes` transformation
|
||||
* [FIPS-PUB-197 Section 5.3.2].
|
||||
*/
|
||||
InvSubBytes : Block -> Block
|
||||
InvSubBytes bs = InvSBox @@ bs
|
||||
|
||||
/**
|
||||
* This property demonstrates that `SubBytes` and `InvSubBytes` are
|
||||
* inverses.
|
||||
*/
|
||||
SubBytesInverts : Block -> Bool
|
||||
property SubBytesInverts bs = InvSubBytes (SubBytes bs) == bs
|
||||
|
||||
/**
|
||||
* This function performs the `ShiftRows` transformation [FIPS-PUB-197
|
||||
* Section 5.1.2]. Here, `ShiftRows` is treated as a permutation of a
|
||||
* sequence bytes rather than a series of cyclic shifts on a matrix of
|
||||
* bytes.
|
||||
*/
|
||||
ShiftRows : Block -> Block
|
||||
ShiftRows bs = bs @@ [ 0, 5, 10, 15
|
||||
, 4, 9, 14, 3
|
||||
, 8, 13, 2, 7
|
||||
, 12, 1, 6, 11
|
||||
]
|
||||
|
||||
/**
|
||||
* This function performs the `InvShiftRows` transformation
|
||||
* [FIPS-PUB-197 Section 5.3.1]. Here, `InvShiftRows` is treated as a
|
||||
* permutation of a sequence bytes rather than a series of cyclic
|
||||
* shifts on a matrix of bytes.
|
||||
*/
|
||||
InvShiftRows : Block -> Block
|
||||
InvShiftRows bs = bs @@ [ 0, 13, 10, 7
|
||||
, 4, 1, 14, 11
|
||||
, 8, 5, 2, 15
|
||||
, 12, 9, 6, 3
|
||||
]
|
||||
|
||||
/**
|
||||
* This property demonstrates that `ShiftRows` and `InvShiftRows` are
|
||||
* inverses.
|
||||
*/
|
||||
ShiftRowsInverts : Block -> Bool
|
||||
property ShiftRowsInverts xs = InvShiftRows (ShiftRows xs) == xs
|
||||
|
||||
/**
|
||||
* This is one step of `MixColumns` [FIPS-PUB-197 Section 5.1.3].
|
||||
*/
|
||||
MixColumnsStep : AESWord -> AESWord
|
||||
MixColumnsStep [s0, s1, s2, s3] =
|
||||
[ (0x02 • s0) ^ (0x03 • s1) ^ s2 ^ s3
|
||||
, s0 ^ (0x02 • s1) ^ (0x03 • s2) ^ s3
|
||||
, s0 ^ s1 ^ (0x02 • s2) ^ (0x03 • s3)
|
||||
, (0x03 • s0) ^ s1 ^ s2 ^ (0x02 • s3)
|
||||
]
|
||||
|
||||
/**
|
||||
* This function performs the `MixColumns` transformation
|
||||
* [FIPS-PUB-197 Section 5.1.3].
|
||||
*/
|
||||
MixColumns : Block -> Block
|
||||
MixColumns bs = join (map MixColumnsStep (split bs))
|
||||
|
||||
/**
|
||||
* The is one step of `InvMixColumns` [FIPS-PUB-197 Section 5.3.3].
|
||||
*/
|
||||
InvMixColumnsStep : AESWord -> AESWord
|
||||
InvMixColumnsStep [s0, s1, s2, s3] =
|
||||
[ (0x0e • s0) ^ (0x0b • s1) ^ (0x0d • s2) ^ (0x09 • s3)
|
||||
, (0x09 • s0) ^ (0x0e • s1) ^ (0x0b • s2) ^ (0x0d • s3)
|
||||
, (0x0d • s0) ^ (0x09 • s1) ^ (0x0e • s2) ^ (0x0b • s3)
|
||||
, (0x0b • s0) ^ (0x0d • s1) ^ (0x09 • s2) ^ (0x0e • s3)
|
||||
]
|
||||
|
||||
/**
|
||||
* This function performs the `InvMixColumns` transformation
|
||||
* [FIPS-PUB-197 Section 5.3.3].
|
||||
*/
|
||||
InvMixColumns : Block -> Block
|
||||
InvMixColumns bs = join (map InvMixColumnsStep (split bs))
|
||||
|
||||
/**
|
||||
* This property demonstrates that the step functions of `MixColumns`
|
||||
* and `InvMixColumns` are inverses.
|
||||
*/
|
||||
MixColumnsStepInverts : AESWord -> Bool
|
||||
property MixColumnsStepInverts b = InvMixColumnsStep (MixColumnsStep b) == b
|
||||
|
||||
/**
|
||||
* This property demonstrates that `MixColumns` and `InvMixColumns` are
|
||||
* inverses.
|
||||
*/
|
||||
MixColumnsInverts : Block -> Bool
|
||||
property MixColumnsInverts bs = InvMixColumns (MixColumns bs) == bs
|
||||
|
||||
/**
|
||||
* This function adds a round key into the current state [FIPS-PUB-197
|
||||
* Section 5.1.4].
|
||||
*/
|
||||
AddRoundKey : Block -> Block -> Block
|
||||
AddRoundKey bs w = bs ^ w
|
||||
|
||||
/**
|
||||
* This property demonstrates that `AddRoundKey` is an involution.
|
||||
*/
|
||||
AddRoundKeyInvolution : Block -> Block -> Bool
|
||||
property AddRoundKeyInvolution bs w = AddRoundKey (AddRoundKey bs w) w == bs
|
||||
Symlink
+1
@@ -0,0 +1 @@
|
||||
rust/Cipher/target/release/libCipher.dylib
|
||||
Symlink
+1
@@ -0,0 +1 @@
|
||||
rust/Cipher/target/release/libCipher.so
|
||||
@@ -0,0 +1,32 @@
|
||||
/*
|
||||
* Description: This is a Cryptol specification of the GF(2^^8)
|
||||
* routines in the Advanced Encryption Standard (AES) [FIPS-PUB-197].
|
||||
*/
|
||||
|
||||
module algorithms::AES::GF28 where
|
||||
|
||||
/**
|
||||
* The `•` symbol denotes multiplication in GF(2^^8) [FIPS-PUB-197
|
||||
* Section 4.2].
|
||||
*/
|
||||
(•) : [8] -> [8] -> [8]
|
||||
(•) b c = pmod (pmult b c) m
|
||||
where m = <| x^^8 + x^^4 + x^^3 + x + 1 |>
|
||||
|
||||
/**
|
||||
* This function performs the product of `b • 0x02` and is implemented
|
||||
* here at the byte level as a left shift and a subsequent conditional
|
||||
* bitwise XOR with `0x1b` [FIPS-PUB-197 Section 4.2].
|
||||
*/
|
||||
xTimes : [8] -> [8]
|
||||
xTimes b = b << 1 ^ (if head b then 0x1b else 0x00)
|
||||
|
||||
/**
|
||||
* This property demonstrates that Cryptol's built-in polynomial
|
||||
* arithmetic is functionally equivalent to AES's GF(2^^8)
|
||||
* multiplication routine [FIPS-PUB-197 Section 4.2].
|
||||
*/
|
||||
GF28MultiplicationCorrect : [8] -> [8] -> Bool
|
||||
property GF28MultiplicationCorrect b c =
|
||||
xTimes b == b • 2
|
||||
/\ b • c == foldl (\a bi -> xTimes a ^ if bi then c else 0x00) 0x00 b
|
||||
@@ -0,0 +1,60 @@
|
||||
/*
|
||||
* Description: This is a Cryptol specification of the `KeyExpansion`
|
||||
* method in the Advanced Encryption Standard (AES) [FIPS-PUB-197].
|
||||
*/
|
||||
|
||||
module algorithms::AES::KeyExpansion where
|
||||
|
||||
import algorithms::AES::Types
|
||||
import algorithms::AES::SBox (SBox)
|
||||
|
||||
/**
|
||||
* This table holds the word array for the round constant
|
||||
* [FIPS-PUB-197 Sections 2.1 and 5.2]. Constants are used here rather
|
||||
* than computing the values in place.
|
||||
*/
|
||||
Rcon : [11]AESWord
|
||||
Rcon = [ undefined
|
||||
, [ 0x01, 0x00, 0x00, 0x00 ]
|
||||
, [ 0x02, 0x00, 0x00, 0x00 ]
|
||||
, [ 0x04, 0x00, 0x00, 0x00 ]
|
||||
, [ 0x08, 0x00, 0x00, 0x00 ]
|
||||
, [ 0x10, 0x00, 0x00, 0x00 ]
|
||||
, [ 0x20, 0x00, 0x00, 0x00 ]
|
||||
, [ 0x40, 0x00, 0x00, 0x00 ]
|
||||
, [ 0x80, 0x00, 0x00, 0x00 ]
|
||||
, [ 0x1b, 0x00, 0x00, 0x00 ]
|
||||
, [ 0x36, 0x00, 0x00, 0x00 ]
|
||||
]
|
||||
|
||||
/**
|
||||
* This function takes a word [a0,a1,a2,a3] as input and performs a
|
||||
* cyclic permutation, returning the word [a1,a2,a3,a0] [FIPS-PUB-197
|
||||
* Section 5.2].
|
||||
*/
|
||||
RotWord : AESWord -> AESWord
|
||||
RotWord [ a0, a1, a2, a3 ] = [ a1, a2, a3, a0 ]
|
||||
|
||||
/**
|
||||
* This function takes a four-byte input word and applies the S-box to
|
||||
* each of the four bytes to produce an output word [FIPS-PUB-197
|
||||
* Section 5.2].
|
||||
*/
|
||||
SubWord : AESWord -> AESWord
|
||||
SubWord [ a0, a1, a2, a3 ] =
|
||||
[ SBox @ a0, SBox @ a1, SBox @ a2, SBox @ a3 ]
|
||||
|
||||
/**
|
||||
* This is the main AES key expansion routine [FIPS-PUB-197 Section
|
||||
* 5.2].
|
||||
*/
|
||||
foreign KeyExpansion : {k} (Key k) => [Nk k]AESWord -> [Nr k + 1]Block
|
||||
KeyExpansion key = split (split (join (join w)))
|
||||
where
|
||||
Nk = `(Nk k)
|
||||
w = [ if i < Nk then key@i
|
||||
| i % Nk == 0 then w@(i - Nk) ^ SubWord (RotWord (w@(i - 1))) ^ Rcon@(i / Nk)
|
||||
| i % Nk == 4 /\ Nk > 6 then w@(i - Nk) ^ SubWord (w@(i - 1))
|
||||
else w@(i - Nk) ^ w@(i - 1)
|
||||
| i <- [ 0 ..< 4 * (Nr k + 1) ]
|
||||
] : [4 * (Nr k + 1)]AESWord
|
||||
+1
@@ -0,0 +1 @@
|
||||
rust/KeyExpansion/target/release/libKeyExpansion.dylib
|
||||
Symlink
+1
@@ -0,0 +1 @@
|
||||
rust/KeyExpansion/target/release/libKeyExpansion.so
|
||||
@@ -0,0 +1,48 @@
|
||||
/*
|
||||
* Description: This is a Cryptol specification for the Advanced
|
||||
* Encryption Standard (AES), also called Rijndael
|
||||
* [FIPS-PUB-197]. This specification is specialized to Nb = 4 and
|
||||
* supports the standard key sizes of 128, 192, and 256-bits.
|
||||
*/
|
||||
|
||||
module algorithms::AES::Main where
|
||||
|
||||
import algorithms::AES::Types
|
||||
import algorithms::AES::Cipher (Cipher, InvCipher)
|
||||
import algorithms::AES::KeyExpansion (KeyExpansion)
|
||||
|
||||
/**
|
||||
* This record holds the main AES block cipher functions [FIPS-PUB-197
|
||||
* Section 5], namely, `Encrypt` and `Decrypt`.
|
||||
*/
|
||||
AES : {k} (Key k)
|
||||
=> { Encrypt : ([k] -> [128] -> [128])
|
||||
, Decrypt : ([k] -> [128] -> [128])
|
||||
}
|
||||
AES = {
|
||||
Encrypt key in = join (Cipher`{k} (KeyExpansion`{k} (split (split key))) (split in))
|
||||
, Decrypt key in = join (InvCipher`{k} (KeyExpansion`{k} (split (split key))) (split in))
|
||||
}
|
||||
|
||||
/**
|
||||
* This property demonstrates that `Encrypt` and `Decrypt` are
|
||||
* inverses.
|
||||
*/
|
||||
EncryptInverts : {k} (Key k) => [k] -> [128] -> Bit
|
||||
property EncryptInverts key in =
|
||||
AES`{k}.Decrypt key (AES`{k}.Encrypt key in) == in
|
||||
|
||||
/**
|
||||
* This is the AES-128 block cipher [FIPS-PUB-197 Section 5].
|
||||
*/
|
||||
AES128 = AES`{128}
|
||||
|
||||
/**
|
||||
* This is the AES-192 block cipher [FIPS-PUB-197 Section 5].
|
||||
*/
|
||||
AES192 = AES`{192}
|
||||
|
||||
/**
|
||||
* This is the AES-256 block cipher [FIPS-PUB-197 Section 5].
|
||||
*/
|
||||
AES256 = AES`{256}
|
||||
@@ -0,0 +1,89 @@
|
||||
/*
|
||||
* Description: This is a Cryptol specification of the `S-Box`es for
|
||||
* the Advanced Encryption Standard (AES) [FIPS-PUB-197].
|
||||
*/
|
||||
|
||||
module algorithms::AES::SBox where
|
||||
|
||||
import shared::algebra::Polynomial::GF2 (is_irreducible, inverse, (^*), (^%), (^^^))
|
||||
|
||||
/** The S-box irreducible polynomial [FIPS-PUB-197 Section 4.2]. */
|
||||
SBoxPolynomial = <| x^^8 + x^^4 + x^^3 + x + 1 |> : [9]
|
||||
|
||||
/** This property demonstrates that the S-Box polynomial is irreducible. */
|
||||
SBoxPolynomialIsIrreducible : Bool
|
||||
property SBoxPolynomialIsIrreducible = is_irreducible`{8} SBoxPolynomial
|
||||
|
||||
/**
|
||||
* This property demonstrates that `inverse` is correct [FIPS-PUB-197
|
||||
* Section 4.4].
|
||||
*
|
||||
* ```
|
||||
* :exhaust inverseCorrect
|
||||
* ```
|
||||
*/
|
||||
inverseCorrect : [8] -> Bool
|
||||
property inverseCorrect b =
|
||||
b == 0 ==> inverse b SBoxPolynomial == 0
|
||||
/\ inverse b SBoxPolynomial == b ^^^ (254, SBoxPolynomial)
|
||||
|
||||
/** Affine transformation [FIPS-PUB-197 Section 5.1.1]. */
|
||||
affine : [8] -> [8]
|
||||
affine b = reverse b'
|
||||
where
|
||||
c = reverse 0b01100011
|
||||
b_ = reverse (inverse b SBoxPolynomial)
|
||||
b'@i = b_@i ^ b_@((i+4) % 8) ^ b_@((i+5) % 8) ^ b_@((i+6) % 8) ^ b_@((i+7) % 8) ^ c@i
|
||||
|
||||
/** This property demonstrates that the AES S-Box is correct. */
|
||||
property SBoxCorrect = [ affine b | b <- [0..255] ] == SBox
|
||||
|
||||
/**
|
||||
* This table is the S-box [FIPS-PUB-197 Section 5.1.1 and Table 4].
|
||||
*/
|
||||
SBox : [256][8]
|
||||
SBox = [ 0x63, 0x7c, 0x77, 0x7b, 0xf2, 0x6b, 0x6f, 0xc5, 0x30, 0x01, 0x67, 0x2b, 0xfe, 0xd7, 0xab, 0x76
|
||||
, 0xca, 0x82, 0xc9, 0x7d, 0xfa, 0x59, 0x47, 0xf0, 0xad, 0xd4, 0xa2, 0xaf, 0x9c, 0xa4, 0x72, 0xc0
|
||||
, 0xb7, 0xfd, 0x93, 0x26, 0x36, 0x3f, 0xf7, 0xcc, 0x34, 0xa5, 0xe5, 0xf1, 0x71, 0xd8, 0x31, 0x15
|
||||
, 0x04, 0xc7, 0x23, 0xc3, 0x18, 0x96, 0x05, 0x9a, 0x07, 0x12, 0x80, 0xe2, 0xeb, 0x27, 0xb2, 0x75
|
||||
, 0x09, 0x83, 0x2c, 0x1a, 0x1b, 0x6e, 0x5a, 0xa0, 0x52, 0x3b, 0xd6, 0xb3, 0x29, 0xe3, 0x2f, 0x84
|
||||
, 0x53, 0xd1, 0x00, 0xed, 0x20, 0xfc, 0xb1, 0x5b, 0x6a, 0xcb, 0xbe, 0x39, 0x4a, 0x4c, 0x58, 0xcf
|
||||
, 0xd0, 0xef, 0xaa, 0xfb, 0x43, 0x4d, 0x33, 0x85, 0x45, 0xf9, 0x02, 0x7f, 0x50, 0x3c, 0x9f, 0xa8
|
||||
, 0x51, 0xa3, 0x40, 0x8f, 0x92, 0x9d, 0x38, 0xf5, 0xbc, 0xb6, 0xda, 0x21, 0x10, 0xff, 0xf3, 0xd2
|
||||
, 0xcd, 0x0c, 0x13, 0xec, 0x5f, 0x97, 0x44, 0x17, 0xc4, 0xa7, 0x7e, 0x3d, 0x64, 0x5d, 0x19, 0x73
|
||||
, 0x60, 0x81, 0x4f, 0xdc, 0x22, 0x2a, 0x90, 0x88, 0x46, 0xee, 0xb8, 0x14, 0xde, 0x5e, 0x0b, 0xdb
|
||||
, 0xe0, 0x32, 0x3a, 0x0a, 0x49, 0x06, 0x24, 0x5c, 0xc2, 0xd3, 0xac, 0x62, 0x91, 0x95, 0xe4, 0x79
|
||||
, 0xe7, 0xc8, 0x37, 0x6d, 0x8d, 0xd5, 0x4e, 0xa9, 0x6c, 0x56, 0xf4, 0xea, 0x65, 0x7a, 0xae, 0x08
|
||||
, 0xba, 0x78, 0x25, 0x2e, 0x1c, 0xa6, 0xb4, 0xc6, 0xe8, 0xdd, 0x74, 0x1f, 0x4b, 0xbd, 0x8b, 0x8a
|
||||
, 0x70, 0x3e, 0xb5, 0x66, 0x48, 0x03, 0xf6, 0x0e, 0x61, 0x35, 0x57, 0xb9, 0x86, 0xc1, 0x1d, 0x9e
|
||||
, 0xe1, 0xf8, 0x98, 0x11, 0x69, 0xd9, 0x8e, 0x94, 0x9b, 0x1e, 0x87, 0xe9, 0xce, 0x55, 0x28, 0xdf
|
||||
, 0x8c, 0xa1, 0x89, 0x0d, 0xbf, 0xe6, 0x42, 0x68, 0x41, 0x99, 0x2d, 0x0f, 0xb0, 0x54, 0xbb, 0x16
|
||||
]
|
||||
|
||||
/**
|
||||
* This table is the inverse S-box [FIPS-PUB-197 Section 5.3.2 and Table 6].
|
||||
*/
|
||||
InvSBox : [256][8]
|
||||
InvSBox = [ 0x52, 0x09, 0x6a, 0xd5, 0x30, 0x36, 0xa5, 0x38, 0xbf, 0x40, 0xa3, 0x9e, 0x81, 0xf3, 0xd7, 0xfb
|
||||
, 0x7c, 0xe3, 0x39, 0x82, 0x9b, 0x2f, 0xff, 0x87, 0x34, 0x8e, 0x43, 0x44, 0xc4, 0xde, 0xe9, 0xcb
|
||||
, 0x54, 0x7b, 0x94, 0x32, 0xa6, 0xc2, 0x23, 0x3d, 0xee, 0x4c, 0x95, 0x0b, 0x42, 0xfa, 0xc3, 0x4e
|
||||
, 0x08, 0x2e, 0xa1, 0x66, 0x28, 0xd9, 0x24, 0xb2, 0x76, 0x5b, 0xa2, 0x49, 0x6d, 0x8b, 0xd1, 0x25
|
||||
, 0x72, 0xf8, 0xf6, 0x64, 0x86, 0x68, 0x98, 0x16, 0xd4, 0xa4, 0x5c, 0xcc, 0x5d, 0x65, 0xb6, 0x92
|
||||
, 0x6c, 0x70, 0x48, 0x50, 0xfd, 0xed, 0xb9, 0xda, 0x5e, 0x15, 0x46, 0x57, 0xa7, 0x8d, 0x9d, 0x84
|
||||
, 0x90, 0xd8, 0xab, 0x00, 0x8c, 0xbc, 0xd3, 0x0a, 0xf7, 0xe4, 0x58, 0x05, 0xb8, 0xb3, 0x45, 0x06
|
||||
, 0xd0, 0x2c, 0x1e, 0x8f, 0xca, 0x3f, 0x0f, 0x02, 0xc1, 0xaf, 0xbd, 0x03, 0x01, 0x13, 0x8a, 0x6b
|
||||
, 0x3a, 0x91, 0x11, 0x41, 0x4f, 0x67, 0xdc, 0xea, 0x97, 0xf2, 0xcf, 0xce, 0xf0, 0xb4, 0xe6, 0x73
|
||||
, 0x96, 0xac, 0x74, 0x22, 0xe7, 0xad, 0x35, 0x85, 0xe2, 0xf9, 0x37, 0xe8, 0x1c, 0x75, 0xdf, 0x6e
|
||||
, 0x47, 0xf1, 0x1a, 0x71, 0x1d, 0x29, 0xc5, 0x89, 0x6f, 0xb7, 0x62, 0x0e, 0xaa, 0x18, 0xbe, 0x1b
|
||||
, 0xfc, 0x56, 0x3e, 0x4b, 0xc6, 0xd2, 0x79, 0x20, 0x9a, 0xdb, 0xc0, 0xfe, 0x78, 0xcd, 0x5a, 0xf4
|
||||
, 0x1f, 0xdd, 0xa8, 0x33, 0x88, 0x07, 0xc7, 0x31, 0xb1, 0x12, 0x10, 0x59, 0x27, 0x80, 0xec, 0x5f
|
||||
, 0x60, 0x51, 0x7f, 0xa9, 0x19, 0xb5, 0x4a, 0x0d, 0x2d, 0xe5, 0x7a, 0x9f, 0x93, 0xc9, 0x9c, 0xef
|
||||
, 0xa0, 0xe0, 0x3b, 0x4d, 0xae, 0x2a, 0xf5, 0xb0, 0xc8, 0xeb, 0xbb, 0x3c, 0x83, 0x53, 0x99, 0x61
|
||||
, 0x17, 0x2b, 0x04, 0x7e, 0xba, 0x77, 0xd6, 0x26, 0xe1, 0x69, 0x14, 0x63, 0x55, 0x21, 0x0c, 0x7d
|
||||
]
|
||||
|
||||
/**
|
||||
* This property demonstrates that `SBox` and `InvSBox` are inverses.
|
||||
*/
|
||||
SBoxInverts : [8] -> Bool
|
||||
property SBoxInverts b = InvSBox @ (SBox @ b) == b
|
||||
@@ -0,0 +1,299 @@
|
||||
/*
|
||||
* Description: This module holds tests for public functions in the
|
||||
* Cryptol specification for the Advanced Encryption Standard (AES)
|
||||
* [FIPS-PUB-197].
|
||||
*/
|
||||
|
||||
module algorithms::AES::Tests where
|
||||
|
||||
import algorithms::AES::KeyExpansion
|
||||
import algorithms::AES::Cipher
|
||||
import algorithms::AES::Main
|
||||
|
||||
/**
|
||||
* This test demonstrates the expansion of a 128-bit key [FIPS-PUB-197
|
||||
* Appendix A.1].
|
||||
*/
|
||||
property Example128KeyExpansion =
|
||||
KeyExpansion`{128} (split (split 0x2b7e151628aed2a6abf7158809cf4f3c))
|
||||
== [ [ 0x2b, 0x7e, 0x15, 0x16
|
||||
, 0x28, 0xae, 0xd2, 0xa6
|
||||
, 0xab, 0xf7, 0x15, 0x88
|
||||
, 0x09, 0xcf, 0x4f, 0x3c
|
||||
]
|
||||
, [ 0xa0, 0xfa, 0xfe, 0x17
|
||||
, 0x88, 0x54, 0x2c, 0xb1
|
||||
, 0x23, 0xa3, 0x39, 0x39
|
||||
, 0x2a, 0x6c, 0x76, 0x05
|
||||
]
|
||||
, [ 0xf2, 0xc2, 0x95, 0xf2
|
||||
, 0x7a, 0x96, 0xb9, 0x43
|
||||
, 0x59, 0x35, 0x80, 0x7a
|
||||
, 0x73, 0x59, 0xf6, 0x7f
|
||||
]
|
||||
, [ 0x3d, 0x80, 0x47, 0x7d
|
||||
, 0x47, 0x16, 0xfe, 0x3e
|
||||
, 0x1e, 0x23, 0x7e, 0x44
|
||||
, 0x6d, 0x7a, 0x88, 0x3b
|
||||
]
|
||||
, [ 0xef, 0x44, 0xa5, 0x41
|
||||
, 0xa8, 0x52, 0x5b, 0x7f
|
||||
, 0xb6, 0x71, 0x25, 0x3b
|
||||
, 0xdb, 0x0b, 0xad, 0x00
|
||||
]
|
||||
, [ 0xd4, 0xd1, 0xc6, 0xf8
|
||||
, 0x7c, 0x83, 0x9d, 0x87
|
||||
, 0xca, 0xf2, 0xb8, 0xbc
|
||||
, 0x11, 0xf9, 0x15, 0xbc
|
||||
]
|
||||
, [ 0x6d, 0x88, 0xa3, 0x7a
|
||||
, 0x11, 0x0b, 0x3e, 0xfd
|
||||
, 0xdb, 0xf9, 0x86, 0x41
|
||||
, 0xca, 0x00, 0x93, 0xfd
|
||||
]
|
||||
, [ 0x4e, 0x54, 0xf7, 0x0e
|
||||
, 0x5f, 0x5f, 0xc9, 0xf3
|
||||
, 0x84, 0xa6, 0x4f, 0xb2
|
||||
, 0x4e, 0xa6, 0xdc, 0x4f
|
||||
]
|
||||
, [ 0xea, 0xd2, 0x73, 0x21
|
||||
, 0xb5, 0x8d, 0xba, 0xd2
|
||||
, 0x31, 0x2b, 0xf5, 0x60
|
||||
, 0x7f, 0x8d, 0x29, 0x2f
|
||||
]
|
||||
, [ 0xac, 0x77, 0x66, 0xf3
|
||||
, 0x19, 0xfa, 0xdc, 0x21
|
||||
, 0x28, 0xd1, 0x29, 0x41
|
||||
, 0x57, 0x5c, 0x00, 0x6e
|
||||
]
|
||||
, [ 0xd0, 0x14, 0xf9, 0xa8
|
||||
, 0xc9, 0xee, 0x25, 0x89
|
||||
, 0xe1, 0x3f, 0x0c, 0xc8
|
||||
, 0xb6, 0x63, 0x0c, 0xa6
|
||||
]
|
||||
]
|
||||
|
||||
/**
|
||||
* This test demonstrates the expansion of a 192-bit key [FIPS-PUB-197
|
||||
* Appendix A.2].
|
||||
*/
|
||||
property Example192KeyExpansion =
|
||||
KeyExpansion`{192} (split (split 0x8e73b0f7da0e6452c810f32b809079e562f8ead2522c6b7b))
|
||||
== [ [ 0x8e, 0x73, 0xb0, 0xf7
|
||||
, 0xda, 0x0e, 0x64, 0x52
|
||||
, 0xc8, 0x10, 0xf3, 0x2b
|
||||
, 0x80, 0x90, 0x79, 0xe5
|
||||
]
|
||||
, [ 0x62, 0xf8, 0xea, 0xd2
|
||||
, 0x52, 0x2c, 0x6b, 0x7b
|
||||
, 0xfe, 0x0c, 0x91, 0xf7
|
||||
, 0x24, 0x02, 0xf5, 0xa5
|
||||
]
|
||||
, [ 0xec, 0x12, 0x06, 0x8e
|
||||
, 0x6c, 0x82, 0x7f, 0x6b
|
||||
, 0x0e, 0x7a, 0x95, 0xb9
|
||||
, 0x5c, 0x56, 0xfe, 0xc2
|
||||
]
|
||||
, [ 0x4d, 0xb7, 0xb4, 0xbd
|
||||
, 0x69, 0xb5, 0x41, 0x18
|
||||
, 0x85, 0xa7, 0x47, 0x96
|
||||
, 0xe9, 0x25, 0x38, 0xfd
|
||||
]
|
||||
, [ 0xe7, 0x5f, 0xad, 0x44
|
||||
, 0xbb, 0x09, 0x53, 0x86
|
||||
, 0x48, 0x5a, 0xf0, 0x57
|
||||
, 0x21, 0xef, 0xb1, 0x4f
|
||||
]
|
||||
, [ 0xa4, 0x48, 0xf6, 0xd9
|
||||
, 0x4d, 0x6d, 0xce, 0x24
|
||||
, 0xaa, 0x32, 0x63, 0x60
|
||||
, 0x11, 0x3b, 0x30, 0xe6
|
||||
]
|
||||
, [ 0xa2, 0x5e, 0x7e, 0xd5
|
||||
, 0x83, 0xb1, 0xcf, 0x9a
|
||||
, 0x27, 0xf9, 0x39, 0x43
|
||||
, 0x6a, 0x94, 0xf7, 0x67
|
||||
]
|
||||
, [ 0xc0, 0xa6, 0x94, 0x07
|
||||
, 0xd1, 0x9d, 0xa4, 0xe1
|
||||
, 0xec, 0x17, 0x86, 0xeb
|
||||
, 0x6f, 0xa6, 0x49, 0x71
|
||||
]
|
||||
, [ 0x48, 0x5f, 0x70, 0x32
|
||||
, 0x22, 0xcb, 0x87, 0x55
|
||||
, 0xe2, 0x6d, 0x13, 0x52
|
||||
, 0x33, 0xf0, 0xb7, 0xb3
|
||||
]
|
||||
, [ 0x40, 0xbe, 0xeb, 0x28
|
||||
, 0x2f, 0x18, 0xa2, 0x59
|
||||
, 0x67, 0x47, 0xd2, 0x6b
|
||||
, 0x45, 0x8c, 0x55, 0x3e
|
||||
]
|
||||
, [ 0xa7, 0xe1, 0x46, 0x6c
|
||||
, 0x94, 0x11, 0xf1, 0xdf
|
||||
, 0x82, 0x1f, 0x75, 0x0a
|
||||
, 0xad, 0x07, 0xd7, 0x53
|
||||
]
|
||||
, [ 0xca, 0x40, 0x05, 0x38
|
||||
, 0x8f, 0xcc, 0x50, 0x06
|
||||
, 0x28, 0x2d, 0x16, 0x6a
|
||||
, 0xbc, 0x3c, 0xe7, 0xb5
|
||||
]
|
||||
, [ 0xe9, 0x8b, 0xa0, 0x6f
|
||||
, 0x44, 0x8c, 0x77, 0x3c
|
||||
, 0x8e, 0xcc, 0x72, 0x04
|
||||
, 0x01, 0x00, 0x22, 0x02
|
||||
]
|
||||
]
|
||||
|
||||
/**
|
||||
* This test demonstrates the expansion of a 256-bit key [FIPS-PUB-197
|
||||
* Appendix A.3].
|
||||
*/
|
||||
property Example256KeyExpansion =
|
||||
KeyExpansion`{256} (split (split 0x603deb1015ca71be2b73aef0857d77811f352c073b6108d72d9810a30914dff4))
|
||||
== [ [ 0x60, 0x3d, 0xeb, 0x10
|
||||
, 0x15, 0xca, 0x71, 0xbe
|
||||
, 0x2b, 0x73, 0xae, 0xf0
|
||||
, 0x85, 0x7d, 0x77, 0x81
|
||||
]
|
||||
, [ 0x1f, 0x35, 0x2c, 0x07
|
||||
, 0x3b, 0x61, 0x08, 0xd7
|
||||
, 0x2d, 0x98, 0x10, 0xa3
|
||||
, 0x09, 0x14, 0xdf, 0xf4
|
||||
]
|
||||
, [ 0x9b, 0xa3, 0x54, 0x11
|
||||
, 0x8e, 0x69, 0x25, 0xaf
|
||||
, 0xa5, 0x1a, 0x8b, 0x5f
|
||||
, 0x20, 0x67, 0xfc, 0xde
|
||||
]
|
||||
, [ 0xa8, 0xb0, 0x9c, 0x1a
|
||||
, 0x93, 0xd1, 0x94, 0xcd
|
||||
, 0xbe, 0x49, 0x84, 0x6e
|
||||
, 0xb7, 0x5d, 0x5b, 0x9a
|
||||
]
|
||||
, [ 0xd5, 0x9a, 0xec, 0xb8
|
||||
, 0x5b, 0xf3, 0xc9, 0x17
|
||||
, 0xfe, 0xe9, 0x42, 0x48
|
||||
, 0xde, 0x8e, 0xbe, 0x96
|
||||
]
|
||||
, [ 0xb5, 0xa9, 0x32, 0x8a
|
||||
, 0x26, 0x78, 0xa6, 0x47
|
||||
, 0x98, 0x31, 0x22, 0x29
|
||||
, 0x2f, 0x6c, 0x79, 0xb3
|
||||
]
|
||||
, [ 0x81, 0x2c, 0x81, 0xad
|
||||
, 0xda, 0xdf, 0x48, 0xba
|
||||
, 0x24, 0x36, 0x0a, 0xf2
|
||||
, 0xfa, 0xb8, 0xb4, 0x64
|
||||
]
|
||||
, [ 0x98, 0xc5, 0xbf, 0xc9
|
||||
, 0xbe, 0xbd, 0x19, 0x8e
|
||||
, 0x26, 0x8c, 0x3b, 0xa7
|
||||
, 0x09, 0xe0, 0x42, 0x14
|
||||
]
|
||||
, [ 0x68, 0x00, 0x7b, 0xac
|
||||
, 0xb2, 0xdf, 0x33, 0x16
|
||||
, 0x96, 0xe9, 0x39, 0xe4
|
||||
, 0x6c, 0x51, 0x8d, 0x80
|
||||
]
|
||||
, [ 0xc8, 0x14, 0xe2, 0x04
|
||||
, 0x76, 0xa9, 0xfb, 0x8a
|
||||
, 0x50, 0x25, 0xc0, 0x2d
|
||||
, 0x59, 0xc5, 0x82, 0x39
|
||||
]
|
||||
, [ 0xde, 0x13, 0x69, 0x67
|
||||
, 0x6c, 0xcc, 0x5a, 0x71
|
||||
, 0xfa, 0x25, 0x63, 0x95
|
||||
, 0x96, 0x74, 0xee, 0x15
|
||||
]
|
||||
, [ 0x58, 0x86, 0xca, 0x5d
|
||||
, 0x2e, 0x2f, 0x31, 0xd7
|
||||
, 0x7e, 0x0a, 0xf1, 0xfa
|
||||
, 0x27, 0xcf, 0x73, 0xc3
|
||||
]
|
||||
, [ 0x74, 0x9c, 0x47, 0xab
|
||||
, 0x18, 0x50, 0x1d, 0xda
|
||||
, 0xe2, 0x75, 0x7e, 0x4f
|
||||
, 0x74, 0x01, 0x90, 0x5a
|
||||
]
|
||||
, [ 0xca, 0xfa, 0xaa, 0xe3
|
||||
, 0xe4, 0xd5, 0x9b, 0x34
|
||||
, 0x9a, 0xdf, 0x6a, 0xce
|
||||
, 0xbd, 0x10, 0x19, 0x0d
|
||||
]
|
||||
, [ 0xfe, 0x48, 0x90, 0xd1
|
||||
, 0xe6, 0x18, 0x8d, 0x0b
|
||||
, 0x04, 0x6d, 0xf3, 0x44
|
||||
, 0x70, 0x6c, 0x63, 0x1e
|
||||
]
|
||||
]
|
||||
|
||||
/**
|
||||
* This tests the `Cipher` and `InvCipher` functions [FIPS-PUB-197
|
||||
* Appendix B].
|
||||
*/
|
||||
property CipherExample =
|
||||
Cipher`{128} key input == output
|
||||
/\ InvCipher`{128} key output == input
|
||||
where
|
||||
input = split 0x3243f6a8885a308d313198a2e0370734
|
||||
key = KeyExpansion`{128} (split (split 0x2b7e151628aed2a6abf7158809cf4f3c))
|
||||
output = split 0x3925841d02dc09fbdc118597196a0b32
|
||||
|
||||
/**
|
||||
* An AES-128 example [AES Test Vectors].
|
||||
*/
|
||||
property AES128Example =
|
||||
map (AES`{128}.Encrypt key) plain == cipher
|
||||
/\ map (AES`{128}.Decrypt key) cipher == plain
|
||||
where
|
||||
key = 0x2b7e151628aed2a6abf7158809cf4f3c
|
||||
plain = [ 0x6bc1bee22e409f96e93d7e117393172a
|
||||
, 0xae2d8a571e03ac9c9eb76fac45af8e51
|
||||
, 0x30c81c46a35ce411e5fbc1191a0a52ef
|
||||
, 0xf69f2445df4f9b17ad2b417be66c3710
|
||||
]
|
||||
cipher = [ 0x3ad77bb40d7a3660a89ecaf32466ef97
|
||||
, 0xf5d3d58503b9699de785895a96fdbaaf
|
||||
, 0x43b1cd7f598ece23881b00e3ed030688
|
||||
, 0x7b0c785e27e8ad3f8223207104725dd4
|
||||
]
|
||||
|
||||
/**
|
||||
* An AES-192 example [AES Test Vectors].
|
||||
*/
|
||||
property AES192Example =
|
||||
map (AES`{192}.Encrypt key) plain == cipher
|
||||
/\ map (AES`{192}.Decrypt key) cipher == plain
|
||||
where
|
||||
key = 0x8e73b0f7da0e6452c810f32b809079e562f8ead2522c6b7b
|
||||
plain = [ 0x6bc1bee22e409f96e93d7e117393172a
|
||||
, 0xae2d8a571e03ac9c9eb76fac45af8e51
|
||||
, 0x30c81c46a35ce411e5fbc1191a0a52ef
|
||||
, 0xf69f2445df4f9b17ad2b417be66c3710
|
||||
]
|
||||
cipher = [ 0xbd334f1d6e45f25ff712a214571fa5cc
|
||||
, 0x974104846d0ad3ad7734ecb3ecee4eef
|
||||
, 0xef7afd2270e2e60adce0ba2face6444e
|
||||
, 0x9a4b41ba738d6c72fb16691603c18e0e
|
||||
]
|
||||
|
||||
/**
|
||||
* An AES-256 example [AES Test Vectors].
|
||||
*/
|
||||
property AES256Example =
|
||||
map (AES`{256}.Encrypt key) plain == cipher
|
||||
/\ map (AES`{256}.Decrypt key) cipher == plain
|
||||
where
|
||||
key = 0x603deb1015ca71be2b73aef0857d77811f352c073b6108d72d9810a30914dff4
|
||||
plain = [ 0x6bc1bee22e409f96e93d7e117393172a
|
||||
, 0xae2d8a571e03ac9c9eb76fac45af8e51
|
||||
, 0x30c81c46a35ce411e5fbc1191a0a52ef
|
||||
, 0xf69f2445df4f9b17ad2b417be66c3710
|
||||
]
|
||||
cipher = [ 0xf3eed1bdb5d2a03c064b5a7e3db181f8
|
||||
, 0x591ccb10d410ed26dc5ba74a31362870
|
||||
, 0xb6ed21b99ca6f4f9f153e7b1beafed1d
|
||||
, 0x23304b7a39f9f3ff067d8d8f9e24ecc7
|
||||
]
|
||||
@@ -0,0 +1,39 @@
|
||||
/*
|
||||
* Description: This is a Cryptol specification of the types needed to
|
||||
* specify the Advanced Encryption Standard (AES) [FIPS-PUB-197].
|
||||
*/
|
||||
|
||||
module algorithms::AES::Types where
|
||||
|
||||
/**
|
||||
* This constraint enforces the standard key sizes of 128, 192, and
|
||||
* 256-bits [FIPS-PUB-197 Sections 1, 5, and 6.1].
|
||||
*/
|
||||
type constraint Key k = (fin k, k % 64 == 0, k / 64 >= 2, k / 64 <= 4)
|
||||
|
||||
/**
|
||||
* This sequence of bytes comprises the input, output, State, and
|
||||
* Round Key [FIPS-PUB-197 Section 2.1].
|
||||
*/
|
||||
type Block = [16][8]
|
||||
|
||||
/**
|
||||
* This sequence of bytes represents a 32-bit word [FIPS-PUB-197
|
||||
* Section 2.1]. `AESWord` is used to avoid conflicting with Cryptol's
|
||||
* built-in `Word`.
|
||||
*/
|
||||
type AESWord = [4][8]
|
||||
|
||||
/**
|
||||
* This type represents the number of 32-bit words comprising the
|
||||
* key. `Nk` is assigned to 4, 6, and 8 for `AES128`, `AES192`, and
|
||||
* `AES256`, respectively [FIPS-PUB-197 Sections 2.3 and 5].
|
||||
*/
|
||||
type Nk k = k / 32
|
||||
|
||||
/**
|
||||
* This type represents the number of rounds to perform. `Nr` is
|
||||
* assigned to 10, 12, and 14 for `AES128`, `AES192`, and `AES256`,
|
||||
* respectively [FIPS-PUB-197 Sections 2.3 and 5].
|
||||
*/
|
||||
type Nr k = Nk k + 6
|
||||
Generated
+14
@@ -0,0 +1,14 @@
|
||||
# This file is automatically @generated by Cargo.
|
||||
# It is not intended for manual editing.
|
||||
version = 3
|
||||
|
||||
[[package]]
|
||||
name = "Cipher"
|
||||
version = "0.1.0"
|
||||
dependencies = [
|
||||
"ffi_utils",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "ffi_utils"
|
||||
version = "0.1.0"
|
||||
@@ -0,0 +1,12 @@
|
||||
[package]
|
||||
name = "Cipher"
|
||||
version = "0.1.0"
|
||||
edition = "2021"
|
||||
|
||||
[lib]
|
||||
name = "Cipher"
|
||||
path = "src/lib.rs"
|
||||
crate-type = ["lib", "cdylib"]
|
||||
|
||||
[dependencies]
|
||||
ffi_utils = { path = "../../../../shared/rust/ffi_utils" }
|
||||
@@ -0,0 +1,252 @@
|
||||
//! This is a Rust implementation of the `Cipher` and `InvCipher`
|
||||
//! methods in the Advanced Encryption Standard (AES) [FIPS-PUB-197].
|
||||
|
||||
#![allow(non_snake_case)]
|
||||
|
||||
use ffi_utils::{get_array, get_vec, output_array};
|
||||
|
||||
/// This sequence of bytes comprises the input, output, State, and
|
||||
/// Round Key [FIPS-PUB-197 Section 2.1].
|
||||
pub type Block = [u8; 16];
|
||||
|
||||
/// This sequence of bytes represents a 32-bit word [FIPS-PUB-197
|
||||
/// Section 2.1].
|
||||
pub type Word = [u8; 4];
|
||||
|
||||
/// This function performs the product of `b • 0x02` and is implemented
|
||||
/// here at the byte level as a left shift and a subsequent conditional
|
||||
/// bitwise XOR with `0x1b` [FIPS-PUB-197 Section 4.2].
|
||||
fn xTimes(x: u8) -> u8 {
|
||||
(x << 1) ^ (if x > 127 { 0x1b } else { 0x00 })
|
||||
}
|
||||
|
||||
/// Multiplication of two bytes representing coefficients of
|
||||
/// polynomials in GF 2^^8 [FIPS-PUB-197 Section 4.3].
|
||||
fn mul_bytes(x: u8, y: u8) -> u8 {
|
||||
let mut a: u8 = 0x00;
|
||||
for i in 0..=7 {
|
||||
a = xTimes(a)
|
||||
^ (if (x >> (7 - i)) & 0x01 == 0x01 {
|
||||
y
|
||||
} else {
|
||||
0x00
|
||||
});
|
||||
}
|
||||
a
|
||||
}
|
||||
|
||||
/// S-box [FIPS-PUB-197 Section 5.1.1, Table 4].
|
||||
pub static SBOX: [u8; 256] = [
|
||||
0x63, 0x7c, 0x77, 0x7b, 0xf2, 0x6b, 0x6f, 0xc5, 0x30, 0x01, 0x67, 0x2b, 0xfe, 0xd7, 0xab, 0x76,
|
||||
0xca, 0x82, 0xc9, 0x7d, 0xfa, 0x59, 0x47, 0xf0, 0xad, 0xd4, 0xa2, 0xaf, 0x9c, 0xa4, 0x72, 0xc0,
|
||||
0xb7, 0xfd, 0x93, 0x26, 0x36, 0x3f, 0xf7, 0xcc, 0x34, 0xa5, 0xe5, 0xf1, 0x71, 0xd8, 0x31, 0x15,
|
||||
0x04, 0xc7, 0x23, 0xc3, 0x18, 0x96, 0x05, 0x9a, 0x07, 0x12, 0x80, 0xe2, 0xeb, 0x27, 0xb2, 0x75,
|
||||
0x09, 0x83, 0x2c, 0x1a, 0x1b, 0x6e, 0x5a, 0xa0, 0x52, 0x3b, 0xd6, 0xb3, 0x29, 0xe3, 0x2f, 0x84,
|
||||
0x53, 0xd1, 0x00, 0xed, 0x20, 0xfc, 0xb1, 0x5b, 0x6a, 0xcb, 0xbe, 0x39, 0x4a, 0x4c, 0x58, 0xcf,
|
||||
0xd0, 0xef, 0xaa, 0xfb, 0x43, 0x4d, 0x33, 0x85, 0x45, 0xf9, 0x02, 0x7f, 0x50, 0x3c, 0x9f, 0xa8,
|
||||
0x51, 0xa3, 0x40, 0x8f, 0x92, 0x9d, 0x38, 0xf5, 0xbc, 0xb6, 0xda, 0x21, 0x10, 0xff, 0xf3, 0xd2,
|
||||
0xcd, 0x0c, 0x13, 0xec, 0x5f, 0x97, 0x44, 0x17, 0xc4, 0xa7, 0x7e, 0x3d, 0x64, 0x5d, 0x19, 0x73,
|
||||
0x60, 0x81, 0x4f, 0xdc, 0x22, 0x2a, 0x90, 0x88, 0x46, 0xee, 0xb8, 0x14, 0xde, 0x5e, 0x0b, 0xdb,
|
||||
0xe0, 0x32, 0x3a, 0x0a, 0x49, 0x06, 0x24, 0x5c, 0xc2, 0xd3, 0xac, 0x62, 0x91, 0x95, 0xe4, 0x79,
|
||||
0xe7, 0xc8, 0x37, 0x6d, 0x8d, 0xd5, 0x4e, 0xa9, 0x6c, 0x56, 0xf4, 0xea, 0x65, 0x7a, 0xae, 0x08,
|
||||
0xba, 0x78, 0x25, 0x2e, 0x1c, 0xa6, 0xb4, 0xc6, 0xe8, 0xdd, 0x74, 0x1f, 0x4b, 0xbd, 0x8b, 0x8a,
|
||||
0x70, 0x3e, 0xb5, 0x66, 0x48, 0x03, 0xf6, 0x0e, 0x61, 0x35, 0x57, 0xb9, 0x86, 0xc1, 0x1d, 0x9e,
|
||||
0xe1, 0xf8, 0x98, 0x11, 0x69, 0xd9, 0x8e, 0x94, 0x9b, 0x1e, 0x87, 0xe9, 0xce, 0x55, 0x28, 0xdf,
|
||||
0x8c, 0xa1, 0x89, 0x0d, 0xbf, 0xe6, 0x42, 0x68, 0x41, 0x99, 0x2d, 0x0f, 0xb0, 0x54, 0xbb, 0x16,
|
||||
];
|
||||
|
||||
/// Inverse S-box [FIPS-PUB-197 Section 5.3.2, Table 6].
|
||||
static INVSBOX: [u8; 256] = [
|
||||
0x52, 0x09, 0x6a, 0xd5, 0x30, 0x36, 0xa5, 0x38, 0xbf, 0x40, 0xa3, 0x9e, 0x81, 0xf3, 0xd7, 0xfb,
|
||||
0x7c, 0xe3, 0x39, 0x82, 0x9b, 0x2f, 0xff, 0x87, 0x34, 0x8e, 0x43, 0x44, 0xc4, 0xde, 0xe9, 0xcb,
|
||||
0x54, 0x7b, 0x94, 0x32, 0xa6, 0xc2, 0x23, 0x3d, 0xee, 0x4c, 0x95, 0x0b, 0x42, 0xfa, 0xc3, 0x4e,
|
||||
0x08, 0x2e, 0xa1, 0x66, 0x28, 0xd9, 0x24, 0xb2, 0x76, 0x5b, 0xa2, 0x49, 0x6d, 0x8b, 0xd1, 0x25,
|
||||
0x72, 0xf8, 0xf6, 0x64, 0x86, 0x68, 0x98, 0x16, 0xd4, 0xa4, 0x5c, 0xcc, 0x5d, 0x65, 0xb6, 0x92,
|
||||
0x6c, 0x70, 0x48, 0x50, 0xfd, 0xed, 0xb9, 0xda, 0x5e, 0x15, 0x46, 0x57, 0xa7, 0x8d, 0x9d, 0x84,
|
||||
0x90, 0xd8, 0xab, 0x00, 0x8c, 0xbc, 0xd3, 0x0a, 0xf7, 0xe4, 0x58, 0x05, 0xb8, 0xb3, 0x45, 0x06,
|
||||
0xd0, 0x2c, 0x1e, 0x8f, 0xca, 0x3f, 0x0f, 0x02, 0xc1, 0xaf, 0xbd, 0x03, 0x01, 0x13, 0x8a, 0x6b,
|
||||
0x3a, 0x91, 0x11, 0x41, 0x4f, 0x67, 0xdc, 0xea, 0x97, 0xf2, 0xcf, 0xce, 0xf0, 0xb4, 0xe6, 0x73,
|
||||
0x96, 0xac, 0x74, 0x22, 0xe7, 0xad, 0x35, 0x85, 0xe2, 0xf9, 0x37, 0xe8, 0x1c, 0x75, 0xdf, 0x6e,
|
||||
0x47, 0xf1, 0x1a, 0x71, 0x1d, 0x29, 0xc5, 0x89, 0x6f, 0xb7, 0x62, 0x0e, 0xaa, 0x18, 0xbe, 0x1b,
|
||||
0xfc, 0x56, 0x3e, 0x4b, 0xc6, 0xd2, 0x79, 0x20, 0x9a, 0xdb, 0xc0, 0xfe, 0x78, 0xcd, 0x5a, 0xf4,
|
||||
0x1f, 0xdd, 0xa8, 0x33, 0x88, 0x07, 0xc7, 0x31, 0xb1, 0x12, 0x10, 0x59, 0x27, 0x80, 0xec, 0x5f,
|
||||
0x60, 0x51, 0x7f, 0xa9, 0x19, 0xb5, 0x4a, 0x0d, 0x2d, 0xe5, 0x7a, 0x9f, 0x93, 0xc9, 0x9c, 0xef,
|
||||
0xa0, 0xe0, 0x3b, 0x4d, 0xae, 0x2a, 0xf5, 0xb0, 0xc8, 0xeb, 0xbb, 0x3c, 0x83, 0x53, 0x99, 0x61,
|
||||
0x17, 0x2b, 0x04, 0x7e, 0xba, 0x77, 0xd6, 0x26, 0xe1, 0x69, 0x14, 0x63, 0x55, 0x21, 0x0c, 0x7d,
|
||||
];
|
||||
|
||||
/// `SubBytes` transformation [FIPS-PUB-197 Section 5.1.1].
|
||||
fn subbytes(xs: Block) -> Block {
|
||||
let mut ret: Block = [0; 16];
|
||||
for i in 0..=15 {
|
||||
ret[i] = SBOX[xs[i] as usize];
|
||||
}
|
||||
ret
|
||||
}
|
||||
|
||||
/// `InvSubBytes` transformation [FIPS-PUB-197 Section 5.3.2].
|
||||
fn inv_subbytes(xs: Block) -> Block {
|
||||
let mut ret: Block = [0; 16];
|
||||
for i in 0..=15 {
|
||||
ret[i] = INVSBOX[xs[i] as usize];
|
||||
}
|
||||
ret
|
||||
}
|
||||
|
||||
/// This function performs the `ShiftRows` transformation [FIPS-PUB-197
|
||||
/// Section 5.1.2]. Here, `ShiftRows` is treated as a permutation of a
|
||||
/// sequence bytes rather than a series of cyclic shifts on a matrix of
|
||||
/// bytes.
|
||||
fn shiftrows(xs: Block) -> Block {
|
||||
static PERM: [usize; 16] = [0, 5, 10, 15, 4, 9, 14, 3, 8, 13, 2, 7, 12, 1, 6, 11];
|
||||
let mut ret: Block = [0; 16];
|
||||
for i in 0..=15 {
|
||||
ret[i] = xs[PERM[i]];
|
||||
}
|
||||
ret
|
||||
}
|
||||
|
||||
/// This function performs the `InvShiftRows` transformation
|
||||
/// [FIPS-PUB-197 Section 5.3.1]. Here, `InvShiftRows` is treated as a
|
||||
/// permutation of a sequence bytes rather than a series of cyclic
|
||||
/// shifts on a matrix of bytes.
|
||||
fn inv_shiftrows(xs: Block) -> Block {
|
||||
static PERM: [usize; 16] = [0, 13, 10, 7, 4, 1, 14, 11, 8, 5, 2, 15, 12, 9, 6, 3];
|
||||
let mut ret: Block = [0; 16];
|
||||
for i in 0..=15 {
|
||||
ret[i] = xs[PERM[i]];
|
||||
}
|
||||
ret
|
||||
}
|
||||
|
||||
/// This is one step of `MixColumns` [FIPS-PUB-197 Section 5.1.3].
|
||||
fn mixcolumns_step([s0, s1, s2, s3]: Word) -> Word {
|
||||
let t0 = mul_bytes(0x02, s0) ^ mul_bytes(0x03, s1) ^ s2 ^ s3;
|
||||
let t1 = s0 ^ mul_bytes(0x02, s1) ^ mul_bytes(0x03, s2) ^ s3;
|
||||
let t2 = s0 ^ s1 ^ mul_bytes(0x02, s2) ^ mul_bytes(0x03, s3);
|
||||
let t3 = mul_bytes(0x03, s0) ^ s1 ^ s2 ^ mul_bytes(0x02, s3);
|
||||
[t0, t1, t2, t3]
|
||||
}
|
||||
|
||||
/// This function performs the `MixColumns` transformation
|
||||
/// [FIPS-PUB-197 Section 5.1.3].
|
||||
fn mixcolumns(
|
||||
[s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]: Block,
|
||||
) -> Block {
|
||||
let [t0, t1, t2, t3] = mixcolumns_step([s0, s1, s2, s3]);
|
||||
let [t4, t5, t6, t7] = mixcolumns_step([s4, s5, s6, s7]);
|
||||
let [t8, t9, t10, t11] = mixcolumns_step([s8, s9, s10, s11]);
|
||||
let [t12, t13, t14, t15] = mixcolumns_step([s12, s13, s14, s15]);
|
||||
[
|
||||
t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15,
|
||||
]
|
||||
}
|
||||
|
||||
/// The is one step of `InvMixColumns` [FIPS-PUB-197 Section 5.3.3].
|
||||
fn inv_mixcolumns_step([s0, s1, s2, s3]: Word) -> Word {
|
||||
let t0 = mul_bytes(0x0e, s0) ^ mul_bytes(0x0b, s1) ^ mul_bytes(0x0d, s2) ^ mul_bytes(0x09, s3);
|
||||
let t1 = mul_bytes(0x09, s0) ^ mul_bytes(0x0e, s1) ^ mul_bytes(0x0b, s2) ^ mul_bytes(0x0d, s3);
|
||||
let t2 = mul_bytes(0x0d, s0) ^ mul_bytes(0x09, s1) ^ mul_bytes(0x0e, s2) ^ mul_bytes(0x0b, s3);
|
||||
let t3 = mul_bytes(0x0b, s0) ^ mul_bytes(0x0d, s1) ^ mul_bytes(0x09, s2) ^ mul_bytes(0x0e, s3);
|
||||
[t0, t1, t2, t3]
|
||||
}
|
||||
|
||||
/// This function performs the `InvMixColumns` transformation
|
||||
/// [FIPS-PUB-197 Section 5.3.3].
|
||||
fn inv_mixcolumns(
|
||||
[s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]: Block,
|
||||
) -> Block {
|
||||
let [t0, t1, t2, t3] = inv_mixcolumns_step([s0, s1, s2, s3]);
|
||||
let [t4, t5, t6, t7] = inv_mixcolumns_step([s4, s5, s6, s7]);
|
||||
let [t8, t9, t10, t11] = inv_mixcolumns_step([s8, s9, s10, s11]);
|
||||
let [t12, t13, t14, t15] = inv_mixcolumns_step([s12, s13, s14, s15]);
|
||||
[
|
||||
t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15,
|
||||
]
|
||||
}
|
||||
|
||||
/// This function performs one round of AES encryption [FIPS-PUB-197
|
||||
/// Section 5.1].
|
||||
fn round(mut xs: Block, ki: Block) -> Block {
|
||||
xs = mixcolumns(shiftrows(subbytes(xs)));
|
||||
for i in 0..=15 {
|
||||
xs[i] ^= ki[i];
|
||||
}
|
||||
xs
|
||||
}
|
||||
|
||||
/// This is an alternate version of the `InvRound` function that is a
|
||||
/// proper inverse of `Round`.
|
||||
fn inv_round(mut xs: Block, ki: Block) -> Block {
|
||||
for i in 0..=15 {
|
||||
xs[i] ^= ki[i];
|
||||
}
|
||||
inv_subbytes(inv_shiftrows(inv_mixcolumns(xs)))
|
||||
}
|
||||
|
||||
/// Takes two `Block`s and returns the first `Block` XOR'd with the
|
||||
/// second.
|
||||
fn xorb(mut a: Block, b: Block) -> Block {
|
||||
for i in 0..=15 {
|
||||
a[i] ^= b[i];
|
||||
}
|
||||
a
|
||||
}
|
||||
|
||||
/// The `Cipher` function performs AES encryption [FIPS-PUB-197
|
||||
/// Section 5.1].
|
||||
#[allow(clippy::needless_range_loop)]
|
||||
#[must_use]
|
||||
pub fn cipher(ks: &[Block], plaintext: Block) -> Block {
|
||||
let pre = xorb(plaintext, ks[0]);
|
||||
let mut mid = pre;
|
||||
for i in 1..(ks.len() - 1) {
|
||||
mid = round(mid, ks[i]);
|
||||
}
|
||||
xorb(shiftrows(subbytes(mid)), ks[ks.len() - 1])
|
||||
}
|
||||
|
||||
/// FFI entrypoint for the `Cipher` function.
|
||||
#[export_name = "Cipher"]
|
||||
pub extern "C" fn cipher_ffi(
|
||||
k: usize,
|
||||
expanded_key_raw: *const Block,
|
||||
pt_raw: *const u8,
|
||||
out_raw: *mut u8,
|
||||
) {
|
||||
let Nr = k / 32 + 6;
|
||||
let expanded_key = get_vec::<Block>(Nr + 1, expanded_key_raw);
|
||||
let pt = get_array::<u8, 16>(pt_raw);
|
||||
let ct = cipher(&expanded_key, pt);
|
||||
output_array::<u8, 16>(&ct, out_raw);
|
||||
}
|
||||
|
||||
/// This is an alternate version of the `InvCipher` function
|
||||
/// [FIPS-PUB-197 Section 5.3]. The following deviates from Algorithm 3
|
||||
/// but is functionally equivalent and more obviously the inverse of
|
||||
/// `Cipher`.
|
||||
#[allow(clippy::needless_range_loop)]
|
||||
#[must_use]
|
||||
pub fn inv_cipher(ks: &[Block], ciphertext: Block) -> Block {
|
||||
let pre = inv_subbytes(inv_shiftrows(xorb(ciphertext, ks[ks.len() - 1])));
|
||||
let mut mid = pre;
|
||||
for i in (1..(ks.len() - 1)).rev() {
|
||||
mid = inv_round(mid, ks[i]);
|
||||
}
|
||||
xorb(mid, ks[0])
|
||||
}
|
||||
|
||||
/// FFI entrypoint for the `InvCipher` function.
|
||||
#[export_name = "InvCipher"]
|
||||
pub extern "C" fn inv_cipher_ffi(
|
||||
k: usize,
|
||||
expanded_key_raw: *const Block,
|
||||
ct_raw: *const u8,
|
||||
out_raw: *mut u8,
|
||||
) {
|
||||
let Nr = k / 32 + 6;
|
||||
let expanded_key = get_vec::<Block>(Nr + 1, expanded_key_raw);
|
||||
let ct = get_array::<u8, 16>(ct_raw);
|
||||
let pt = inv_cipher(&expanded_key, ct);
|
||||
output_array::<u8, 16>(&pt, out_raw);
|
||||
}
|
||||
@@ -0,0 +1,118 @@
|
||||
from pathlib import Path
|
||||
import unittest
|
||||
from saw_client import *
|
||||
from saw_client.crucible import *
|
||||
from saw_client.mir import *
|
||||
from saw_client.proofscript import *
|
||||
from saw_client.mir_type import *
|
||||
|
||||
def ref_to_fresh(c : Contract, ty : MIRType, name : Optional[str] = None,
|
||||
read_only : bool = False) -> Tuple[FreshVar, SetupVal]:
|
||||
"""Add to ``Contract`` ``c`` an allocation of a reference of type ``ty`` initialized to an unknown fresh value.
|
||||
If ``read_only == True`` then the allocated memory is immutable.
|
||||
|
||||
:returns A fresh variable bound to the reference's initial value and the newly allocated reference. (The fresh
|
||||
variable will be assigned ``name`` if provided/available.)"""
|
||||
var = c.fresh_var(ty, name)
|
||||
ptr = c.alloc(ty, points_to = var, read_only = read_only)
|
||||
return (var, ptr)
|
||||
|
||||
# fn F(xs: Block) -> Block {
|
||||
class block_to_block_Contract(Contract):
|
||||
def __init__(self, F : CryptolTerm):
|
||||
super().__init__()
|
||||
self.F = F
|
||||
def specification(self):
|
||||
xs = self.fresh_var(array_ty(16, u8), "xs")
|
||||
self.execute_func(xs)
|
||||
self.returns(cry_f("{self.F} {xs}"))
|
||||
|
||||
def block_to_block_verify(self, mod, F_rust, F_cryptol):
|
||||
result = mir_verify(mod, F_rust, block_to_block_Contract(cry_f(F_cryptol)),
|
||||
script=ProofScript([rme]))
|
||||
self.assertIs(result.is_success(), True)
|
||||
return result
|
||||
|
||||
# fn F(xs: Block, ki: Block) -> Block {
|
||||
# Matches `round` and `inv_round`
|
||||
class round_Contract(Contract):
|
||||
def __init__(self, F : CryptolTerm):
|
||||
super().__init__()
|
||||
self.F = F
|
||||
def specification(self):
|
||||
xs = self.fresh_var(array_ty(16, u8), "xs")
|
||||
ki = self.fresh_var(array_ty(16, u8), "ki")
|
||||
self.execute_func(xs, ki)
|
||||
self.returns(cry_f("{self.F} {xs} {ki}"))
|
||||
|
||||
def round_verify(self, mod, F_rust, F_cryptol, lemmas, script=ProofScript([rme])):
|
||||
result = mir_verify(mod, F_rust, round_Contract(cry_f(F_cryptol)),
|
||||
lemmas=lemmas,
|
||||
script=script)
|
||||
self.assertIs(result.is_success(), True)
|
||||
return result
|
||||
|
||||
# fn F(ks: &[Block], plaintext: Block) -> Block {
|
||||
# Matches `cipher` and `inv_cipher`
|
||||
class cipher_Contract(Contract):
|
||||
def __init__(self, k: int, F: CryptolTerm):
|
||||
super().__init__()
|
||||
self.k = k
|
||||
self.F = F
|
||||
def specification(self):
|
||||
k = cry_f("{self.k} : [32]");
|
||||
(ks, ks_p) = ref_to_fresh(self, array_ty(self.k/32 + 6 + 1, array_ty(16, u8)), name="ks", read_only=True)
|
||||
plaintext = self.fresh_var(array_ty(16, u8), "plaintext")
|
||||
self.execute_func(slice_value(ks_p), plaintext)
|
||||
self.returns(cry_f("{self.F}`{{{self.k}}} {ks} {plaintext}"))
|
||||
|
||||
def cipher_verify(self, mod, k, F_rust, F_cryptol, lemmas, script=ProofScript([rme])):
|
||||
result = mir_verify(mod, F_rust, cipher_Contract(k, cry_f(F_cryptol)),
|
||||
lemmas=lemmas,
|
||||
script=script)
|
||||
self.assertIs(result.is_success(), True)
|
||||
return result
|
||||
|
||||
class Cipher(unittest.TestCase):
|
||||
def test_Cipher(self):
|
||||
connect(reset_server=True)
|
||||
if __name__ == "__main__": view(LogResults(verbose_failure=True))
|
||||
|
||||
basedir = Path(__file__).absolute().parents[1] # Get absolute path to `Cargo.toml`
|
||||
crypath = basedir/"../../Cipher.cry"
|
||||
mirpath = basedir/"linked-mir.json"
|
||||
|
||||
cryptol_load_file(str(crypath))
|
||||
mod = mir_load_module(str(mirpath))
|
||||
|
||||
subbytes_result = block_to_block_verify(self, mod, 'Cipher::subbytes', 'SubBytes')
|
||||
inv_subbytes_result = block_to_block_verify(self, mod, 'Cipher::inv_subbytes', 'InvSubBytes')
|
||||
shiftrows_result = block_to_block_verify(self, mod, 'Cipher::shiftrows', 'ShiftRows')
|
||||
inv_shiftrows_result = block_to_block_verify(self, mod, 'Cipher::inv_shiftrows', 'InvShiftRows')
|
||||
mixcolums_result = block_to_block_verify(self, mod, 'Cipher::mixcolumns', 'MixColumns')
|
||||
inv_mixcolums_result = block_to_block_verify(self, mod, 'Cipher::inv_mixcolumns', 'InvMixColumns')
|
||||
|
||||
round_result = round_verify(self, mod, 'Cipher::round', "Round",
|
||||
lemmas=[subbytes_result, shiftrows_result, mixcolums_result])
|
||||
inv_round_result = round_verify(self, mod, 'Cipher::inv_round', "InvRound'",
|
||||
lemmas=[inv_subbytes_result, inv_shiftrows_result, inv_mixcolums_result],
|
||||
script=ProofScript([z3(["InvSubBytes", "InvShiftRows", "InvMixColumns"])]))
|
||||
|
||||
def cipher_result(k):
|
||||
return cipher_verify(self, mod, k, 'Cipher::cipher', "Cipher",
|
||||
lemmas=[round_result, subbytes_result, shiftrows_result],
|
||||
script=ProofScript([z3(["Round", "SubBytes", "ShiftRows"])]))
|
||||
cipher_128_result = cipher_result(128)
|
||||
cipher_192_result = cipher_result(192)
|
||||
cipher_256_result = cipher_result(256)
|
||||
|
||||
def inv_cipher_result(k):
|
||||
return cipher_verify(self, mod, k, 'Cipher::inv_cipher', "InvCipher'",
|
||||
lemmas=[inv_round_result, inv_subbytes_result, inv_shiftrows_result],
|
||||
script=ProofScript([cvc5(["InvRound", "InvSubBytes", "InvShiftRows"])]))
|
||||
inv_cipher_128_result = inv_cipher_result(128)
|
||||
inv_cipher_192_result = inv_cipher_result(192)
|
||||
inv_cipher_256_result = inv_cipher_result(256)
|
||||
|
||||
if __name__ == "__main__":
|
||||
unittest.main()
|
||||
+22
@@ -0,0 +1,22 @@
|
||||
# This file is automatically @generated by Cargo.
|
||||
# It is not intended for manual editing.
|
||||
version = 3
|
||||
|
||||
[[package]]
|
||||
name = "Cipher"
|
||||
version = "0.1.0"
|
||||
dependencies = [
|
||||
"ffi_utils",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "KeyExpansion"
|
||||
version = "0.1.0"
|
||||
dependencies = [
|
||||
"Cipher",
|
||||
"ffi_utils",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "ffi_utils"
|
||||
version = "0.1.0"
|
||||
@@ -0,0 +1,13 @@
|
||||
[package]
|
||||
name = "KeyExpansion"
|
||||
version = "0.1.0"
|
||||
edition = "2021"
|
||||
|
||||
[lib]
|
||||
name = "KeyExpansion"
|
||||
path = "src/lib.rs"
|
||||
crate-type = ["lib", "cdylib"]
|
||||
|
||||
[dependencies]
|
||||
ffi_utils = { path = "../../../../shared/rust/ffi_utils" }
|
||||
Cipher = { path = "../Cipher" }
|
||||
@@ -0,0 +1,88 @@
|
||||
//! This is a Rust implementation of the `KeyExpansion` method in
|
||||
//! the Advanced Encryption Standard (AES) [FIPS-PUB-197].
|
||||
|
||||
#![allow(non_snake_case)]
|
||||
|
||||
use ffi_utils::{get_vec, output_vec};
|
||||
use Cipher::{Block, Word, SBOX};
|
||||
|
||||
/// This table holds the word array for the round constant
|
||||
/// [FIPS-PUB-197 Sections 2.1 and 5.2]. Constants are used here rather
|
||||
/// than computing the values in place.
|
||||
static RCON: [Word; 11] = [
|
||||
[0x00, 0x00, 0x00, 0x00], // undefined
|
||||
[0x01, 0x00, 0x00, 0x00],
|
||||
[0x02, 0x00, 0x00, 0x00],
|
||||
[0x04, 0x00, 0x00, 0x00],
|
||||
[0x08, 0x00, 0x00, 0x00],
|
||||
[0x10, 0x00, 0x00, 0x00],
|
||||
[0x20, 0x00, 0x00, 0x00],
|
||||
[0x40, 0x00, 0x00, 0x00],
|
||||
[0x80, 0x00, 0x00, 0x00],
|
||||
[0x1b, 0x00, 0x00, 0x00],
|
||||
[0x36, 0x00, 0x00, 0x00],
|
||||
];
|
||||
|
||||
/// This function takes a word [a0,a1,a2,a3] as input and performs a
|
||||
/// cyclic permutation, returning the word [a1,a2,a3,a0] [FIPS-PUB-197
|
||||
/// Section 5.2].
|
||||
fn rotword([a0, a1, a2, a3]: Word) -> Word {
|
||||
[a1, a2, a3, a0]
|
||||
}
|
||||
|
||||
/// This function takes a four-byte input word and applies the S-box to
|
||||
/// each of the four bytes to produce an output word [FIPS-PUB-197
|
||||
/// Section 5.2].
|
||||
fn subword(w: Word) -> Word {
|
||||
let mut ret = [0, 0, 0, 0];
|
||||
for i in 0..=3 {
|
||||
ret[i] = SBOX[w[i] as usize];
|
||||
}
|
||||
ret
|
||||
}
|
||||
|
||||
/// Takes two `Word`s and returns the first `Word` XOR'd with the
|
||||
/// second.
|
||||
fn xorw(mut a: Word, b: Word) -> Word {
|
||||
for i in 0..=3 {
|
||||
a[i] ^= b[i];
|
||||
}
|
||||
a
|
||||
}
|
||||
|
||||
/// This is the main AES key expansion routine [FIPS-PUB-197 Section
|
||||
/// 5.2].
|
||||
#[must_use]
|
||||
pub fn key_expansion(k: usize, key: &[Word]) -> [Block; 15] {
|
||||
let nk = k / 32;
|
||||
let nr = nk + 6;
|
||||
let mut w: [Word; 64] = [[0; 4]; 64];
|
||||
for i in 0..(4 * (nr + 1)) {
|
||||
if i < nk {
|
||||
w[i] = key[i];
|
||||
} else if i % nk == 0 {
|
||||
w[i] = xorw(w[i - nk], xorw(subword(rotword(w[i - 1])), RCON[i / nk]));
|
||||
} else if (i % nk == 4) && (nk > 6) {
|
||||
w[i] = xorw(w[i - nk], subword(w[i - 1]));
|
||||
} else {
|
||||
w[i] = xorw(w[i - nk], w[i - 1]);
|
||||
}
|
||||
}
|
||||
let mut expanded_key: [Block; 15] = [[0u8; 16]; 15];
|
||||
for i in 0..=nr {
|
||||
for j in 0..=15 {
|
||||
expanded_key[i][j] = w[i * 4 + j / 4][j % 4];
|
||||
}
|
||||
}
|
||||
expanded_key
|
||||
}
|
||||
|
||||
/// FFI entrypoint for the `KeyExpansion` function.
|
||||
#[export_name = "KeyExpansion"]
|
||||
pub extern "C" fn key_expansion_ffi(k: usize, key_raw: *const Word, out_raw: *mut Block) {
|
||||
let key = get_vec::<Word>(k / 32, key_raw);
|
||||
let expanded_key = key_expansion(k, &key);
|
||||
let mut expanded_key_vec: Vec<Block> = expanded_key.to_vec();
|
||||
expanded_key_vec.resize(k / 32 + 6 + 1, [0; 16]);
|
||||
output_vec::<Block>(&expanded_key_vec, out_raw);
|
||||
}
|
||||
@@ -0,0 +1,78 @@
|
||||
from pathlib import Path
|
||||
import unittest
|
||||
from saw_client import *
|
||||
from saw_client.crucible import *
|
||||
from saw_client.mir import *
|
||||
from saw_client.proofscript import *
|
||||
from saw_client.mir_type import *
|
||||
|
||||
def ref_to_fresh(c : Contract, ty : MIRType, name : Optional[str] = None,
|
||||
read_only : bool = False) -> Tuple[FreshVar, SetupVal]:
|
||||
"""Add to ``Contract`` ``c`` an allocation of a reference of type ``ty`` initialized to an unknown fresh value.
|
||||
If ``read_only == True`` then the allocated memory is immutable.
|
||||
|
||||
:returns A fresh variable bound to the reference's initial value and the newly allocated reference. (The fresh
|
||||
variable will be assigned ``name`` if provided/available.)"""
|
||||
var = c.fresh_var(ty, name)
|
||||
ptr = c.alloc(ty, points_to = var, read_only = read_only)
|
||||
return (var, ptr)
|
||||
|
||||
# fn subword(w: Word) -> Word
|
||||
class subword_Contract(Contract):
|
||||
def specification(self):
|
||||
a = self.fresh_var(array_ty(4, u8), "a")
|
||||
|
||||
self.execute_func(a)
|
||||
|
||||
self.returns(cry_f("SubWord {a}"))
|
||||
|
||||
# pub fn key_expansion(k: usize, key: &[Word]) -> Vec<Block>
|
||||
class key_expansion_Contract(Contract):
|
||||
def __init__(self, k : int):
|
||||
super().__init__()
|
||||
self.k = k
|
||||
def specification(self):
|
||||
k = cry_f("{self.k} : [64]");
|
||||
(key, key_p) = ref_to_fresh(self, array_ty(self.k // 32, array_ty(4, u8)), name="key", read_only=True)
|
||||
|
||||
self.execute_func(k, slice_value(key_p))
|
||||
|
||||
# The use of slices means the potentially unused part of the
|
||||
# 15-block array is all zeros and we need to account for them.
|
||||
key_from_cryptol = cry_f("KeyExpansion`{{{self.k}}} {key} # zero : [15][16][8]")
|
||||
|
||||
self.returns(key_from_cryptol)
|
||||
|
||||
class KeyExpansion(unittest.TestCase):
|
||||
def test_KeyExpansion(self):
|
||||
connect(reset_server=True)
|
||||
if __name__ == "__main__": view(LogResults(verbose_failure=True))
|
||||
|
||||
basedir = Path(__file__).absolute().parents[1] # Get absolute path to `Cargo.toml`
|
||||
crypath = basedir/"../../KeyExpansion.cry"
|
||||
mirpath = basedir/"linked-mir.json"
|
||||
|
||||
cryptol_load_file(str(crypath))
|
||||
mod = mir_load_module(str(mirpath))
|
||||
|
||||
subword_result = mir_verify(mod,
|
||||
'KeyExpansion::subword',
|
||||
subword_Contract(),
|
||||
script=ProofScript([rme]))
|
||||
self.assertIs(subword_result.is_success(), True)
|
||||
|
||||
def key_expand_result(k):
|
||||
result = mir_verify(mod,
|
||||
'KeyExpansion::key_expansion',
|
||||
key_expansion_Contract(k),
|
||||
lemmas=[subword_result],
|
||||
script=ProofScript([z3(["SubWord"])]))
|
||||
self.assertIs(result.is_success(), True)
|
||||
return result
|
||||
|
||||
key_expand_128_result = key_expand_result(128)
|
||||
key_expand_192_result = key_expand_result(192)
|
||||
key_expand_256_result = key_expand_result(256)
|
||||
|
||||
if __name__ == "__main__":
|
||||
unittest.main()
|
||||
@@ -0,0 +1,143 @@
|
||||
/*
|
||||
* This is a SAW script that guides SAW to prove the properties found
|
||||
* in `algorithms/AES/Cipher.cry`.
|
||||
*/
|
||||
|
||||
// Include common SAW utilities.
|
||||
include "../../../shared/SAW/utils.saw";
|
||||
|
||||
// Import the Cryptol specification for AES's `Cipher` and `InvCipher`
|
||||
// routines.
|
||||
import "../Cipher.cry";
|
||||
|
||||
let verify_SubBytesInverts : TopLevel Theorem =
|
||||
proveit {{ SubBytesInverts }} rme;
|
||||
|
||||
let verify_ShiftRowsInverts : TopLevel Theorem =
|
||||
proveit {{ ShiftRowsInverts }} rme;
|
||||
|
||||
let verify_MixColumnsStepInverts : TopLevel Theorem =
|
||||
proveit {{ MixColumnsStepInverts }} rme;
|
||||
|
||||
let verify_MixColumnsInverts : TopLevel Theorem =
|
||||
do {
|
||||
MixColumnsStepInverts_lemma <- verify_MixColumnsStepInverts;
|
||||
|
||||
proveit {{ MixColumnsInverts }}
|
||||
do {
|
||||
goal_eval_unint ["InvMixColumnsStep", "MixColumnsStep"];
|
||||
use_lemmas [ MixColumnsStepInverts_lemma ];
|
||||
goal_eval; trivial;
|
||||
};
|
||||
};
|
||||
|
||||
let verify_AddRoundKeyInvolution : TopLevel Theorem =
|
||||
proveit {{ AddRoundKeyInvolution }} rme;
|
||||
|
||||
let verify_RoundInverts : TopLevel Theorem =
|
||||
do {
|
||||
AddRoundKeyInvolution_lemma <- verify_AddRoundKeyInvolution;
|
||||
SubBytesInverts_lemma <- verify_SubBytesInverts;
|
||||
ShiftRowsInverts_lemma <- verify_ShiftRowsInverts;
|
||||
MixColumnsInverts_lemma <- verify_MixColumnsInverts;
|
||||
|
||||
proveit {{ RoundInverts }}
|
||||
do {
|
||||
goal_eval_unint [ "AddRoundKey"
|
||||
, "SubBytes" , "InvSubBytes"
|
||||
, "ShiftRows" , "InvShiftRows"
|
||||
, "MixColumns", "InvMixColumns"
|
||||
];
|
||||
use_lemmas [ AddRoundKeyInvolution_lemma
|
||||
, SubBytesInverts_lemma
|
||||
, ShiftRowsInverts_lemma
|
||||
, MixColumnsInverts_lemma
|
||||
];
|
||||
goal_eval; trivial;
|
||||
};
|
||||
};
|
||||
|
||||
// This parameterized lemma will be proven at all 3 key sizes (128,
|
||||
// 192, and 256).
|
||||
|
||||
let verify_InvCipherEquivalence (KeySize : Int) : TopLevel Theorem =
|
||||
do {
|
||||
proveit {{ InvCipherEquivalence`{KeySize} }}
|
||||
do {
|
||||
goal_eval_unint [ "AddRoundKey"
|
||||
, "InvSubBytes"
|
||||
, "InvShiftRows"
|
||||
, "InvMixColumns"
|
||||
];
|
||||
simplify (addsimp (core_thm "bvEq_refl") empty_ss);
|
||||
goal_eval; trivial;
|
||||
};
|
||||
};
|
||||
|
||||
let verify_CipherInverts (KeySize : Int) : TopLevel Theorem =
|
||||
do {
|
||||
AddRoundKeyInvolution_lemma <- verify_AddRoundKeyInvolution;
|
||||
SubBytesInverts_lemma <- verify_SubBytesInverts;
|
||||
ShiftRowsInverts_lemma <- verify_ShiftRowsInverts;
|
||||
MixColumnsInverts_lemma <- verify_MixColumnsInverts;
|
||||
|
||||
proveit {{ CipherInverts`{KeySize} }}
|
||||
do {
|
||||
goal_eval_unint [ "AddRoundKey"
|
||||
, "SubBytes" , "InvSubBytes"
|
||||
, "ShiftRows" , "InvShiftRows"
|
||||
, "MixColumns", "InvMixColumns"
|
||||
];
|
||||
use_lemmas [ AddRoundKeyInvolution_lemma
|
||||
, SubBytesInverts_lemma
|
||||
, ShiftRowsInverts_lemma
|
||||
, MixColumnsInverts_lemma
|
||||
];
|
||||
goal_eval; trivial;
|
||||
};
|
||||
};
|
||||
|
||||
// This parameterized lemma will be proven at all 3 key sizes (128,
|
||||
// 192, and 256).
|
||||
|
||||
let verify_CipherInverts' (KeySize : Int) : TopLevel Theorem =
|
||||
do {
|
||||
AddRoundKeyInvolution_lemma <- verify_AddRoundKeyInvolution;
|
||||
SubBytesInverts_lemma <- verify_SubBytesInverts;
|
||||
ShiftRowsInverts_lemma <- verify_ShiftRowsInverts;
|
||||
RoundInverts_lemma <- verify_RoundInverts;
|
||||
|
||||
proveit {{ CipherInverts'`{KeySize} }}
|
||||
do {
|
||||
goal_eval_unint [ "AddRoundKey"
|
||||
, "SubBytes" , "InvSubBytes"
|
||||
, "ShiftRows", "InvShiftRows"
|
||||
, "Round" , "InvRound'"
|
||||
];
|
||||
use_lemmas [ AddRoundKeyInvolution_lemma
|
||||
, SubBytesInverts_lemma
|
||||
, ShiftRowsInverts_lemma
|
||||
, RoundInverts_lemma
|
||||
];
|
||||
goal_eval; trivial;
|
||||
};
|
||||
};
|
||||
|
||||
/*
|
||||
* Verify public properties of `algorithms::AES::Cipher`.
|
||||
*/
|
||||
let main : TopLevel [Theorem] = do {
|
||||
CipherInverts_lemmas <- for [128, 192, 256] verify_CipherInverts;
|
||||
CipherInverts'_lemmas <- for [128, 192, 256] verify_CipherInverts';
|
||||
InvCipherEquivalence_lemmas <- for [128, 192, 256] verify_InvCipherEquivalence;
|
||||
|
||||
summarize_verification;
|
||||
|
||||
return
|
||||
(foldl concat []
|
||||
[ CipherInverts_lemmas
|
||||
, CipherInverts'_lemmas
|
||||
, InvCipherEquivalence_lemmas
|
||||
]
|
||||
);
|
||||
};
|
||||
@@ -0,0 +1,24 @@
|
||||
/*
|
||||
* This is a SAW script that guides SAW to prove the properties found
|
||||
* in `algorithms/AES/GF28.cry`.
|
||||
*/
|
||||
|
||||
// Include common SAW utilities.
|
||||
include "../../../shared/SAW/utils.saw";
|
||||
|
||||
// Import the AES Cryptol GF(2^^8) functions.
|
||||
import "../GF28.cry";
|
||||
|
||||
let verify_GF28MultiplicationCorrect : TopLevel Theorem =
|
||||
proveit {{ GF28MultiplicationCorrect }} rme;
|
||||
|
||||
/*
|
||||
* Verify public properties of `algorithms::AES::GF28`.
|
||||
*/
|
||||
let main : TopLevel [Theorem] = do {
|
||||
GF28MultiplicationCorrect_lemma <- verify_GF28MultiplicationCorrect;
|
||||
|
||||
summarize_verification;
|
||||
|
||||
return [GF28MultiplicationCorrect_lemma];
|
||||
};
|
||||
@@ -0,0 +1,47 @@
|
||||
/*
|
||||
* This is a SAW script that guides SAW to prove the properties found
|
||||
* in `algorithms/AES/Main.cry`.
|
||||
*/
|
||||
|
||||
// Include common SAW utilities.
|
||||
include "../../../shared/SAW/utils.saw";
|
||||
|
||||
// Include theorems from `Cipher` for use as lemmas.
|
||||
include "Cipher.saw";
|
||||
|
||||
// Import the Cryptol specification for AES's `Encrypt` and `Decrypt`
|
||||
// routines.
|
||||
import "../Main.cry";
|
||||
import "../Types.cry";
|
||||
|
||||
// This helper lemma rewrites away the `split (join ...)` between
|
||||
// `decrypt` and `encrypt` in the `encryptInverts` proof goal.
|
||||
let verify_split_join : TopLevel Theorem =
|
||||
proveit {{ \(xs : Block) -> split (join xs) == xs }} rme;
|
||||
|
||||
// This parameterized lemma will be proven at all 3 key sizes (128,
|
||||
// 192, and 256).
|
||||
|
||||
let verify_EncryptInverts (keySize : Int) : TopLevel Theorem =
|
||||
do {
|
||||
split_join_lemma <- verify_split_join;
|
||||
CipherInverts_lemma_keySize <- verify_CipherInverts keySize;
|
||||
|
||||
proveit {{ EncryptInverts`{keySize} }}
|
||||
do {
|
||||
goal_eval_unint [ "split", "join", "InvCipher", "Cipher" ];
|
||||
use_lemmas [ split_join_lemma, CipherInverts_lemma_keySize ];
|
||||
goal_eval; trivial;
|
||||
};
|
||||
};
|
||||
|
||||
/*
|
||||
* Verify public properties of `algorithms::AES::Main`.
|
||||
*/
|
||||
let main : TopLevel [Theorem] = do {
|
||||
EncryptInverts_lemmas <- for [128, 192, 256] verify_EncryptInverts;
|
||||
|
||||
summarize_verification;
|
||||
|
||||
return EncryptInverts_lemmas;
|
||||
};
|
||||
@@ -0,0 +1,24 @@
|
||||
/*
|
||||
* This is a SAW script that guides SAW to prove the properties found
|
||||
* in `algorithms/AES/SBox.cry`.
|
||||
*/
|
||||
|
||||
// Include common SAW utilities.
|
||||
include "../../../shared/SAW/utils.saw";
|
||||
|
||||
// Import the Cryptol specification for AES's `SBox`es.
|
||||
import "../SBox.cry";
|
||||
|
||||
let verify_SBoxInverts : TopLevel Theorem =
|
||||
proveit {{ SBoxInverts }} rme;
|
||||
|
||||
/*
|
||||
* Verify public properties of `algorithms::AES::SBox`.
|
||||
*/
|
||||
let main : TopLevel [Theorem] = do {
|
||||
SBoxInverts_lemma <- verify_SBoxInverts;
|
||||
|
||||
summarize_verification;
|
||||
|
||||
return [SBoxInverts_lemma];
|
||||
};
|
||||
@@ -0,0 +1,42 @@
|
||||
/*
|
||||
* This is a SAW script that guides SAW to prove the properties found
|
||||
* in `algorithms/AES`.
|
||||
*/
|
||||
|
||||
// Include common SAW utilities.
|
||||
include "../../../shared/SAW/utils.saw";
|
||||
|
||||
include "Main.saw";
|
||||
let Main_main = main;
|
||||
|
||||
include "GF28.saw";
|
||||
let GF28_main = main;
|
||||
|
||||
include "SBox.saw";
|
||||
let SBox_main = main;
|
||||
|
||||
include "Cipher.saw";
|
||||
let Cipher_main = main;
|
||||
|
||||
/*
|
||||
* Script to run on command line:
|
||||
* `saw all.saw`
|
||||
* Return:
|
||||
* `TopLevel [Theorem]` verifying all lemmas used throughout `algorithms/AES`.
|
||||
*/
|
||||
let main : TopLevel [Theorem] = do {
|
||||
Main_lemmas <- Main_main;
|
||||
GF28_lemmas <- GF28_main;
|
||||
SBox_lemmas <- SBox_main;
|
||||
Cipher_lemmas <- Cipher_main;
|
||||
|
||||
summarize_verification;
|
||||
|
||||
return
|
||||
(foldl concat []
|
||||
[ Main_lemmas
|
||||
, GF28_lemmas
|
||||
, SBox_lemmas
|
||||
, Cipher_lemmas
|
||||
]);
|
||||
};
|
||||
@@ -0,0 +1,13 @@
|
||||
# Bibliography
|
||||
|
||||
[NSA19] U.S. National Security Agency. Mathematical routines for the
|
||||
NIST prime elliptic curves. November 19, 2019.
|
||||
|
||||
[FIPS186-5] National Institute of Standards and Technology. FIPS
|
||||
186-5. Digital Signature Standard (DSS). February 3, 2023.
|
||||
https://doi.org/10.6028/NIST.FIPS.186-5
|
||||
|
||||
[NISTSP800-186] Recommendations for Discrete Logarithm-based
|
||||
Cryptography: Elliptic Curve Domain Parameters. NIST SP
|
||||
800-186. February 2023.
|
||||
https://doi.org/10.6028/NIST.SP.800-186
|
||||
@@ -0,0 +1,206 @@
|
||||
/*
|
||||
* Description: This module provides ECDSA signature creation and
|
||||
* verification routines for the NIST elliptic curves P-192, P-224,
|
||||
* P-256, P-384, and P-521 [FIPS186-5].
|
||||
*/
|
||||
|
||||
module algorithms::ECDSA::ECDSA where
|
||||
|
||||
import shared::common::utils::TypeCoercion (ZtoZ)
|
||||
import shared::common::utils::Enum (unwrap)
|
||||
import algorithms::ECDSA::Routines as Routines where
|
||||
type p = _p
|
||||
b = _b
|
||||
mp_mod_sqrt = _mp_mod_sqrt
|
||||
|
||||
parameter
|
||||
/**
|
||||
* `p` is an odd prime number > 3 [NSA19 Section 1], used to make an
|
||||
* elliptic curve over `GF(p)`.
|
||||
*/
|
||||
type p : #
|
||||
type constraint (fin p, prime p, p > 8) // `p > 8` comes from scalar multiplications.
|
||||
|
||||
/**
|
||||
* An elliptic curve over `GF(p)` has an order, which is the
|
||||
* smallest positive integer `n` such that for any point `S`, `nS =
|
||||
* O`. The order of each of the NIST elliptic curves is prime [NSA19
|
||||
* Section 2.2].
|
||||
*/
|
||||
type n : #
|
||||
type constraint (prime n, p >= n)
|
||||
|
||||
/**
|
||||
* Elliptic curve parameter. y ^^ 2 == x ^^ 3 - 3 * x + b [NSA19
|
||||
* Section 1].
|
||||
*/
|
||||
b : Z p
|
||||
|
||||
/** Base point for an elliptic curve group [NSA19 Section 1]. */
|
||||
G : { x : Z p, y : Z p, z : Z p }
|
||||
|
||||
/**
|
||||
* Modular square root function specialized on `p` [NSA19 Section
|
||||
* 3.2].
|
||||
*/
|
||||
mp_mod_sqrt : Z p -> Z p
|
||||
|
||||
/* Workaround for parameter hiding */
|
||||
type _p = p
|
||||
_b = b
|
||||
_mp_mod_sqrt = mp_mod_sqrt
|
||||
|
||||
/**
|
||||
* ECDSA Signature Generation Algorithm [FIPS186-5 Section 6.4.1].
|
||||
*
|
||||
* Inputs:
|
||||
* `M`: Bit string to be signed.
|
||||
* `d`: Private key in the interval [1, n-1].
|
||||
* `Hash`: an approved hash function [FIPS186-5 Section 2.3].
|
||||
* `k`: a per-message secret number (0 < k < n).
|
||||
*
|
||||
* Outputs:
|
||||
* `(r, s)`: A pair of integers each in the interval `[1, n-1].
|
||||
*
|
||||
* Types:
|
||||
* `hashlen`: The digest size of `Hash` [FIPS186-5 Section 6.4.1].
|
||||
*/
|
||||
sign :
|
||||
{ hashlen, a }
|
||||
( fin hashlen, fin a )
|
||||
=> [a] -> Z n -> ([a] -> [hashlen]) -> Z n -> Result (Z n, Z n) (String _)
|
||||
sign M d Hash k =
|
||||
if d == 0 \/ r == 0 \/ s == 0 then
|
||||
Err "failure"
|
||||
else Ok (r, s)
|
||||
where
|
||||
// 1. Compute `H = Hash(M)`
|
||||
H = Hash M : [hashlen]
|
||||
// 2(a). If `len(n) ≥ hashlen`, set `E = H`. Otherwise, set `E`
|
||||
// equal to the leftmost `log2(n)` bits of `H`.
|
||||
E = take H : [min (width n) hashlen]
|
||||
// 2(b). Convert the bit string `E` to the integer `e`.
|
||||
e = fromInteger (toInteger E) : Z n
|
||||
// 4. Compute `k^^-1 mod n`.
|
||||
k' = recip k
|
||||
// 5. Compute the elliptic curve point `R = [k]G`.
|
||||
R = Routines::ec_mult (ZtoZ k) G
|
||||
// 6. Set `xR` to x-coordinate of the affine representation of the
|
||||
// point `R = (xR, yR)`. By definition of 'order', `[k]G` is not
|
||||
// the point at infinity, and so the Affine transformation of
|
||||
// `[k]G` will not fail. Hence `unwrap` here is safe to use.
|
||||
{x = xR, y = _} = unwrap (ec_affinify R)
|
||||
// 7. Convert the field element `xR` to the integer `r1`.
|
||||
r1 = fromZ xR
|
||||
// 8. Set `r = r1 mod n`
|
||||
r = fromInteger r1 : Z n
|
||||
// 9. Compute `s = `k^^-1 * (e + r * d) mod n`
|
||||
s = k' * (e + r * d)
|
||||
|
||||
/**
|
||||
* ECDSA Signature Verification Algorithm [FIPS186-5 Section 6.4.2].
|
||||
*
|
||||
* Inputs:
|
||||
* `M`: A message
|
||||
* `(r, s)`: A pair of integers.
|
||||
* `Q`: A purported signature verification key.
|
||||
* `Hash`: an approved hash function [FIPS186-5 Section 2.3].
|
||||
*
|
||||
* Outputs:
|
||||
* A Boolean value denoting "accept" (`True`) or "reject" (`False`).
|
||||
*
|
||||
* Types:
|
||||
* `hashlen`: The digest size of `Hash` [FIPS186-5 Section 6.4.1].
|
||||
*/
|
||||
verify :
|
||||
{ hashlen, a }
|
||||
( fin hashlen, fin a )
|
||||
=> [a] -> (Z n, Z n) -> ProjectivePoint -> ([a] -> [hashlen]) -> Bool
|
||||
verify M (r, s) Q Hash =
|
||||
// 1. Verify that both `r` and `s` are integers in the interval
|
||||
// `[1, n − 1]`. Output “reject” if verification fails.
|
||||
if r == 0 \/ s == 0 \/ affinifyFailed \/ r1VerificationFailed then
|
||||
False
|
||||
else True
|
||||
where
|
||||
// 2. Compute `H = Hash(M)`
|
||||
H = Hash M : [hashlen]
|
||||
// 3(a). If `len(n) ≥ hashlen`, set `E = H`. Otherwise, set `E`
|
||||
// equal to the leftmost `log2(n)` bits of `H`.
|
||||
E = take H : [min (width n) hashlen]
|
||||
// 3(b). Convert the bit string `E` to the integer `e`.
|
||||
e = fromInteger (toInteger E) : Z n
|
||||
// 4. Compute `s^^-1 mod n`.
|
||||
s' = recip s
|
||||
// 5. Compute `u = e * s^^-1` and `v = r * s^^-1`.
|
||||
(u, v) = (e * s', r * s')
|
||||
// 6. Compute `R1 = [u]G + [v]Q`.
|
||||
R1 = Routines::ec_twin_mult (ZtoZ u) G (ZtoZ v) Q
|
||||
// 7. Set `xR` to x-coordinate of the affine representation of the
|
||||
// point `R1 = (xR, yR)`.
|
||||
({x = xR, y = _}, affinifyFailed) =
|
||||
case (ec_affinify R1) of
|
||||
Ok a -> (a, False)
|
||||
Err _ -> (undefined, True)
|
||||
// 8. Convert the field element `xR` to the integer `r1`.
|
||||
r1 = fromZ xR
|
||||
// 9. Verify that `r = r1 mod n`
|
||||
r1VerificationFailed = r != fromInteger r1
|
||||
|
||||
/**
|
||||
* ECDSA Key Pair Generation [FIPS186-5 Section A.2.1]. Essentially
|
||||
* step 5.
|
||||
*/
|
||||
private_to_public : Z n -> ProjectivePoint
|
||||
private_to_public d = Routines::ec_mult (ZtoZ d) G
|
||||
|
||||
/**
|
||||
* Routine 2.2.2: Create an affine point `R` from a projective point
|
||||
* `S` [NSA19 Section 2.2].
|
||||
*/
|
||||
ec_affinify : ProjectivePoint -> Result AffinePoint (String _)
|
||||
ec_affinify = Routines::ec_affinify
|
||||
|
||||
/**
|
||||
* "The affine representations of `S` is a pair `S = (Sx, Sy)` of
|
||||
* elements of `GF(p)` which satisfy the defining equation [NSA19
|
||||
* Section 2.2]."
|
||||
*/
|
||||
type AffinePoint = Routines::AffinePoint
|
||||
|
||||
/**
|
||||
* A projective representation of `S` is a triple `S = (Sx, Sy, Sz) of
|
||||
* elements of `GF(p)`, such that `Sy ^^ 2 == Sx ^^ 3 * Sz ^^ 4 + b *
|
||||
* Sz ^^ 6 (mod p)` [NSA19 Section 2.2].
|
||||
*/
|
||||
type ProjectivePoint = Routines::ProjectivePoint
|
||||
|
||||
/**
|
||||
* Routine 2.2.3: Set `Rbar` to compressed `Sbar` from an affine point
|
||||
* `S` [NSA19 Section 2.2].
|
||||
*/
|
||||
ec_compress : AffinePoint -> [2 + width p]
|
||||
ec_compress = Routines::ec_compress
|
||||
|
||||
/**
|
||||
* Routine 2.2.4: Create an affine point `R` from compressed `Sbar`
|
||||
* [NSA19 Section 2.2].
|
||||
*/
|
||||
ec_decompress : [2 + width p] -> Result AffinePoint (String _)
|
||||
ec_decompress = Routines::ec_decompress
|
||||
|
||||
/**
|
||||
* Use `G` as a generator to produce random affine points and test the
|
||||
* compression and decompression algorithms.
|
||||
*
|
||||
* ```
|
||||
* :check decompress_correct
|
||||
* ```
|
||||
*/
|
||||
decompress_correct : Z n -> Bool
|
||||
property decompress_correct x =
|
||||
affine_decompress_correct (unwrap (ec_affinify (Routines::ec_mult (ZtoZ x) G)))
|
||||
where
|
||||
affine_decompress_correct : AffinePoint -> Bool
|
||||
affine_decompress_correct R =
|
||||
R == unwrap (ec_decompress (ec_compress R))
|
||||
@@ -0,0 +1,313 @@
|
||||
/*
|
||||
* Description: This module provides "routines for implementing
|
||||
* primitives for elliptic curve cryptography on the NIST elliptic
|
||||
* curves P-192, P-224, P-256, P-384, P-521" [NSA19].
|
||||
*/
|
||||
|
||||
module algorithms::ECDSA::Routines where
|
||||
|
||||
import shared::common::utils::TypeCoercion (BVtoZ, ZtoZ, ZtoBV)
|
||||
import shared::common::utils::Enum
|
||||
|
||||
parameter
|
||||
/**
|
||||
* `p` is an odd prime number > 3 [NSA19 Section 1], used to make an
|
||||
* elliptic curve over `GF(p)`.
|
||||
*/
|
||||
type p : #
|
||||
type constraint (fin p, prime p, p > 8) // `p > 8` comes from scalar multiplications.
|
||||
|
||||
/**
|
||||
* Elliptic curve parameter. y ^^ 2 == x ^^ 3 - 3 * x + b [NSA19
|
||||
* Section 1].
|
||||
*/
|
||||
b : Z p
|
||||
|
||||
/**
|
||||
* Modular square root function specialized on `p` [NSA19 Section
|
||||
* 3.2].
|
||||
*/
|
||||
mp_mod_sqrt : Z p -> Z p
|
||||
|
||||
/**
|
||||
* Bit-length of `p` [NSA19 Section 1].
|
||||
*/
|
||||
type n = width p
|
||||
|
||||
/**
|
||||
* "The affine representations of `S` is a pair `S = (Sx, Sy)` of
|
||||
* elements of `GF(p)` which satisfy the defining equation [NSA19
|
||||
* Section 2.2]."
|
||||
*/
|
||||
type AffinePoint = { x : Z p, y : Z p }
|
||||
|
||||
/**
|
||||
* A projective representation of `S` is a triple `S = (Sx, Sy, Sz) of
|
||||
* elements of `GF(p)`, such that `Sy ^^ 2 == Sx ^^ 3 * Sz ^^ 4 + b *
|
||||
* Sz ^^ 6 (mod p)` [NSA19 Section 2.2].
|
||||
*/
|
||||
type ProjectivePoint = { x : Z p, y : Z p, z : Z p }
|
||||
|
||||
/**
|
||||
* "The point at infinity, or the identity [NSA19 Section 2.2."
|
||||
*/
|
||||
O : ProjectivePoint
|
||||
O = { x = 1, y = 1, z = 0 }
|
||||
|
||||
/**
|
||||
* Routine 2.2.1: Create a projective point `R` from an affine point
|
||||
* `S` [NSA19 Section 2.2].
|
||||
*/
|
||||
ec_projectify : AffinePoint -> ProjectivePoint
|
||||
ec_projectify S = R
|
||||
where R = { x = S.x
|
||||
, y = S.y
|
||||
, z = 1
|
||||
}
|
||||
|
||||
/**
|
||||
* Routine 2.2.2: Create an affine point `R` from a projective point
|
||||
* `S` [NSA19 Section 2.2].
|
||||
*/
|
||||
ec_affinify : ProjectivePoint -> Result AffinePoint (String _)
|
||||
ec_affinify S =
|
||||
if S.z == 0 then
|
||||
Err "Cannot affinify the point at infinity"
|
||||
else Ok R
|
||||
where
|
||||
lambda = recip S.z
|
||||
R = { x = lambda ^^ 2 * S.x
|
||||
, y = lambda ^^ 3 * S.y
|
||||
}
|
||||
|
||||
/**
|
||||
* This is a helper function to deterine whether a given point is on
|
||||
* the curve [NSA19 Section 1].
|
||||
*/
|
||||
pointIsOnCurve : AffinePoint -> Bool
|
||||
pointIsOnCurve { x = x, y = y } =
|
||||
y ^^ 2 == x ^^ 3 - 3 * x + b
|
||||
|
||||
/**
|
||||
* Routine 2.2.3: Set `Rbar` to compressed `Sbar` from an affine point
|
||||
* `S` [NSA19 Section 2.2].
|
||||
*/
|
||||
ec_compress : AffinePoint -> [2 + width p]
|
||||
ec_compress S = Rbar
|
||||
where
|
||||
Rbar = drop (2 + (Sy % 2)) # Sx
|
||||
Sx = ZtoBV S.x : [width p]
|
||||
Sy = ZtoBV S.y : [width p]
|
||||
|
||||
/**
|
||||
* Routine 2.2.4: Create an affine point `R` from compressed `Sbar`
|
||||
* [NSA19 Section 2.2].
|
||||
*/
|
||||
ec_decompress : [2 + width p] -> Result AffinePoint (String _)
|
||||
ec_decompress S = R
|
||||
where
|
||||
c = toInteger (take S : [2])
|
||||
Rx = BVtoZ (drop S : [width p]) : Z p
|
||||
t0 = Rx ^^ 3 - 3 * Rx + b
|
||||
t1 = mp_mod_sqrt t0
|
||||
Ry = if fromZ t1 % 2 == c % 2 then
|
||||
t1
|
||||
else
|
||||
-t1
|
||||
R = if t1 ^^ 2 != t0 then
|
||||
Err "no such point"
|
||||
else
|
||||
Ok { x = Rx, y = Ry }
|
||||
|
||||
/**
|
||||
* Property demonstrating that `mp_mod_sqrt` is correct.
|
||||
*
|
||||
* ```
|
||||
* :check decompress_correct
|
||||
* ```
|
||||
*/
|
||||
mp_mod_sqrt_correct : Z p -> Bool
|
||||
property mp_mod_sqrt_correct x =
|
||||
(mp_mod_sqrt (x ^^ 2)) ^^ 2 == (x ^^ 2)
|
||||
|
||||
/**
|
||||
* Routine 2.2.5: Check whether the affine point `S` is on the curve
|
||||
* [NSA19 Section 2.2].
|
||||
*/
|
||||
ec_is_point_affine : AffinePoint -> Bool
|
||||
ec_is_point_affine S = S.y ^^ 2 == t
|
||||
where t = S.x ^^ 3 - 3 * S.x + b
|
||||
|
||||
/**
|
||||
* Routine 2.2.6: Set `R` to `2S` [NSA19 Section 2.2].
|
||||
*/
|
||||
ec_double : ProjectivePoint -> ProjectivePoint
|
||||
ec_double S =
|
||||
if S.z == 0 then
|
||||
{ x = 1, y = 1, z = 0 } // 5: R <- (1, 1, 0) and return */
|
||||
else
|
||||
{ x = r18, y = r23, z = r13 }
|
||||
where
|
||||
r7 = S.z ^^ 2 // 7: t4 <- t3 ^^ 2
|
||||
r8 = S.x - r7 // 8: t5 <- t1 - t4
|
||||
r9 = S.x + r7 // 9: t4 <- t1 + t4
|
||||
r10 = r9 * r8 // 10: t5 <- t4 * t5
|
||||
r11 = 3 * r10 // 11: t4 <- 3 * t5
|
||||
r12 = S.z * S.y // 12: t3 <- t3 * t2
|
||||
r13 = 2 * r12 // 13: t3 <- 2 * t3
|
||||
r14 = S.y ^^ 2 // 14: t2 <- t2 ^^ 2
|
||||
r15 = S.x * r14 // 15: t5 <- t1 * t2
|
||||
r16 = 4 * r15 // 16: t5 <- 4 * t5
|
||||
r17 = r11 ^^ 2 // 17: t1 <- t4 ^^ 2
|
||||
r18 = r17 - 2 * r16 // 18: t1 <- t1 - 2 * t5
|
||||
r19 = r14 ^^ 2 // 19: t2 <- t2 ^^ 2
|
||||
r20 = 8 * r19 // 20: t2 <- 8 * t2
|
||||
r21 = r16 - r18 // 21: t5 <- t5 - t1
|
||||
r22 = r11 * r21 // 22: t5 <- t4 * t5
|
||||
r23 = r22 - r20 // 23: t2 <- t5 - t2
|
||||
|
||||
/**
|
||||
* Routine 2.2.7: Set `R` to `S + T`. Set `R` to `(0, 0, 0)` if `S ==
|
||||
* T` [NSA19 Section 2.2].
|
||||
*/
|
||||
ec_add : ProjectivePoint -> ProjectivePoint -> ProjectivePoint
|
||||
ec_add S T =
|
||||
if r13 == 0 then
|
||||
if r14 == 0 then
|
||||
{ x = 0, y = 0, z = 0 } // 17: R <- (0, 0, 0) and return */
|
||||
else
|
||||
{ x = 1, y = 1, z = 0 } // 19: R <- (1, 1, 0) and return */
|
||||
else
|
||||
{ x = r32, y = r37, z = r27 }
|
||||
where
|
||||
r4 = T.z ^^ 2 // 4: t7 <- t6 ^^ 2
|
||||
r5 = S.x * r4 // 5: t1 <- t1 * t7
|
||||
r6 = T.z * r4 // 6: t7 <- t6 * t7
|
||||
r7 = S.y * r6 // 7: t2 <- t2 * t7
|
||||
|
||||
// Covers cases on lines 2-7 and 24-26.
|
||||
(t1, t2, t3) = if T.z != 1 then (r5, r7, r25) else (S.x, S.y, S.z)
|
||||
|
||||
r9 = S.z ^^ 2 // 9: t7 <- t3 ^^ 2
|
||||
r10 = T.x * r9 // 10: t4 <- t4 * t7
|
||||
r11 = S.z * r9 // 11: t7 <- t3 * t7
|
||||
r12 = T.y * r11 // 12: t5 <- t5 * t7
|
||||
r13 = t1 - r10 // 13: t4 <- t1 - t4
|
||||
r14 = t2 - r12 // 14: t5 <- t2 - t5
|
||||
|
||||
r22 = 2 * t1 - r13 // 22: t1 <- 2 * t1 - t4
|
||||
r23 = 2 * t2 - r14 // 23: t2 <- 2 * t2 - t5
|
||||
|
||||
r25 = S.z * T.z // 25: t3 <- t3 * t6
|
||||
|
||||
r27 = t3 * r13 // 27: t3 <- t3 * t4
|
||||
r28 = r13 ^^ 2 // 28: t7 <- t4 ^^ 2
|
||||
r29 = r13 * r28 // 29: t4 <- t4 * t7
|
||||
r30 = r22 * r28 // 30: t7 <- t1 * t7
|
||||
r31 = r14 ^^ 2 // 31: t1 <- t5 ^^ 2
|
||||
r32 = r31 - r30 // 32: t1 <- t1 - t7
|
||||
r33 = r30 - 2 * r32 // 33: t7 <- t7 - 2 * t1
|
||||
r34 = r14 * r33 // 34: t5 <- t5 * t7
|
||||
r35 = r23 * r29 // 35: t4 <- t2 * t4
|
||||
r36 = r34 - r35 // 36: t2 <- t5 - t4
|
||||
r37 = r36 /. 2 // 37: t2 <- t2 / 2
|
||||
|
||||
/**
|
||||
* Routine 2.2.8: Set `R` to `S + T` [NSA19 Section 2.2].
|
||||
*/
|
||||
ec_full_add : ProjectivePoint -> ProjectivePoint -> ProjectivePoint
|
||||
ec_full_add S T =
|
||||
if S.z == 0 then T // 1-4: if Sz == 0 then R <- T, return
|
||||
| T.z == 0 then S // 5-8: if Tz == 0 then R <- S, return
|
||||
// 10-11: if R == (0, 0, 0) then ec_double (R, s)
|
||||
| R == {x = 0, y = 0, z = 0} then ec_double S
|
||||
else R
|
||||
where
|
||||
R = ec_add S T // 9: ec_add (R, S, T)
|
||||
|
||||
/**
|
||||
* Routine 2.2.9: Set `R` to `S - T` [NSA19 Section 2.2].
|
||||
*/
|
||||
ec_full_sub : ProjectivePoint -> ProjectivePoint -> ProjectivePoint
|
||||
ec_full_sub S T = R
|
||||
where
|
||||
U = {x = T.x, y = -T.y, z = T.z}
|
||||
R = ec_full_add S U
|
||||
|
||||
/**
|
||||
* Routine 2.2.10: Set `R` to `d * S` [NSA19 Section 2.2].
|
||||
*
|
||||
* ```
|
||||
* :s prover=cvc5
|
||||
* :safe ec_mult
|
||||
* ```
|
||||
*/
|
||||
ec_mult : Z p -> ProjectivePoint -> ProjectivePoint
|
||||
ec_mult d S =
|
||||
if d == 0 then { x = 1, y = 1, z = 0 }
|
||||
| d == 1 then S
|
||||
| S.z == 0 then { x = 1, y = 1, z = 0 }
|
||||
else Rs!1
|
||||
where
|
||||
S' = if S.z != 1 then ec_projectify (unwrap (ec_affinify S))
|
||||
else S // `unwrap` is safe here because `Err` is guarded by
|
||||
// the `S.z == 0` case above.
|
||||
h = 3 * k
|
||||
k = ZtoBV d : [n + 2]
|
||||
Rs = [ { x = 1, y = 1, z = 0 } ] // Start with 1 instead of `S` to avoid
|
||||
// needing to find the high-bit.
|
||||
# [ if hi && ~ki then ec_full_add RiDouble S'
|
||||
| ~hi && ki then ec_full_sub RiDouble S'
|
||||
else RiDouble
|
||||
where RiDouble = ec_double Ri
|
||||
| ki <- k | hi <- h | Ri <- Rs ]
|
||||
|
||||
/**
|
||||
* Routine 2.2.11: An auxiliary function for `ec_twin_mult` [NSA19
|
||||
* Section 2.2].
|
||||
*/
|
||||
F : [5] -> [5]
|
||||
F t = if 18 <= t /\ t < 22 then 9
|
||||
| 14 <= t /\ t < 18 then 10
|
||||
| 22 <= t /\ t < 24 then 11
|
||||
| 4 <= t /\ t < 12 then 14
|
||||
else 12
|
||||
|
||||
/**
|
||||
* Routine 2.2.12: Set `R` to `d0 * S + d1 * T` where `0 <= d0, d1 <
|
||||
* p` [NSA19 Section 2.2].
|
||||
*/
|
||||
ec_twin_mult : Z p -> ProjectivePoint -> Z p -> ProjectivePoint -> ProjectivePoint
|
||||
ec_twin_mult d0 S d1 T = (last states).0
|
||||
where
|
||||
SpT = ec_full_add S T
|
||||
SmT = ec_full_sub S T
|
||||
e0 = ZtoBV d0 : [max 4 n]
|
||||
e1 = ZtoBV d1 : [max 4 n]
|
||||
c = [ [ False, False ] # take e0
|
||||
, [ False, False ] # take e1
|
||||
] : [2][6]
|
||||
states = [ ( O, c ) ] #
|
||||
[ (Rk', c')
|
||||
where
|
||||
h0 = if c0@0 then 31 - tail c0 else tail c0
|
||||
h1 = if c1@0 then 31 - tail c1 else tail c1
|
||||
u0 = if h0 < F h1 then 0 else if c0@0 then -1 else 1
|
||||
u1 = if h1 < F h0 then 0 else if c1@0 then -1 else 1
|
||||
c' = [ [ (u0 != 0) ^ c0@1 ] # (drop`{2} c0) # [e0k]
|
||||
, [ (u1 != 0) ^ c1@1 ] # (drop`{2} c1) # [e1k]
|
||||
]
|
||||
Rk' = if (u0 == -1) && (u1 == -1) then ec_full_sub RkDouble SpT
|
||||
| (u0 == -1) && (u1 == 0) then ec_full_sub RkDouble S
|
||||
| (u0 == -1) && (u1 == 1) then ec_full_sub RkDouble SmT
|
||||
| (u0 == 0) && (u1 == -1) then ec_full_sub RkDouble T
|
||||
| (u0 == 0) && (u1 == 1) then ec_full_add RkDouble T
|
||||
| (u0 == 1) && (u1 == -1) then ec_full_add RkDouble SmT
|
||||
| (u0 == 1) && (u1 == 0) then ec_full_add RkDouble S
|
||||
| (u0 == 1) && (u1 == 1) then ec_full_add RkDouble SpT
|
||||
else RkDouble
|
||||
RkDouble = ec_double Rk
|
||||
| (Rk, [c0, c1]) <- states
|
||||
| e0k <- drop`{4} e0 # (0 : [5])
|
||||
| e1k <- drop`{4} e1 # (0 : [5])
|
||||
]
|
||||
@@ -0,0 +1,28 @@
|
||||
/*
|
||||
* Description: This is an instantiation of ECDSA for the NIST
|
||||
* elliptic curve P-192 [NSA19, NISTSP800-186].
|
||||
*/
|
||||
|
||||
module algorithms::ECDSA::p192 = algorithms::ECDSA::ECDSA where
|
||||
|
||||
type p = 6277101735386680763835789423207666416083908700390324961279
|
||||
|
||||
type n = 6277101735386680763835789423176059013767194773182842284081
|
||||
|
||||
b = 2455155546008943817740293915197451784769108058161191238065
|
||||
|
||||
G = {x = 602046282375688656758213480587526111916698976636884684818,
|
||||
y = 174050332293622031404857552280219410364023488927386650641,
|
||||
z = 1}
|
||||
|
||||
mp_mod_sqrt : Z p -> Z p
|
||||
mp_mod_sqrt c = r''
|
||||
where
|
||||
t1 = c ^^ 2 ; t1' = t1 * c
|
||||
t2 = t1' ^^ (2^^2) ; t2' = t2 * t1'
|
||||
t3 = t2' ^^ (2^^4) ; t3' = t3 * t2'
|
||||
t4 = t3' ^^ (2^^8) ; t4' = t4 * t3'
|
||||
t5 = t4' ^^ (2^^16) ; t5' = t5 * t4'
|
||||
t6 = t5' ^^ (2^^32) ; t6' = t6 * t5'
|
||||
r = t6' ^^ (2^^64) ; r' = r * t6'
|
||||
r'' = r' ^^ (2^^62)
|
||||
@@ -0,0 +1,72 @@
|
||||
/*
|
||||
* Description: This is an instantiation of ECDSA for the NIST
|
||||
* elliptic curve P-224 [NSA19, NISTSP800-186].
|
||||
*/
|
||||
|
||||
module algorithms::ECDSA::p224 = algorithms::ECDSA::ECDSA where
|
||||
|
||||
import shared::common::utils::TypeCoercion (ZtoBV)
|
||||
|
||||
type p = 26959946667150639794667015087019630673557916260026308143510066298881
|
||||
|
||||
type n = 26959946667150639794667015087019625940457807714424391721682722368061
|
||||
|
||||
b = 18958286285566608000408668544493926415504680968679321075787234672564
|
||||
|
||||
G = {x = 19277929113566293071110308034699488026831934219452440156649784352033,
|
||||
y = 19926808758034470970197974370888749184205991990603949537637343198772,
|
||||
z = 1}
|
||||
|
||||
mp_mod_sqrt : Z p -> Z p
|
||||
mp_mod_sqrt c = r
|
||||
where
|
||||
s = random (ZtoBV c)
|
||||
(d0, e0, f0) = RP c s
|
||||
(d1, e1, f1) = RS (d0, e0, f0)
|
||||
state = [(d1, e1, f1)] #
|
||||
[ if d1' == 0 then (d, e, f) else (d1', e1', f1')
|
||||
where (d1', e1', f1') = RS (d, e, f)
|
||||
| (d, e, f) <- state ]
|
||||
(d0', e0', _) = state@95
|
||||
r = d0' /. e0'
|
||||
|
||||
RS : (Z p, Z p, Z p) -> (Z p, Z p, Z p)
|
||||
RS (d0, e0, f0) = (d1, e1', f1'')
|
||||
where
|
||||
t = d0 ^^ 2
|
||||
e1 = d0 * e0
|
||||
d1 = t + f0
|
||||
e1' = e1 + e1
|
||||
f1 = t * f0
|
||||
f1' = f1 + f1
|
||||
f1'' = f1' + f1'
|
||||
|
||||
RSS : (Z p, Z p, Z p) -> [7] -> (Z p, Z p, Z p)
|
||||
RSS (d0, e0, f0) j = (d1, e1, f1)
|
||||
where
|
||||
(d1, e1, f1) = (iterate RS (d0, e0, f0))@j
|
||||
|
||||
RM : Z p -> Z p -> Z p -> Z p -> Z p -> (Z p, Z p, Z p)
|
||||
RM c d0 e0 d1 e1 = (d2, e2', f2'')
|
||||
where
|
||||
t1 = e0 * e1
|
||||
t1' = t1 * c
|
||||
t1'' = -t1'
|
||||
t2 = d0 * d1
|
||||
t2' = t2 + t1''
|
||||
t1''' = d0 * e1
|
||||
e2 = d1 * e0
|
||||
e2' = e2 + t1'''
|
||||
f2 = e2' ^^ 2
|
||||
f2' = f2 * c
|
||||
f2'' = -f2'
|
||||
d2 = t2'
|
||||
|
||||
RP : Z p -> Z p -> (Z p, Z p, Z p)
|
||||
RP c r = (d1, e1, f1)
|
||||
where
|
||||
(d1, e1, f1) = foldl body (r, 1, -c) [0..6]
|
||||
body (d0, e0, f0) i = (d1'', e1'', f1'')
|
||||
where
|
||||
(d1', e1', _) = RSS (d0, e0, f0) (2^^i)
|
||||
(d1'', e1'', f1'') = RM c d1' e1' d0 e0
|
||||
@@ -0,0 +1,27 @@
|
||||
/*
|
||||
* Description: This is an instantiation of ECDSA for the NIST
|
||||
* elliptic curve P-256 [NSA19, NISTSP800-186].
|
||||
*/
|
||||
|
||||
module algorithms::ECDSA::p256 = algorithms::ECDSA::ECDSA where
|
||||
|
||||
type p = 115792089210356248762697446949407573530086143415290314195533631308867097853951
|
||||
|
||||
type n = 115792089210356248762697446949407573529996955224135760342422259061068512044369
|
||||
|
||||
b = 41058363725152142129326129780047268409114441015993725554835256314039467401291
|
||||
|
||||
G = {x = 48439561293906451759052585252797914202762949526041747995844080717082404635286,
|
||||
y = 36134250956749795798585127919587881956611106672985015071877198253568414405109,
|
||||
z = 1}
|
||||
|
||||
mp_mod_sqrt : Z p -> Z p
|
||||
mp_mod_sqrt c = r'' ^^ (2 ^^ 94)
|
||||
where
|
||||
t1 = (c ^^ 2) * c
|
||||
t2 = (t1 ^^ (2 ^^ 2)) * t1
|
||||
t3 = (t2 ^^ (2 ^^ 4)) * t2
|
||||
t4 = (t3 ^^ (2 ^^ 8)) * t3
|
||||
r = (t4 ^^ (2 ^^ 16)) * t4
|
||||
r' = (r ^^ (2 ^^ 32)) * c
|
||||
r'' = (r' ^^ (2 ^^ 96)) * c
|
||||
@@ -0,0 +1,35 @@
|
||||
/*
|
||||
* Description: This is an instantiation of ECDSA for the NIST
|
||||
* elliptic curve P-384 [NSA19, NISTSP800-186].
|
||||
*/
|
||||
|
||||
module algorithms::ECDSA::p384 = algorithms::ECDSA::ECDSA where
|
||||
|
||||
type p = 39402006196394479212279040100143613805079739270465446667948293404245721771496870329047266088258938001861606973112319
|
||||
|
||||
type n = 39402006196394479212279040100143613805079739270465446667946905279627659399113263569398956308152294913554433653942643
|
||||
|
||||
b = 27580193559959705877849011840389048093056905856361568521428707301988689241309860865136260764883745107765439761230575
|
||||
|
||||
G = {x = 26247035095799689268623156744566981891852923491109213387815615900925518854738050089022388053975719786650872476732087,
|
||||
y = 8325710961489029985546751289520108179287853048861315594709205902480503199884419224438643760392947333078086511627871,
|
||||
z = 1}
|
||||
|
||||
mp_mod_sqrt : Z p -> Z p
|
||||
mp_mod_sqrt c = r''' ^^ (2 ^^ 30)
|
||||
where
|
||||
t1 = (c ^^ 2) * c
|
||||
t2 = (t1 ^^ (2 ^^ 2)) * t1
|
||||
t2' = (t2 ^^ 2) * c
|
||||
t3 = (t2' ^^ (2 ^^ 5)) * t2'
|
||||
t4 = (t3 ^^ (2 ^^ 5)) * t2'
|
||||
t2'' = (t4 ^^ (2 ^^ 15)) * t4
|
||||
t3' = t2'' ^^ (2 ^^ 2)
|
||||
t1' = t3' * t1
|
||||
t3'' = t3' ^^ (2 ^^ 28)
|
||||
t2''' = t2'' * t3''
|
||||
t3''' = (t2''' ^^ (2 ^^ 60)) * t2'''
|
||||
r = (t3''' ^^ (2 ^^ 120)) * t3'''
|
||||
r' = (r ^^ (2 ^^ 15)) * t4
|
||||
r'' = (r' ^^ (2 ^^ 33)) * t1'
|
||||
r''' = (r'' ^^ (2 ^^ 64)) * c
|
||||
@@ -0,0 +1,21 @@
|
||||
/*
|
||||
* Description: This is an instantiation of ECDSA for the NIST
|
||||
* elliptic curve P-521 [NSA19, NISTSP800-186].
|
||||
*/
|
||||
|
||||
module algorithms::ECDSA::p521 = algorithms::ECDSA::ECDSA where
|
||||
|
||||
type p = 6864797660130609714981900799081393217269435300143305409394463459185543183397656052122559640661454554977296311391480858037121987999716643812574028291115057151
|
||||
|
||||
type n = 6864797660130609714981900799081393217269435300143305409394463459185543183397655394245057746333217197532963996371363321113864768612440380340372808892707005449
|
||||
|
||||
b = 1093849038073734274511112390766805569936207598951683748994586394495953116150735016013708737573759623248592132296706313309438452531591012912142327488478985984
|
||||
|
||||
G = {x = 2661740802050217063228768716723360960729859168756973147706671368418802944996427808491545080627771902352094241225065558662157113545570916814161637315895999846,
|
||||
y = 3757180025770020463545507224491183603594455134769762486694567779615544477440556316691234405012945539562144444537289428522585666729196580810124344277578376784,
|
||||
z = 1}
|
||||
|
||||
mp_mod_sqrt : Z p -> Z p
|
||||
mp_mod_sqrt c = rs@519
|
||||
where
|
||||
rs = [c] # [ ri ^^ 2 | ri <- rs ]
|
||||
@@ -0,0 +1,37 @@
|
||||
/*
|
||||
* Description: This module contains a single test from:
|
||||
* `https://csrc.nist.gov/Projects/cryptographic-algorithm-validation-program/digital-signatures`
|
||||
*/
|
||||
|
||||
module algorithms::ECDSA::tests::p192 where
|
||||
|
||||
import shared::common::utils::TypeCoercion (BVtoZ)
|
||||
import shared::common::utils::Enum (unwrap)
|
||||
import algorithms::ECDSA::p192
|
||||
import algorithms::SHA1::Main as SHA1
|
||||
|
||||
/** Message to sign */
|
||||
M = 0x66e98a165854cd07989b1ee0ec3f8dbe0ee3c2fb0051ef53a0be03457c4f21bce7dc50ef4df37486c3207dfee26bde4ed62340cbb2da784906b1b783b4d601bdff4ae1a7e5e85a85afa3208dc60f0990c823bedddb3db663426665152ed7b093d6bda506c93a694b83ac71553f31f5cc0d6ba2fa248090e8796573c4915d1586
|
||||
|
||||
/** Private key */
|
||||
d = BVtoZ 0x0017899949d02b55f9556846411cc9de512c6f16ecdeb1c4
|
||||
|
||||
/** Random value */
|
||||
k = BVtoZ 0x0098e9c07e8e6adb97b77d85b0c10a265e11737a89a3e37b
|
||||
|
||||
/** `r` component of the signature */
|
||||
r = BVtoZ 0xaf1f749e3df6220ff04efd178618a977e0838b1b9dc126e3
|
||||
|
||||
/** `s` component of the signature */
|
||||
s = BVtoZ 0x8990a04c6cc0ff26264ecf8f7831381a9dbc6e53cc8cc860
|
||||
|
||||
/** Public key */
|
||||
Q = { x = BVtoZ 0x14f69738599689f5706ab71343becc886ef1569a2d1137fe
|
||||
, y = BVtoZ 0x0cf5a433909e33217fb4df6b9593f71d43fb1c2a5653b763
|
||||
}
|
||||
|
||||
/** A test of p192 */
|
||||
property p192Test =
|
||||
unwrap(sign M d SHA1::hash k) == (r, s)
|
||||
/\ verify M (r, s) (private_to_public d) SHA1::hash
|
||||
/\ Q == unwrap (ec_affinify (private_to_public d))
|
||||
@@ -0,0 +1,37 @@
|
||||
/*
|
||||
* Description: This module contains a single test from:
|
||||
* `https://csrc.nist.gov/Projects/cryptographic-algorithm-validation-program/digital-signatures`
|
||||
*/
|
||||
|
||||
module algorithms::ECDSA::tests::p224 where
|
||||
|
||||
import shared::common::utils::TypeCoercion (BVtoZ)
|
||||
import shared::common::utils::Enum (unwrap)
|
||||
import algorithms::ECDSA::p224
|
||||
import algorithms::SHA2::SHA384 as SHA384
|
||||
|
||||
/** Message to sign */
|
||||
M = 0x25e4416695f77551fdce276355528ccf1ddc2483821c5d22d751d50111ca2fadc6593b52c74f4b5957494f1df25b0b2f86950d0d19229ec6506fee8581d2dd09d48418b146ff16bd84a17ca0dc83b1888eb407376da6c8a88fa1e60b8c2a2471dfde4b3996ef673d5bde3d70c434dc9f2488e9de16ae657d29e5e59ec922a1ec
|
||||
|
||||
/** Private key */
|
||||
d = BVtoZ 0x62c572ee0d6f81b27e591d788bfc2f42b5105d2663078dfb58069ebd
|
||||
|
||||
/** Random value */
|
||||
k = BVtoZ 0x0f0bb1e428bcdebf4dc62a5278068efc0f8ce75f89e89b3630f102b2
|
||||
|
||||
/** `r` component of the signature */
|
||||
r = BVtoZ 0xaac0ea27e129f544abcc77f110e70bbdd5aa3e425dc39d5e8887025d
|
||||
|
||||
/** `s` component of the signature */
|
||||
s = BVtoZ 0x10e5dd06aee6b8419a04aa33d9d5678b0039c3acc3c4b61fe106bfdc
|
||||
|
||||
/** Public key */
|
||||
Q = { x = BVtoZ 0xbd6ba605639b98fa8113a16a3bb004ddfaec901c98a931206165f4a5
|
||||
, y = BVtoZ 0xa3190b10ef39e88abd60b2293b4707512b45c6c5ed5794cc11454427
|
||||
}
|
||||
|
||||
/** A test of p224 */
|
||||
property p224Test =
|
||||
unwrap(sign M d SHA384::hash k) == (r, s)
|
||||
/\ verify M (r, s) (private_to_public d) SHA384::hash
|
||||
/\ Q == unwrap (ec_affinify (private_to_public d))
|
||||
@@ -0,0 +1,37 @@
|
||||
/*
|
||||
* Description: This module contains a single test from:
|
||||
* `https://csrc.nist.gov/Projects/cryptographic-algorithm-validation-program/digital-signatures`
|
||||
*/
|
||||
|
||||
module algorithms::ECDSA::tests::p256 where
|
||||
|
||||
import shared::common::utils::TypeCoercion (BVtoZ)
|
||||
import shared::common::utils::Enum (unwrap)
|
||||
import algorithms::ECDSA::p256
|
||||
import algorithms::SHA2::SHA384 as SHA384
|
||||
|
||||
/** Message to sign */
|
||||
M = 0xe0b8596b375f3306bbc6e77a0b42f7469d7e83635990e74aa6d713594a3a24498feff5006790742d9c2e9b47d714bee932435db747c6e733e3d8de41f2f91311f2e9fd8e025651631ffd84f66732d3473fbd1627e63dc7194048ebec93c95c159b5039ab5e79e42c80b484a943f125de3da1e04e5bf9c16671ad55a1117d3306
|
||||
|
||||
/** Private key */
|
||||
d = BVtoZ 0xb6faf2c8922235c589c27368a3b3e6e2f42eb6073bf9507f19eed0746c79dced
|
||||
|
||||
/** Random value */
|
||||
k = BVtoZ 0x9980b9cdfcef3ab8e219b9827ed6afdd4dbf20bd927e9cd01f15762703487007
|
||||
|
||||
/** `r` component of the signature */
|
||||
r = BVtoZ 0xf5087878e212b703578f5c66f434883f3ef414dc23e2e8d8ab6a8d159ed5ad83
|
||||
|
||||
/** `s` component of the signature */
|
||||
s = BVtoZ 0x306b4c6c20213707982dffbb30fba99b96e792163dd59dbe606e734328dd7c8a
|
||||
|
||||
/** Public key */
|
||||
Q = { x = BVtoZ 0xe0e7b99bc62d8dd67883e39ed9fa0657789c5ff556cc1fd8dd1e2a55e9e3f243
|
||||
, y = BVtoZ 0x63fbfd0232b95578075c903a4dbf85ad58f8350516e1ec89b0ee1f5e1362da69
|
||||
}
|
||||
|
||||
/** A test of p256 */
|
||||
property p256Test =
|
||||
unwrap(sign M d SHA384::hash k) == (r, s)
|
||||
/\ verify M (r, s) (private_to_public d) SHA384::hash
|
||||
/\ Q == unwrap (ec_affinify (private_to_public d))
|
||||
@@ -0,0 +1,37 @@
|
||||
/*
|
||||
* Description: This module contains a single test from:
|
||||
* `https://csrc.nist.gov/Projects/cryptographic-algorithm-validation-program/digital-signatures`
|
||||
*/
|
||||
|
||||
module algorithms::ECDSA::tests::p384 where
|
||||
|
||||
import shared::common::utils::TypeCoercion (BVtoZ)
|
||||
import shared::common::utils::Enum (unwrap)
|
||||
import algorithms::ECDSA::p384
|
||||
import algorithms::SHA2::SHA384 as SHA384
|
||||
|
||||
/** Message to sign */
|
||||
M = 0x6b45d88037392e1371d9fd1cd174e9c1838d11c3d6133dc17e65fa0c485dcca9f52d41b60161246039e42ec784d49400bffdb51459f5de654091301a09378f93464d52118b48d44b30d781eb1dbed09da11fb4c818dbd442d161aba4b9edc79f05e4b7e401651395b53bd8b5bd3f2aaa6a00877fa9b45cadb8e648550b4c6cbe
|
||||
|
||||
/** Private key */
|
||||
d = BVtoZ 0x201b432d8df14324182d6261db3e4b3f46a8284482d52e370da41e6cbdf45ec2952f5db7ccbce3bc29449f4fb080ac97
|
||||
|
||||
/** Random value */
|
||||
k = BVtoZ 0xdcedabf85978e090f733c6e16646fa34df9ded6e5ce28c6676a00f58a25283db8885e16ce5bf97f917c81e1f25c9c771
|
||||
|
||||
/** `r` component of the signature */
|
||||
r = BVtoZ 0x50835a9251bad008106177ef004b091a1e4235cd0da84fff54542b0ed755c1d6f251609d14ecf18f9e1ddfe69b946e32
|
||||
|
||||
/** `s` component of the signature */
|
||||
s = BVtoZ 0x0475f3d30c6463b646e8d3bf2455830314611cbde404be518b14464fdb195fdcc92eb222e61f426a4a592c00a6a89721
|
||||
|
||||
/** Public key */
|
||||
Q = { x = BVtoZ 0xc2b47944fb5de342d03285880177ca5f7d0f2fcad7678cce4229d6e1932fcac11bfc3c3e97d942a3c56bf34123013dbf
|
||||
, y = BVtoZ 0x37257906a8223866eda0743c519616a76a758ae58aee81c5fd35fbf3a855b7754a36d4a0672df95d6c44a81cf7620c2d
|
||||
}
|
||||
|
||||
/** A test of p384 */
|
||||
property p384Test =
|
||||
unwrap(sign M d SHA384::hash k) == (r, s)
|
||||
/\ verify M (r, s) (private_to_public d) SHA384::hash
|
||||
/\ Q == unwrap (ec_affinify (private_to_public d))
|
||||
@@ -0,0 +1,37 @@
|
||||
/*
|
||||
* Description: This module contains a single test from:
|
||||
* `https://csrc.nist.gov/Projects/cryptographic-algorithm-validation-program/digital-signatures`
|
||||
*/
|
||||
|
||||
module algorithms::ECDSA::tests::p521 where
|
||||
|
||||
import shared::common::utils::TypeCoercion (BVtoZ)
|
||||
import shared::common::utils::Enum (unwrap)
|
||||
import algorithms::ECDSA::p521
|
||||
import algorithms::SHA2::SHA384 as SHA384
|
||||
|
||||
/** Message to sign */
|
||||
M = 0xdbc094402c5b559d53168c6f0c550d827499c6fb2186ae2db15b89b4e6f46220386d6f01bebde91b6ceb3ec7b4696e2cbfd14894dd0b7d656d23396ce920044f9ca514bf115cf98ecaa55b950a9e49365c2f3a05be5020e93db92c37437513044973e792af814d0ffad2c8ecc89ae4b35ccb19318f0b988a7d33ec5a4fe85dfe
|
||||
|
||||
/** Private key */
|
||||
d = BVtoZ (`0x095976d387d814e68aeb09abecdbf4228db7232cd3229569ade537f33e07ed0da0abdee84ab057c9a00049f45250e2719d1ecaccf91c0e6fcdd4016b75bdd98a950 : [521])
|
||||
|
||||
/** Random value */
|
||||
k = BVtoZ (`0x0a8d90686bd1104627836afe698effe22c51aa3b651737a940f2b0f9cd72c594575e550adb142e467a3f631f4429514df8296d8f5144df86faa9e3a8f13939ad5b3 : [521])
|
||||
|
||||
/** `r` component of the signature */
|
||||
r = BVtoZ (`0x02128f77df66d16a604ffcd1a515e039d49bf6b91a215b814b2a1c88d32039521fbd142f717817b838450229025670d99c1fd5ab18bd965f093cae7accff0675aae : [521])
|
||||
|
||||
/** `s` component of the signature */
|
||||
s = BVtoZ (`0x008dc65a243700a84619dce14e44ea8557e36631db1a55de15865497dbfd66e76a7471f78e510c04e613ced332aa563432a1017da8b81c146059ccc7930153103a6 : [521])
|
||||
|
||||
/** Public key */
|
||||
Q = { x = BVtoZ (`0x13b4ab7bc1ddf7fd74ca6f75ac560c94169f435361e74eba1f8e759ac70ab3af138d8807aca3d8e73b5c2eb787f6dcca2718122bd94f08943a686b115d869d3f406 : [521])
|
||||
, y = BVtoZ (`0x0f293c1d627b44e7954d0546270665888144a94d437679d074787959d0d944d8223b9d4b5d068b4fbbd1176a004b476810475cd2a200b83eccd226d08b444a71e71 : [521])
|
||||
}
|
||||
|
||||
/** A test of p521 */
|
||||
property p521Test =
|
||||
unwrap(sign M d SHA384::hash k) == (r, s)
|
||||
/\ verify M (r, s) (private_to_public d) SHA384::hash
|
||||
/\ Q == unwrap (ec_affinify (private_to_public d))
|
||||
@@ -0,0 +1,12 @@
|
||||
# Bibliography
|
||||
|
||||
[FIPS-PUB-198-1] The Keyed-Hash Message Authentication Code (HMAC).
|
||||
Federal Information Processing Standards Publication 198-1.
|
||||
July 2008.
|
||||
https://doi.org/10.6028/NIST.FIPS.198-1
|
||||
|
||||
[NIST SP 800-107r1] Recommendation for Applications Using Approved
|
||||
Hash Algorithms (Withdrawn). Quynh Dang. August 2021.
|
||||
https://doi.org/10.6028/NIST.SP.800-107r1
|
||||
|
||||
[NIST HMAC Examples] https://csrc.nist.gov/projects/cryptographic-standards-and-guidelines/example-values#aHashing
|
||||
@@ -0,0 +1,65 @@
|
||||
/*
|
||||
* Description: This is a Cryptol specification for a keyed-Hash
|
||||
* Message Authentication Code (HMAC), a mechanism for message
|
||||
* authentication using an Approved Cryptographic Hash Function (ACHF)
|
||||
* [FIPS-PUB-198-1 Section 2.3].
|
||||
*/
|
||||
|
||||
module algorithms::HMAC::Main where
|
||||
|
||||
/*
|
||||
* `HMAC` and `HMAC_init` use the following types [FIPS-PUB-198-1
|
||||
* Section 2.3]:
|
||||
* `λ` : The number of (leftmost) bits of the output used
|
||||
* [FIPS-PUB-198-1 Section 5].
|
||||
* `B` : Block size (in bytes) of the input of the ACHF.
|
||||
* `k` : Length of `K` in bytes.
|
||||
* `n` : Length of `text` in bits, where `0 <= n < 2^^B - 8*B`.
|
||||
* `L` : Block size (in bytes) of the output of the ACHF.
|
||||
*/
|
||||
|
||||
/**
|
||||
* This defines the HMAC message authentication function using the
|
||||
* ACHF `Hk`, `Hn`, and `HL`. Each ACHF is technically the same but
|
||||
* defined with a different input size.
|
||||
*/
|
||||
HMAC :
|
||||
{ λ, B, k, n, L}
|
||||
( λ <= L * 8
|
||||
, fin B, 2 ^^ B >= 8 * B
|
||||
, fin k
|
||||
, fin n, n < 2 ^^ B - 8 * B
|
||||
, L <= B
|
||||
)
|
||||
=> ([k * 8] -> [L * 8])
|
||||
-> ([B * 8 + n] -> [L * 8])
|
||||
-> ([(B + L) * 8] -> [L * 8])
|
||||
-> [k][8]
|
||||
-> [n]
|
||||
-> [λ]
|
||||
HMAC Hk Hn HL K text =
|
||||
take (HL ((K0 ^ opad) # (Hn ((K0 ^ ipad) # text))))
|
||||
where
|
||||
K0 : [B * 8] // `K` after preprocessing to form
|
||||
// a `B`-byte key.
|
||||
K0 = HMAC_init Hk K
|
||||
opad = join (repeat`{B} 0x5C) // [FIPS-PUB-198-1 Section 2.3]
|
||||
ipad = join (repeat`{B} 0x36) // [FIPS-PUB-198-1 Section 2.3]
|
||||
|
||||
private
|
||||
|
||||
/**
|
||||
* This function initializes the HMAC key `K` by performing step 1-3
|
||||
* of [FIPS-PUB-198-1 Section 4 Table 1]. Step 2 implicitly requires
|
||||
* `L <= B`.
|
||||
*/
|
||||
HMAC_init :
|
||||
{ B, k, L }
|
||||
( fin B, fin k, L <= B )
|
||||
=> ([k * 8] -> [L * 8])
|
||||
-> [k][8]
|
||||
-> [B * 8]
|
||||
HMAC_init Hk K
|
||||
| k == B => join K
|
||||
| k > B => Hk (join K) # (zero : [(B - L) * 8])
|
||||
| k < B => join K # (zero : [(B - k) * 8])
|
||||
@@ -0,0 +1,62 @@
|
||||
/*
|
||||
* Description: The following properties check test vectors for
|
||||
* HMAC-SHA3-224 provided by [NIST HMAC Examples].
|
||||
*/
|
||||
|
||||
module algorithms::HMAC::tests::SHA3_224 where
|
||||
|
||||
import algorithms::SHA3::SHA3_224 (HMAC)
|
||||
|
||||
property Sample1 = HMAC key msg == mac
|
||||
where
|
||||
key = split (join [ 0x00010203, 0x04050607, 0x08090a0b, 0x0c0d0e0f
|
||||
, 0x10111213, 0x14151617, 0x18191a1b
|
||||
])
|
||||
msg = join "Sample message for keylen<blocklen"
|
||||
mac = join [ 0x332cfd59, 0x347fdb8e, 0x576e7726, 0x0be4aba2
|
||||
, 0xd6dc5311, 0x7b3bfb52, 0xc6d18c04
|
||||
]
|
||||
|
||||
property Sample2 = HMAC key msg == mac
|
||||
where
|
||||
key = split (join [ 0x00010203, 0x04050607, 0x08090a0b, 0x0c0d0e0f
|
||||
, 0x10111213, 0x14151617, 0x18191a1b, 0x1c1d1e1f
|
||||
, 0x20212223, 0x24252627, 0x28292a2b, 0x2c2d2e2f
|
||||
, 0x30313233, 0x34353637, 0x38393a3b, 0x3c3d3e3f
|
||||
, 0x40414243, 0x44454647, 0x48494a4b, 0x4c4d4e4f
|
||||
, 0x50515253, 0x54555657, 0x58595a5b, 0x5c5d5e5f
|
||||
, 0x60616263, 0x64656667, 0x68696a6b, 0x6c6d6e6f
|
||||
, 0x70717273, 0x74757677, 0x78797a7b, 0x7c7d7e7f
|
||||
, 0x80818283, 0x84858687, 0x88898a8b, 0x8c8d8e8f
|
||||
])
|
||||
msg = join "Sample message for keylen=blocklen"
|
||||
mac = join [ 0xd8b733bc, 0xf66c644a, 0x12323d56, 0x4e24dcf3
|
||||
, 0xfc75f231, 0xf3b67968, 0x359100c7
|
||||
]
|
||||
|
||||
property Sample3 = HMAC key msg == mac
|
||||
where
|
||||
key = split (join [ 0x00010203, 0x04050607, 0x08090a0b, 0x0c0d0e0f
|
||||
, 0x10111213, 0x14151617, 0x18191a1b, 0x1c1d1e1f
|
||||
, 0x20212223, 0x24252627, 0x28292a2b, 0x2c2d2e2f
|
||||
, 0x30313233, 0x34353637, 0x38393a3b, 0x3c3d3e3f
|
||||
, 0x40414243, 0x44454647, 0x48494a4b, 0x4c4d4e4f
|
||||
, 0x50515253, 0x54555657, 0x58595a5b, 0x5c5d5e5f
|
||||
, 0x60616263, 0x64656667, 0x68696a6b, 0x6c6d6e6f
|
||||
, 0x70717273, 0x74757677, 0x78797a7b, 0x7c7d7e7f
|
||||
, 0x80818283, 0x84858687, 0x88898a8b, 0x8c8d8e8f
|
||||
, 0x90919293, 0x94959697, 0x98999a9b, 0x9c9d9e9f
|
||||
, 0xa0a1a2a3, 0xa4a5a6a7, 0xa8a9aaab
|
||||
])
|
||||
msg = join "Sample message for keylen>blocklen"
|
||||
mac = join [ 0x078695ee, 0xcc227c63, 0x6ad31d06, 0x3a15dd05
|
||||
, 0xa7e819a6, 0x6ec6d8de, 0x1e193e59
|
||||
]
|
||||
|
||||
property Sample4 = take (HMAC key msg) == mac
|
||||
where
|
||||
key = split (join [ 0x00010203, 0x04050607, 0x08090a0b, 0x0c0d0e0f
|
||||
, 0x10111213, 0x14151617, 0x18191a1b
|
||||
])
|
||||
msg = join "Sample message for keylen<blocklen, with truncated tag"
|
||||
mac = join [0x8569c54c, 0xbb00a9b7, 0x8ff1b391] # 0xb0e5
|
||||
@@ -0,0 +1,62 @@
|
||||
/*
|
||||
* Description: The following properties check test vectors for
|
||||
* HMAC-SHA3-256 provided by [NIST HMAC Examples].
|
||||
*/
|
||||
module algorithms::HMAC::tests::SHA3_256 where
|
||||
|
||||
import algorithms::SHA3::SHA3_256 (HMAC)
|
||||
|
||||
property Sample1 = HMAC key msg == mac
|
||||
where
|
||||
key = split (join [ 0x00010203, 0x04050607, 0x08090a0b, 0x0c0d0e0f
|
||||
, 0x10111213, 0x14151617, 0x18191a1b, 0x1c1d1e1f
|
||||
])
|
||||
msg = join "Sample message for keylen<blocklen"
|
||||
mac = join [ 0x4fe8e202, 0xc4f058e8, 0xdddc23d8, 0xc34e4673
|
||||
, 0x43e23555, 0xe24fc2f0, 0x25d598f5, 0x58f67205
|
||||
]
|
||||
|
||||
property Sample2 = HMAC key msg == mac
|
||||
where
|
||||
key = split (join [ 0x00010203, 0x04050607, 0x08090a0b, 0x0c0d0e0f
|
||||
, 0x10111213, 0x14151617, 0x18191a1b, 0x1c1d1e1f
|
||||
, 0x20212223, 0x24252627, 0x28292a2b, 0x2c2d2e2f
|
||||
, 0x30313233, 0x34353637, 0x38393a3b, 0x3c3d3e3f
|
||||
, 0x40414243, 0x44454647, 0x48494a4b, 0x4c4d4e4f
|
||||
, 0x50515253, 0x54555657, 0x58595a5b, 0x5c5d5e5f
|
||||
, 0x60616263, 0x64656667, 0x68696a6b, 0x6c6d6e6f
|
||||
, 0x70717273, 0x74757677, 0x78797a7b, 0x7c7d7e7f
|
||||
, 0x80818283, 0x84858687
|
||||
])
|
||||
msg = join "Sample message for keylen=blocklen"
|
||||
mac = join [ 0x68b94e2e, 0x538a9be4, 0x103bebb5, 0xaa016d47
|
||||
, 0x961d4d1a, 0xa9060613, 0x13b557f8, 0xaf2c3faa
|
||||
]
|
||||
|
||||
property Sample3 = HMAC key msg == mac
|
||||
where
|
||||
key = split (join [ 0x00010203, 0x04050607, 0x08090a0b, 0x0c0d0e0f
|
||||
, 0x10111213, 0x14151617, 0x18191a1b, 0x1c1d1e1f
|
||||
, 0x20212223, 0x24252627, 0x28292a2b, 0x2c2d2e2f
|
||||
, 0x30313233, 0x34353637, 0x38393a3b, 0x3c3d3e3f
|
||||
, 0x40414243, 0x44454647, 0x48494a4b, 0x4c4d4e4f
|
||||
, 0x50515253, 0x54555657, 0x58595a5b, 0x5c5d5e5f
|
||||
, 0x60616263, 0x64656667, 0x68696a6b, 0x6c6d6e6f
|
||||
, 0x70717273, 0x74757677, 0x78797a7b, 0x7c7d7e7f
|
||||
, 0x80818283, 0x84858687, 0x88898a8b, 0x8c8d8e8f
|
||||
, 0x90919293, 0x94959697, 0x98999a9b, 0x9c9d9e9f
|
||||
, 0xa0a1a2a3, 0xa4a5a6a7
|
||||
])
|
||||
msg = join "Sample message for keylen>blocklen"
|
||||
mac = join [ 0x9bcf2c23, 0x8e235c3c, 0xe88404e8, 0x13bd2f3a
|
||||
, 0x97185ac6, 0xf238c63d, 0x6229a00b, 0x07974258
|
||||
]
|
||||
|
||||
property Sample4 = take (HMAC key msg) == mac
|
||||
where
|
||||
key = split (join [ 0x00010203, 0x04050607, 0x08090a0b, 0x0c0d0e0f
|
||||
, 0x10111213, 0x14151617, 0x18191a1b, 0x1c1d1e1f
|
||||
])
|
||||
msg = join "Sample message for keylen<blocklen, with truncated tag"
|
||||
mac = join [ 0xc8dc7148, 0xd8c1423a, 0xa549105d, 0xafdf9cad
|
||||
]
|
||||
@@ -0,0 +1,65 @@
|
||||
/*
|
||||
* Description: The following properties check test vectors for
|
||||
* HMAC-SHA3-384 provided by [NIST HMAC Examples].
|
||||
*/
|
||||
module algorithms::HMAC::tests::SHA3_384 where
|
||||
|
||||
import algorithms::SHA3::SHA3_384 (HMAC)
|
||||
|
||||
property Sample1 = HMAC key msg == mac
|
||||
where
|
||||
key = split (join [ 0x00010203, 0x04050607, 0x08090a0b, 0x0c0d0e0f
|
||||
, 0x10111213, 0x14151617, 0x18191a1b, 0x1c1d1e1f
|
||||
, 0x20212223, 0x24252627, 0x28292a2b, 0x2c2d2e2f
|
||||
])
|
||||
msg = join "Sample message for keylen<blocklen"
|
||||
mac = join [ 0xd588a3c5, 0x1f3f2d90, 0x6e8298c1, 0x199aa8ff
|
||||
, 0x62962181, 0x27f6b38a, 0x90b6afe2, 0xc5617725
|
||||
, 0xbc99987f, 0x79b22a55, 0x7b6520db, 0x710b7f42
|
||||
]
|
||||
|
||||
property Sample2 = HMAC key msg == mac
|
||||
where
|
||||
key = split (join [ 0x00010203, 0x04050607, 0x08090a0b, 0x0c0d0e0f
|
||||
, 0x10111213, 0x14151617, 0x18191a1b, 0x1c1d1e1f
|
||||
, 0x20212223, 0x24252627, 0x28292a2b, 0x2c2d2e2f
|
||||
, 0x30313233, 0x34353637, 0x38393a3b, 0x3c3d3e3f
|
||||
, 0x40414243, 0x44454647, 0x48494a4b, 0x4c4d4e4f
|
||||
, 0x50515253, 0x54555657, 0x58595a5b, 0x5c5d5e5f
|
||||
, 0x60616263, 0x64656667
|
||||
])
|
||||
msg = join "Sample message for keylen=blocklen"
|
||||
mac = join [ 0xa27d24b5, 0x92e8c8cb, 0xf6d4ce6f, 0xc5bf62d8
|
||||
, 0xfc98bf2d, 0x486640d9, 0xeb8099e2, 0x4047837f
|
||||
, 0x5f3bffbe, 0x92dcce90, 0xb4ed5b1e, 0x7e44fa90
|
||||
]
|
||||
|
||||
property Sample3 = HMAC key msg == mac
|
||||
where
|
||||
key = split (join [ 0x00010203, 0x04050607, 0x08090a0b, 0x0c0d0e0f
|
||||
, 0x10111213, 0x14151617, 0x18191a1b, 0x1c1d1e1f
|
||||
, 0x20212223, 0x24252627, 0x28292a2b, 0x2c2d2e2f
|
||||
, 0x30313233, 0x34353637, 0x38393a3b, 0x3c3d3e3f
|
||||
, 0x40414243, 0x44454647, 0x48494a4b, 0x4c4d4e4f
|
||||
, 0x50515253, 0x54555657, 0x58595a5b, 0x5c5d5e5f
|
||||
, 0x60616263, 0x64656667, 0x68696a6b, 0x6c6d6e6f
|
||||
, 0x70717273, 0x74757677, 0x78797a7b, 0x7c7d7e7f
|
||||
, 0x80818283, 0x84858687, 0x88898a8b, 0x8c8d8e8f
|
||||
, 0x90919293, 0x94959697
|
||||
])
|
||||
msg = join "Sample message for keylen>blocklen"
|
||||
mac = join [ 0xe5ae4c73, 0x9f455279, 0x368ebf36, 0xd4f5354c
|
||||
, 0x95aa184c, 0x899d3870, 0xe460ebc2, 0x88ef1f94
|
||||
, 0x70053f73, 0xf7c6da2a, 0x71bcaec3, 0x8ce7d6ac
|
||||
]
|
||||
|
||||
property Sample4 = take (HMAC key msg) == mac
|
||||
where
|
||||
key = split (join [ 0x00010203, 0x04050607, 0x08090a0b, 0x0c0d0e0f
|
||||
, 0x10111213, 0x14151617, 0x18191a1b, 0x1c1d1e1f
|
||||
, 0x20212223, 0x24252627, 0x28292a2b, 0x2c2d2e2f
|
||||
])
|
||||
msg = join "Sample message for keylen<blocklen, with truncated tag"
|
||||
mac = join [ 0x25f4bf53, 0x606e91af, 0x79d24a4b, 0xb1fd6aec
|
||||
, 0xd44414a3, 0x0c8ebb0a
|
||||
]
|
||||
@@ -0,0 +1,67 @@
|
||||
/*
|
||||
* Description: The following properties check test vectors for
|
||||
* HMAC-SHA3-512 provided by [NIST HMAC Examples].
|
||||
*/
|
||||
module algorithms::HMAC::tests::SHA3_512 where
|
||||
|
||||
import algorithms::SHA3::SHA3_512 (HMAC)
|
||||
|
||||
property Sample1 = HMAC key msg == mac
|
||||
where
|
||||
key = split (join [ 0x00010203, 0x04050607, 0x08090a0b, 0x0c0d0e0f
|
||||
, 0x10111213, 0x14151617, 0x18191a1b, 0x1c1d1e1f
|
||||
, 0x20212223, 0x24252627, 0x28292a2b, 0x2c2d2e2f
|
||||
, 0x30313233, 0x34353637, 0x38393a3b, 0x3c3d3e3f
|
||||
])
|
||||
msg = join "Sample message for keylen<blocklen"
|
||||
mac = join [ 0x4efd629d, 0x6c71bf86, 0x162658f2, 0x9943b1c3
|
||||
, 0x08ce27cd, 0xfa6db0d9, 0xc3ce8176, 0x3f9cbce5
|
||||
, 0xf7ebe986, 0x8031db1a, 0x8f8eb7b6, 0xb95e5c5e
|
||||
, 0x3f657a89, 0x96c86a2f, 0x6527e307, 0xf0213196
|
||||
]
|
||||
|
||||
property Sample2 = HMAC key msg == mac
|
||||
where
|
||||
key = split (join [ 0x00010203, 0x04050607, 0x08090a0b, 0x0c0d0e0f
|
||||
, 0x10111213, 0x14151617, 0x18191a1b, 0x1c1d1e1f
|
||||
, 0x20212223, 0x24252627, 0x28292a2b, 0x2c2d2e2f
|
||||
, 0x30313233, 0x34353637, 0x38393a3b, 0x3c3d3e3f
|
||||
, 0x40414243, 0x44454647
|
||||
])
|
||||
msg = join "Sample message for keylen=blocklen"
|
||||
mac = join [ 0x544e257e, 0xa2a3e5ea, 0x19a590e6, 0xa24b724c
|
||||
, 0xe6327757, 0x723fe275, 0x1b75bf00, 0x7d80f6b3
|
||||
, 0x60744bf1, 0xb7a88ea5, 0x85f9765b, 0x47911976
|
||||
, 0xd3191cf8, 0x3c039f5f, 0xfab0d29c, 0xc9d9b6da
|
||||
]
|
||||
|
||||
property Sample3 = HMAC key msg == mac
|
||||
where
|
||||
key = split (join [ 0x00010203, 0x04050607, 0x08090a0b, 0x0c0d0e0f
|
||||
, 0x10111213, 0x14151617, 0x18191a1b, 0x1c1d1e1f
|
||||
, 0x20212223, 0x24252627, 0x28292a2b, 0x2c2d2e2f
|
||||
, 0x30313233, 0x34353637, 0x38393a3b, 0x3c3d3e3f
|
||||
, 0x40414243, 0x44454647, 0x48494a4b, 0x4c4d4e4f
|
||||
, 0x50515253, 0x54555657, 0x58595a5b, 0x5c5d5e5f
|
||||
, 0x60616263, 0x64656667, 0x68696a6b, 0x6c6d6e6f
|
||||
, 0x70717273, 0x74757677, 0x78797a7b, 0x7c7d7e7f
|
||||
, 0x80818283, 0x84858687
|
||||
])
|
||||
msg = join "Sample message for keylen>blocklen"
|
||||
mac = join [ 0x5f464f5e, 0x5b7848e3, 0x885e49b2, 0xc385f069
|
||||
, 0x4985d0e3, 0x8966242d, 0xc4a5fe3f, 0xea4b37d4
|
||||
, 0x6b65cece, 0xd5dcf594, 0x38dd840b, 0xab22269f
|
||||
, 0x0ba7febd, 0xb9fcf746, 0x02a35666, 0xb2a32915
|
||||
]
|
||||
|
||||
property Sample4 = take (HMAC key msg) == mac
|
||||
where
|
||||
key = split (join [ 0x00010203, 0x04050607, 0x08090a0b, 0x0c0d0e0f
|
||||
, 0x10111213, 0x14151617, 0x18191a1b, 0x1c1d1e1f
|
||||
, 0x20212223, 0x24252627, 0x28292a2b, 0x2c2d2e2f
|
||||
, 0x30313233, 0x34353637, 0x38393a3b, 0x3c3d3e3f
|
||||
])
|
||||
msg = join "Sample message for keylen<blocklen, with truncated tag"
|
||||
mac = join [ 0x7bb06d85, 0x9257b25c, 0xe73ca700, 0xdf34c5cb
|
||||
, 0xef5c898b, 0xac91029e, 0x0b27975d, 0x4e526a08
|
||||
]
|
||||
@@ -0,0 +1,9 @@
|
||||
# Bibliography
|
||||
|
||||
[FIPS-PUB-202] SHA-3 Standard: Permutation-Based Hash and
|
||||
Extendable-Output Functions. August 2015.
|
||||
http://dx.doi.org/10.6028/NIST.FIPS.202
|
||||
|
||||
[NIST-SP-800-185] NIST Special Publication 800-185. SHA-3 Derived
|
||||
Functions: cSHAKE, KMAC, TupleHash and ParallelHash. December 2016.
|
||||
https://doi.org/10.6028/NIST.SP.800-185
|
||||
@@ -0,0 +1,116 @@
|
||||
/*
|
||||
* Description: This module provides KECCAK Message Authentication
|
||||
* Code (KMAC) functions [NIST-SP-800-185 Section 4].
|
||||
*/
|
||||
|
||||
module algorithms::KMAC::Main where
|
||||
|
||||
import algorithms::Keccak::derived (bytepad, encode_string, right_encode)
|
||||
import algorithms::Keccak::Main (bitReordering)
|
||||
import algorithms::cSHAKE::Main (cSHAKE128, cSHAKE256)
|
||||
|
||||
/**
|
||||
* The KECCAK Message Authentication Code (KMAC128) algorithm is a PRF
|
||||
* and keyed hash function based on Keccak. It provides
|
||||
* variable-length output, and unlike `SHAKE128` and `cSHAKE128`,
|
||||
* altering the requested output length generates a new, unrelated
|
||||
* output [NIST-SP-800-185 Section 4.3].
|
||||
*
|
||||
* Inputs:
|
||||
* `K`: A key bit string of any length, including zero.
|
||||
* `X`: The main input bit string. It may be of any length, including zero.
|
||||
* `S`: A customization bit string of any length, including zero. If
|
||||
* no customization is desired, set `S` to the empty string.
|
||||
*
|
||||
* Notable types:
|
||||
* `L`: An integer representing the requested output length in
|
||||
* bits.
|
||||
*/
|
||||
KMAC128 :
|
||||
{ L, k, a, s }
|
||||
( L < 2 ^^ 2040, k < 2 ^^ 2040, fin a, s < 2 ^^ 2040)
|
||||
=> [k] -> [a] -> [s] -> [L]
|
||||
KMAC128 K X S =
|
||||
cSHAKE128`{L} newX (join "KMAC") S
|
||||
where
|
||||
K' = bitReordering K
|
||||
X' = bitReordering X
|
||||
newX = bitReordering (bytepad`{168} (encode_string K') # X' # right_encode`{L})
|
||||
|
||||
/**
|
||||
* The KECCAK Message Authentication Code (KMAC256) algorithm is a PRF
|
||||
* and keyed hash function based on Keccak. It provides
|
||||
* variable-length output, and unlike `SHAKE256` and `cSHAKE256`,
|
||||
* altering the requested output length generates a new, unrelated
|
||||
* output [NIST-SP-800-185 Section 4.3].
|
||||
*
|
||||
* Inputs:
|
||||
* `K`: A key bit string of any length, including zero.
|
||||
* `X`: The main input bit string. It may be of any length, including zero.
|
||||
* `S`: A customization bit string of any length, including zero. If
|
||||
* no customization is desired, set `S` to the empty string.
|
||||
*
|
||||
* Notable types:
|
||||
* `L`: An integer representing the requested output length in
|
||||
* bits.
|
||||
*/
|
||||
KMAC256 :
|
||||
{ L, k, a, s }
|
||||
( L < 2 ^^ 2040, k < 2 ^^ 2040, fin a, s < 2 ^^ 2040)
|
||||
=> [k] -> [a] -> [s] -> [L]
|
||||
KMAC256 K X S =
|
||||
cSHAKE256`{L} newX (join "KMAC") S
|
||||
where
|
||||
K' = bitReordering K
|
||||
X' = bitReordering X
|
||||
newX = bitReordering (bytepad`{136} (encode_string K') # X' # right_encode`{L})
|
||||
|
||||
/**
|
||||
* This is a variant of KMAC128 as an XOF [NIST-SP-800-185 Section
|
||||
* 4.3.1].
|
||||
*
|
||||
* Inputs:
|
||||
* `K`: A key bit string of any length, including zero.
|
||||
* `X`: The main input bit string. It may be of any length, including zero.
|
||||
* `S`: A customization bit string of any length, including zero. If
|
||||
* no customization is desired, set `S` to the empty string.
|
||||
*
|
||||
* Notable types:
|
||||
* `L`: An integer representing the requested output length in
|
||||
* bits.
|
||||
*/
|
||||
KMACXOF128 :
|
||||
{ L, k, a, s }
|
||||
( k < 2 ^^ 2040, fin a, s < 2 ^^ 2040)
|
||||
=> [k] -> [a] -> [s] -> [L]
|
||||
KMACXOF128 K X S =
|
||||
cSHAKE128`{L} newX (join "KMAC") S
|
||||
where
|
||||
K' = bitReordering K
|
||||
X' = bitReordering X
|
||||
newX = bitReordering (bytepad`{168} (encode_string K') # X' # right_encode`{0})
|
||||
|
||||
/**
|
||||
* This is a variant of KMAC256 as an XOF [NIST-SP-800-185 Section
|
||||
* 4.3.1].
|
||||
*
|
||||
* Inputs:
|
||||
* `K`: A key bit string of any length, including zero.
|
||||
* `X`: The main input bit string. It may be of any length, including zero.
|
||||
* `S`: A customization bit string of any length, including zero. If
|
||||
* no customization is desired, set `S` to the empty string.
|
||||
*
|
||||
* Notable types:
|
||||
* `L`: An integer representing the requested output length in
|
||||
* bits.
|
||||
*/
|
||||
KMACXOF256 :
|
||||
{ L, k, a, s }
|
||||
( k < 2 ^^ 2040, fin a, s < 2 ^^ 2040)
|
||||
=> [k] -> [a] -> [s] -> [L]
|
||||
KMACXOF256 K X S =
|
||||
cSHAKE256`{L} newX (join "KMAC") S
|
||||
where
|
||||
K' = bitReordering K
|
||||
X' = bitReordering X
|
||||
newX = bitReordering (bytepad`{136} (encode_string K') # X' # right_encode`{0})
|
||||
@@ -0,0 +1,15 @@
|
||||
# Bibliography
|
||||
|
||||
[FIPS-PUB-202] SHA-3 Standard: Permutation-Based Hash and
|
||||
Extendable-Output Functions. August 2015.
|
||||
http://dx.doi.org/10.6028/NIST.FIPS.202
|
||||
|
||||
[NIST-SP-800-185] SHA-3 Derived Functions: cSHAKE, KMAC, TupleHash,
|
||||
and ParallelHash. John Kelsey, Shu-jen Chang, Ray Perlnder. NIST
|
||||
Special Publication 800-185. December 2016.
|
||||
https://doi.org/10.6028/NIST.SP.800-185
|
||||
|
||||
[SHA3 Test Vectors], National Institute of Standards and
|
||||
Technology. Cryptographic Standards and Guidelines: Examples with
|
||||
Intermediate Values, 2022.
|
||||
https://csrc.nist.gov/projects/cryptographic-standards-and-guidelines/example-values
|
||||
@@ -0,0 +1,137 @@
|
||||
/*
|
||||
* Description: This is a Cryptol specification for the Secure Hash
|
||||
* Algorithm-3 (SHA-3) family of functions on binary data. Each of
|
||||
* the SHA-3 functions is based on an instance of the Keccak algorithm
|
||||
* that NIST selected as the winner of the SHA-3 Cryptographic Hash
|
||||
* Algorithm Competition. This Cryptol spec is also for the Keccak-p
|
||||
* family of mathematical permutations, including the permutation that
|
||||
* underlies Keccak, in order to facilite the development of
|
||||
* additional permutation-based cryptographic functions
|
||||
* [FIPS-PUB-202].
|
||||
*/
|
||||
|
||||
module algorithms::Keccak::Main where
|
||||
|
||||
import algorithms::Keccak::Types
|
||||
import algorithms::Keccak::StepMappings
|
||||
import shared::sponge::Main as sponge
|
||||
|
||||
/**
|
||||
* The conversion function from hexadecimal strings to the SHA-3
|
||||
* strings that they represent [FIPS-PUB-202 Section B.1].
|
||||
*/
|
||||
h2b : {n, m} (n <= 8 * m) => [m * 2 * 4] -> [n]
|
||||
h2b H
|
||||
| fin n => take (join (map reverse Hs))
|
||||
where Hs = groupBy`{8} H : [m][8]
|
||||
| n == inf => join (map reverse Hs) // avoid `take`
|
||||
where Hs = groupBy`{8} H : [m][8]
|
||||
|
||||
/** Test for `h2b` [FIPS-PUB-202 Section B.1] */
|
||||
property h2bTest = h2b`{14} 0xA32E == 0b1100_0101_0111_01
|
||||
|
||||
/**
|
||||
* The conversion function from SHA-3 bit strings to the hexadecimal
|
||||
* strings that represent them [FIPS-PUB-202 Section B.1].
|
||||
*/
|
||||
b2h : {n} (fin n) => [n] -> [n + n %^ 8]
|
||||
b2h S = H
|
||||
where
|
||||
T = S # zero : [n + n %^ 8]
|
||||
H = h2b`{m = n /^ (2 * 4)} T
|
||||
|
||||
/**
|
||||
* Property demonstrating that `h2b` inverts `b2h`.
|
||||
*
|
||||
* ```
|
||||
* :prove h2bInvertsb2h`{0}
|
||||
* :prove h2bInvertsb2h`{1}
|
||||
* :prove h2bInvertsb2h`{10}
|
||||
* ```
|
||||
*/
|
||||
h2bInvertsb2h : {n} (fin n) => [n] -> Bool
|
||||
property h2bInvertsb2h S = h2b`{n, n /^ 8} (b2h S) == S
|
||||
|
||||
/**
|
||||
* Property demonstrating that `b2h` inverts `h2b`.
|
||||
* Essentially, this transformation preserves all the full bytes of
|
||||
* `H` and zeros out the first `n %^ 8` residual bits in the last
|
||||
* partial byte, if one exists.
|
||||
*
|
||||
* ```
|
||||
* :prove b2hInvertsh2b`{0, 0}
|
||||
* :prove b2hInvertsh2b`{0, 1}
|
||||
* :prove b2hInvertsh2b`{1, 1}
|
||||
* :prove b2hInvertsh2b`{7, 1}
|
||||
* :prove b2hInvertsh2b`{8, 1}
|
||||
* :prove b2hInvertsh2b`{101, 33}
|
||||
* ```
|
||||
*/
|
||||
b2hInvertsh2b : {n, m} (fin m, n <= 8 * m) => [m * 2 * 4] -> Bool
|
||||
property b2hInvertsh2b H = b2h (h2b`{n, m} H) == L # z # R
|
||||
where
|
||||
L = take`{n - n % 8} H
|
||||
z = zero`{[n %^ 8]}
|
||||
R = drop`{back=n % 8} (take`{n + n %^ 8} H)
|
||||
|
||||
/**
|
||||
* Keccak employs a involutory bit-reordering function to swap between
|
||||
* binary and hexadecimal representations. Specifically, "In binary
|
||||
* representation, bytes are written with the low-order bit first,
|
||||
* while in hexadecimal representation, bytes are written with the
|
||||
* high-order digit first. E.g., 0x01 = 10000000 and 0x80 = 00000001."
|
||||
* [NIST-SP-800-185 Section 2]. Note that `take`ing `n` bits from a
|
||||
* reordered *infinte* sequence can give a different result than
|
||||
* reordering a finite sequence of length `n`. Namely, the residual
|
||||
* bits in any final partial byte may be different. For example:
|
||||
* ```
|
||||
* > take`{12} (bitReordering (0x123 # zero : [inf]))
|
||||
* 0x480
|
||||
* > bitReordering 0x123
|
||||
* 0x483
|
||||
* ```
|
||||
*/
|
||||
bitReordering : {a} [a] -> [a]
|
||||
bitReordering x
|
||||
| fin a => h2b`{m = (a - a % 8) / 8} bytes # bits
|
||||
where (bytes, bits) = splitAt`{front = a - (a % 8), back = a % 8} x
|
||||
| a == inf => h2b`{m = a} x
|
||||
|
||||
/**
|
||||
* Property demonstrating that `bitReordering` is an involution.
|
||||
*
|
||||
* ```
|
||||
* :prove bitReorderingIsAnInvolution`{0}
|
||||
* :prove bitReorderingIsAnInvolution`{1}
|
||||
* :prove bitReorderingIsAnInvolution`{31}
|
||||
* :prove bitReorderingIsAnInvolution`{32}
|
||||
* :prove bitReorderingIsAnInvolution`{33}
|
||||
* :prove bitReorderingIsAnInvolution`{100}
|
||||
* ```
|
||||
*/
|
||||
bitReorderingIsAnInvolution : {a} (fin a) => [a] -> Bool
|
||||
property bitReorderingIsAnInvolution x = bitReordering (bitReordering x) == x
|
||||
|
||||
/**
|
||||
* This property demonstrates that `take`ing `n` bits from a reordered
|
||||
* *infinte* sequence can give a different result than reordering a
|
||||
* finite sequence of length `n`. Namely, the residual bits in any
|
||||
* final partial byte may be different. This is something to be aware
|
||||
* of when working with infinite sequences, e.g. XOFs.
|
||||
*/
|
||||
bitReorderingInfIssue : Bool
|
||||
property bitReorderingInfIssue =
|
||||
take`{12} (bitReordering (0x123 # zero : [inf])) == 0x480
|
||||
/\ bitReordering 0x123 == 0x483
|
||||
|
||||
/**
|
||||
* The following defines the Keccak family of functions. In
|
||||
* particular, Keccak[c] = sponge[Keccak_p[1600, 24], pad10*1, 1600 -
|
||||
* c] [FIPS-PUB-202].
|
||||
*/
|
||||
Keccak :
|
||||
{c, d, a}
|
||||
(fin c, 1600 > c, fin a)
|
||||
=> [a] -> [d]
|
||||
Keccak N =
|
||||
take`{d, inf} (sponge::sponge`{b=1600, r=1600-c} Keccak_p_w64_nr24 (sponge::pad10s1 N))
|
||||
@@ -0,0 +1,46 @@
|
||||
/*
|
||||
* Description: This module contains a Cryptol specification for the
|
||||
* functions used to convert between state strings and state arrays in
|
||||
* the Keccak family of functions [FIPS-PUB-202].
|
||||
*/
|
||||
|
||||
module algorithms::Keccak::StateConversions where
|
||||
import algorithms::Keccak::Types as Types
|
||||
|
||||
/**
|
||||
* The following function transforms a string state `S` into a state
|
||||
* array `A` [FIPS-PUB-202 Section 3.1.2].
|
||||
*/
|
||||
toState : {w} (fin w) => Types::String w -> Types::State w
|
||||
toState S = A
|
||||
where
|
||||
A@x@y = (split S : [25][w]) @ (5 * y + x)
|
||||
|
||||
/**
|
||||
* The following function transforms a state array `A` into a string
|
||||
* state `S` [FIPS-PUB-202 Section 3.1.3].
|
||||
*/
|
||||
toString : {w} (fin w) => Types::State w -> Types::String w
|
||||
toString A = S
|
||||
where
|
||||
S = join [ A@i@j | j <- [0..4], i <- [0..4] ]
|
||||
|
||||
/**
|
||||
* The following property shows that `toString` inverts `toState`.
|
||||
* ```
|
||||
* :prove toStatetoStringProp`{32}
|
||||
* :prove toStatetoStringProp`{64}
|
||||
* ```
|
||||
*/
|
||||
toStatetoStringProp : {w} (fin w) => Types::String w -> Bool
|
||||
property toStatetoStringProp S = toString (toState S) == S
|
||||
|
||||
/**
|
||||
* The following property confirms that `toState` inverts `toString`.
|
||||
* ```
|
||||
* :prove toStringtoStateProp`{32}
|
||||
* :prove toStringtoStateProp`{64}
|
||||
* ```
|
||||
*/
|
||||
toStringtoStateProp : {w} (fin w) => Types::State w -> Bool
|
||||
property toStringtoStateProp S = toState (toString S) == S
|
||||
@@ -0,0 +1,154 @@
|
||||
/*
|
||||
* Description: This module is a Cryptol specification for the Step
|
||||
* Mapping algorithms as specified by [FIPS-PUB-202 Section 3.2].
|
||||
*/
|
||||
|
||||
module algorithms::Keccak::StepMappings where
|
||||
|
||||
import algorithms::Keccak::Types as Types
|
||||
import algorithms::Keccak::StateConversions
|
||||
import shared::LFSR::Main as LFSR
|
||||
import shared::common::utils::BitVector (parity)
|
||||
|
||||
/**
|
||||
* The following defines "⨁" as an infix operator for the XOR
|
||||
* operation and is used to match the formatting of [FIPS-PUB-202] as
|
||||
* closely as possible.
|
||||
*/
|
||||
(⨁) = (^)
|
||||
infixl 45 ⨁
|
||||
|
||||
/**
|
||||
* [FIPS-PUB-202 Algorithm 1]
|
||||
* 1. For all pairs (x,z) such that 0≤x<5 and 0≤z<w, let
|
||||
* C[x,z]=A[x,0,z] ⨁ A[x,1,z] ⨁ A[x,2,z] ⨁ A[x,3,z] ⨁ A[x,4,z].
|
||||
*
|
||||
* 2. For all pairs (x,z) such that 0≤x<5 and 0≤z<w, let
|
||||
* D[x,z] = C[(x-1) mod 5, z] ⨁ C[(x+1) mod 5, (z-1) mod w].
|
||||
*
|
||||
* 3. For all triples (x,y,z) such that 0≤x<5, 0≤y<5, and 0≤z<w, let
|
||||
* A'[x,y,z] = A[x,y,z] ⨁ D[x,z].
|
||||
*/
|
||||
θ : {w} (fin w) => Types::State w -> Types::State w
|
||||
θ A = A'
|
||||
where
|
||||
C, D : [5][w]
|
||||
C@x = A@x@0 ⨁ A@x@1 ⨁ A@x@2 ⨁ A@x@3 ⨁ A@x@4
|
||||
D@x = C@((x-1) % 5) ⨁ C@((x+1) % 5) >>> 1
|
||||
A'@x@y = A@x@y ⨁ D@x
|
||||
|
||||
/**
|
||||
* [FIPS-PUB-202 Algorithm 2]
|
||||
* 1. For all z such that 0≤z<w, let A'[0,0,z] = A[0,0,z].
|
||||
* 2. Let (x,y) = (1,0).
|
||||
* 3. For t from 0 to 23:
|
||||
* a. for all z such that 0≤z<w, let A'[x,y,z]=A[x,y,(z-(t+1)(t+2)/2 mod w]
|
||||
* b. let (x,y) = (y,(2x+3y) mod 5).
|
||||
*
|
||||
* Here we specify the offset table variant.
|
||||
*/
|
||||
ρ : {w} (fin w) => Types::State w -> Types::State w
|
||||
ρ A = A'
|
||||
where
|
||||
A' = groupBy`{5} [ a >>> o | a <- join A | o <- offsets ]
|
||||
offsets = [ 0, 36, 3, 105, 210
|
||||
, 1, 300, 10, 45, 66
|
||||
, 190, 6, 171, 15, 253
|
||||
, 28, 55, 153, 21, 120
|
||||
, 91, 276, 231, 136, 78
|
||||
]
|
||||
|
||||
/**
|
||||
* [FIPS-PUB-202 Algorithm 3]
|
||||
* For all triples (x,y,z) such that 0≤x<5, 0≤y<5, 0≤z<w, let
|
||||
* A'[x,y,z] = A[(x+3y) mod 5, x, z]
|
||||
*/
|
||||
π : {w} (fin w) => Types::State w -> Types::State w
|
||||
π A = A'
|
||||
where
|
||||
A'@x@y = A@((x + 3 * y) % 5)@x
|
||||
|
||||
/**
|
||||
* [FIPS-PUB-202 Algorithm 4]
|
||||
* For all triples (x,y,z) such that 0≤x<5, 0≤y<5, 0≤z<w, let
|
||||
* A'[x,y,z] = A[x,y,z] ⨁ ((A[(x+1) mod 5, y, z] ⨁ 1) ⦁ A[(x+2) mod 5, y, z]).
|
||||
*/
|
||||
χ : {w} (fin w) => Types::State w -> Types::State w
|
||||
χ A = A'
|
||||
where
|
||||
A'@x = A@x ⨁ ~A@((x+1) % 5) && A@((x+2) % 5)
|
||||
|
||||
/**
|
||||
* [FIPS-PUB-202 Algorithm 5]
|
||||
* The specification of ι's round constant `rc`. Each of these l + 1
|
||||
* bits is generated by a function that is based on a linear feedback
|
||||
* shift register. Note, l = log2(w).
|
||||
*/
|
||||
rc : [inf]
|
||||
rc = (LFSR::fmsrRun (⨁) <| x^^8 + x^^6 + x^^5 + x^^4 + 1 |> 0b10000000).stream
|
||||
|
||||
/**
|
||||
* [FIPS-PUB-202 Algorithm 6]
|
||||
* For all triples (x,y,z) such that 0≤x<5, 0≤y<5, 0≤z<w, let
|
||||
* A'[0,0,z]=A'[0,0,z] ⨁ RC[z].
|
||||
* Otherwise,
|
||||
* A'[x,y,z] = A[x,y,z].
|
||||
* The round constant bits for `ir` are excited by
|
||||
* RC[2^^j - 1] = rc(j+7*ir)
|
||||
*/
|
||||
ι :
|
||||
{w, a}
|
||||
(fin w, Integral a, Literal (max 7 (lg2 w)) a)
|
||||
=> Types::State w -> a -> Types::State w
|
||||
ι A ir = A'
|
||||
where
|
||||
type l = lg2 w // [FIPS-PUB-202 Section 2.2]
|
||||
A'@x@y = if (x == 0 /\ y == 0) then A@x@y ⨁ RC else A@x@y
|
||||
RC = updates zero
|
||||
[ 2^^j - 1 | j <- [0 .. l] ]
|
||||
[ rc @ (j + 7*ir) | j <- [0 .. l] ]
|
||||
|
||||
/**
|
||||
* The Keccak Round Function, `Rnd`, is the transformation that
|
||||
* results from applying the step functions in order [FIPS-PUB-202
|
||||
* part of Algorithm 7].
|
||||
*/
|
||||
Rnd :
|
||||
{w, a}
|
||||
(fin w, Integral a, Literal (max 7 (lg2 w)) a)
|
||||
=> Types::State w -> a -> Types::State w
|
||||
Rnd A ir = ι (χ (π (ρ (θ A)))) ir
|
||||
|
||||
/**
|
||||
* [FIPS-PUB-202 Algorithm 7]
|
||||
* 1. Converts `S` into a state array, `A`, as described in Section 3.1.2.
|
||||
* 2. For `ir` from `12+2l-nr` to `12+2l-1`, let `A = Rnd(A, ir)`.
|
||||
* 3. Convert `A` into a string `S'` of length `b`, as described in Section 3.1.3.
|
||||
* 4. Return `S'`.
|
||||
*/
|
||||
Keccak_p :
|
||||
{ w, nr }
|
||||
( fin w
|
||||
, fin nr
|
||||
, 12 + 2 * (lg2 w) >= nr
|
||||
)
|
||||
=> Types::String w -> Types::String w
|
||||
Keccak_p S = S'
|
||||
where
|
||||
type l = lg2 w
|
||||
A = toState S
|
||||
A' = foldl Rnd A [12 + 2*l - nr .. < 12 + 2*l]
|
||||
S' = toString A'
|
||||
|
||||
/**
|
||||
* A Rust FFI for Keccak_p specialized to `w = 64` and `nr = 24`.
|
||||
*/
|
||||
foreign Keccak_p_FFI : Types::State 64 -> Types::State 64
|
||||
Keccak_p_FFI A = toState (Keccak_p`{w = 64, nr = 24} (toString A))
|
||||
|
||||
/**
|
||||
* A shim to rejigger types for ease of FFI integration into the main
|
||||
* Keccak function.
|
||||
*/
|
||||
Keccak_p_w64_nr24 : Types::String 64 -> Types::String 64
|
||||
Keccak_p_w64_nr24 S = toString (Keccak_p_FFI (toState S))
|
||||
+1
@@ -0,0 +1 @@
|
||||
rust/target/release/libKeccak.dylib
|
||||
+1
@@ -0,0 +1 @@
|
||||
rust/target/release/libKeccak.so
|
||||
@@ -0,0 +1,20 @@
|
||||
/*
|
||||
* Description: This is a Cryptol specification for the types needed
|
||||
* to specify the Keccak family of algorithms.
|
||||
*/
|
||||
|
||||
module algorithms::Keccak::Types where
|
||||
|
||||
/**
|
||||
* The `State` type is a 5-by-5-by-w array of bits that represents the
|
||||
* state for a Keccak-p permutation. The indices for x, y, and z
|
||||
* coordinates range from 0 to 4, 0 to 4, and 0 to `w-1`, respectively
|
||||
* [FIPS-PUB-202 Section 2.1].
|
||||
*/
|
||||
type State w = [5][5][w]
|
||||
|
||||
/**
|
||||
* The `String` type is a 5*5*w array of bits that also represents the
|
||||
* state of a Keccak-p permutation [FIPS-PUB-202 Section 2.1].
|
||||
*/
|
||||
type String w = [5*5*w]
|
||||
@@ -0,0 +1,103 @@
|
||||
/*
|
||||
* Description: This is a Cryptol spec for several helper functions
|
||||
* used to define the SHA-3 derived hash functions `cSHAKE`, `KMAC`,
|
||||
* `TupleHash`, and `ParallelHash` [NIST-SP-800-185].
|
||||
*/
|
||||
|
||||
module algorithms::Keccak::derived where
|
||||
|
||||
/**
|
||||
* For a natural number `i` ranging from 0 to 255, `enc8 i` is the
|
||||
* byte encoding of `i`, with bit `0` being the low-order bit of the
|
||||
* byte [NIST-SP-800-185 Section 2.2]. This function differs in that
|
||||
* it will encode an entire sequence of bytes rather than just one.
|
||||
*/
|
||||
enc8 : {n} [n][8] -> [n][8]
|
||||
enc8 = map reverse
|
||||
|
||||
/**
|
||||
* This computes the number of bits needed to encode `x`
|
||||
* [NIST-SP-800-185 Section 2.3.1].
|
||||
*/
|
||||
type EncodeSize x = 8 * (1 + max 1 (width x /^ 8))
|
||||
|
||||
/**
|
||||
* This function encodes an integer `x` as a byte string in a way that
|
||||
* can be unambiguously parsed from the end of the string by inserting
|
||||
* the length of the byte string after the representation of `x`
|
||||
* [NIST-SP-800-185 Section 2.3.1].
|
||||
*/
|
||||
right_encode : {x} (x < 2 ^^ 2040) => [EncodeSize x]
|
||||
right_encode = join (𝑂 # 𝑂np1)
|
||||
where
|
||||
type n = max 1 (width x /^ 8)
|
||||
𝑂 = enc8 (groupBy`{8, n} `x)
|
||||
𝑂np1 = enc8 [fromInteger `n]
|
||||
|
||||
/** `right_encode` example [NIST-SP-800-185 Section 2.3.1] */
|
||||
property right_encode_example =
|
||||
right_encode`{0} == 0b00000000_10000000
|
||||
|
||||
/**
|
||||
* This function encodes an integer `x` as a byte string in a way that
|
||||
* can be unambiguously parsed from the beginning of the string by
|
||||
* inserting the length of the byte string before the representation
|
||||
* of `x` [NIST-SP-800-185 Section 2.3.1].
|
||||
*/
|
||||
left_encode : {x} (x < 2 ^^ 2040) => [EncodeSize x]
|
||||
left_encode = join (𝑂0 # 𝑂)
|
||||
where
|
||||
type n = max 1 (width x /^ 8)
|
||||
𝑂 = enc8 (groupBy`{8} `x)
|
||||
𝑂0 = enc8 [fromInteger `n]
|
||||
|
||||
/** `left_encode` example [NIST-SP-800-185 Section 2.3.1] */
|
||||
property left_encode_example =
|
||||
left_encode`{0} == 0b10000000_00000000
|
||||
|
||||
/**
|
||||
* This function encodes bit strings in a way that can be parsed
|
||||
* unambiguously from the beginning of the string `S` [NIST-SP-800-185
|
||||
* Section 2.3.2].
|
||||
*/
|
||||
encode_string :
|
||||
{x} (x < 2 ^^ 2040)
|
||||
=> [x] -> [EncodeSize x + x]
|
||||
encode_string S = left_encode`{x} # S
|
||||
|
||||
/** `encode_string` example [NIST-SP-800-185 Section 2.3.2] */
|
||||
property encode_string_example =
|
||||
encode_string [] == 0b10000000_00000000
|
||||
|
||||
/**
|
||||
* The `bytepad(X, w)` function prepends an encoding of the integer
|
||||
* `w` to the input string `X`, then pads the result with zeros until
|
||||
* it is a byte string whose length in bytes is a multiple of `w`. In
|
||||
* general, `bytepad` is intended to be used on encoded strings. The
|
||||
* byte string `bytepad(encode_string(S), w)` can be parsed
|
||||
* unambiguously from its beginning, whereas bytepad does not provide
|
||||
* unambiguous padding for all input strings [NIST-SP-800-185 Section
|
||||
* 2.3.3].
|
||||
*/
|
||||
bytepad :
|
||||
{w, a}
|
||||
(w > 0, w < 2 ^^ 2040, fin a)
|
||||
=> [a]
|
||||
-> [ EncodeSize a // `left_encode`
|
||||
+ a // `X`
|
||||
+ (EncodeSize a + a) %^ (w * 8) // pad to next multiple of `w`
|
||||
]
|
||||
bytepad X = left_encode`{w} # X # zero
|
||||
|
||||
/**
|
||||
* Let parameters `a` and `b` be non-negative integers that denote a
|
||||
* specific position in a bit string `X`. Informally, the
|
||||
* `substring(X, a, b)` function returns a substring from the bit
|
||||
* string `X` containing the values at bit positions `a, a+1, ...,
|
||||
* b−1`, inclusive. Note that all bit positions in the input and
|
||||
* output strings are indexed from zero. Thus, the first bit in a
|
||||
* string is in position `0`, and the last bit in an `n`-bit string is
|
||||
* in position `n−1` [NIST-SP-800-185 Section 2.3.4].
|
||||
*/
|
||||
substring : {a, b, n} (fin a, a <= b, b <= n) => [n] -> [b - a]
|
||||
substring X = X @@ [ a ..< b ]
|
||||
Generated
+14
@@ -0,0 +1,14 @@
|
||||
# This file is automatically @generated by Cargo.
|
||||
# It is not intended for manual editing.
|
||||
version = 3
|
||||
|
||||
[[package]]
|
||||
name = "Keccak"
|
||||
version = "0.1.0"
|
||||
dependencies = [
|
||||
"ffi_utils",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "ffi_utils"
|
||||
version = "0.1.0"
|
||||
@@ -0,0 +1,12 @@
|
||||
[package]
|
||||
name = "Keccak"
|
||||
version = "0.1.0"
|
||||
edition = "2021"
|
||||
|
||||
[lib]
|
||||
name = "Keccak"
|
||||
path = "src/lib.rs"
|
||||
crate-type = ["lib", "cdylib"]
|
||||
|
||||
[dependencies]
|
||||
ffi_utils = { path = "../../../shared/rust/ffi_utils" }
|
||||
@@ -0,0 +1,270 @@
|
||||
//! This is a Rust implementation of Keccak [FIPS-PUB-202] where `w
|
||||
//! = 64`.
|
||||
|
||||
#![allow(non_snake_case)]
|
||||
|
||||
/// The `State` type is a 5-by-5-by-w array of bits that represents
|
||||
/// the state for a `Keccak-p` permutation. The indices for `x`, `y`,
|
||||
/// and `z` coordinates range from 0 to 4, 0 to 4, and 0 to `w-1`,
|
||||
/// respectively [FIPS-PUB-202 Section 2.1].
|
||||
type State = [[u64; 5]; 5];
|
||||
|
||||
/// # `theta` [FIPS-PUB-202 Algorithm 1]
|
||||
///
|
||||
/// 1. For all pairs `(x,z)` such that `0≤x<5` and `0≤z<w`, let
|
||||
/// `C[x,z]=A[x,0,z] ⨁ A[x,1,z] ⨁ A[x,2,z] ⨁ A[x,3,z] ⨁ A[x,4,z]`.
|
||||
///
|
||||
/// 2. For all pairs `(x,z)` such that `0≤x<5` and `0≤z<w`, let
|
||||
/// `D[x,z] = C[(x-1) mod 5, z] ⨁ C[(x+1) mod 5, (z-1) mod w]`.
|
||||
///
|
||||
/// 3. For all triples (x,y,z) such that `0≤x<5`, `0≤y<5`, and
|
||||
/// `0≤z<w`, let `A'[x,y,z] = A[x,y,z] ⨁ D[x,z]`.
|
||||
#[allow(clippy::needless_range_loop)]
|
||||
fn theta(A: &mut State) {
|
||||
let mut C: [u64; 5] = [0; 5];
|
||||
let mut D: [u64; 5] = [0; 5];
|
||||
|
||||
for x in 0..5usize {
|
||||
C[x] = A[x][0] ^ A[x][1] ^ A[x][2] ^ A[x][3] ^ A[x][4];
|
||||
}
|
||||
|
||||
for x in 0..5usize {
|
||||
D[x] = C[(x + 5 - 1) % 5] ^ C[(x + 1) % 5].rotate_right(1);
|
||||
}
|
||||
|
||||
for x in 0..5usize {
|
||||
for y in 0..5usize {
|
||||
A[x][y] ^= D[x];
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// # `rho` [FIPS-PUB-202 Algorithm 2]
|
||||
///
|
||||
/// 1. For all `z` such that `0≤z<w`, let `A'[0,0,z] = A[0,0,z]`.
|
||||
/// 2. Let `(x,y) = (1,0)`.
|
||||
/// 3. For `t` from 0 to 23:
|
||||
/// a. for all `z` such that `0≤z<w`, let `A'[x,y,z]=A[x,y,(z-(t+1)(t+2)/2 mod w]`
|
||||
/// b. let `(x,y) = (y,(2x+3y) mod 5)`.
|
||||
///
|
||||
/// Here we specify the offset table variant.
|
||||
fn rho(A: &mut State) {
|
||||
let offsets = [
|
||||
[0, 36, 3, 105, 210],
|
||||
[1, 300, 10, 45, 66],
|
||||
[190, 6, 171, 15, 253],
|
||||
[28, 55, 153, 21, 120],
|
||||
[91, 276, 231, 136, 78],
|
||||
];
|
||||
|
||||
for x in 0..5usize {
|
||||
for y in 0..5usize {
|
||||
A[x][y] = A[x][y].rotate_right(offsets[x][y]);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// # `pi` [FIPS-PUB-202 Algorithm 3]
|
||||
///
|
||||
/// For all triples `(x,y,z)` such that `0≤x<5`, `0≤y<5`, `0≤z<w`, let
|
||||
/// `A'[x,y,z] = A[(x+3y) mod 5, x, z]`
|
||||
fn pi(A: &mut State) {
|
||||
let A_p = *A;
|
||||
for x in 0..5usize {
|
||||
for y in 0..5usize {
|
||||
A[x][y] = A_p[(x + 3 * y) % 5][x];
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// # `chi` [FIPS-PUB-202 Algorithm 4]
|
||||
///
|
||||
/// For all triples `(x,y,z)` such that `0≤x<5`, `0≤y<5`, `0≤z<w`, let
|
||||
/// `A'[x,y,z] = A[x,y,z] ⨁ ((A[(x+1) mod 5, y, z] ⨁ 1) ⦁ A[(x+2) mod
|
||||
/// 5, y, z])`.
|
||||
fn chi(A: &mut State) {
|
||||
let A_p = *A;
|
||||
for x in 0..5usize {
|
||||
for y in 0..5usize {
|
||||
A[x][y] = A_p[x][y] ^ !A_p[(x + 1) % 5][y] & A_p[(x + 2) % 5][y];
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// # `rc` [FIPS-PUB-202 Algorithm 5]
|
||||
///
|
||||
/// The specification of `iota`'s round constant `rc`, specialized and
|
||||
/// tabled given `w = 64`. The round constant bits for `ir` are
|
||||
/// excited by RC[2^^j - 1] = rc(j+7*ir)
|
||||
const RC: [u64; 24] = [
|
||||
0x8000_0000_0000_0000,
|
||||
0x4101_0000_0000_0000,
|
||||
0x5101_0000_0000_0001,
|
||||
0x0001_0001_0000_0001,
|
||||
0xd101_0000_0000_0000,
|
||||
0x8000_0001_0000_0000,
|
||||
0x8101_0001_0000_0001,
|
||||
0x9001_0000_0000_0001,
|
||||
0x5100_0000_0000_0000,
|
||||
0x1100_0000_0000_0000,
|
||||
0x9001_0001_0000_0000,
|
||||
0x5000_0001_0000_0000,
|
||||
0xd101_0001_0000_0000,
|
||||
0xd100_0000_0000_0001,
|
||||
0x9101_0000_0000_0001,
|
||||
0xc001_0000_0000_0001,
|
||||
0x4001_0000_0000_0001,
|
||||
0x0100_0000_0000_0001,
|
||||
0x5001_0000_0000_0000,
|
||||
0x5000_0001_0000_0001,
|
||||
0x8101_0001_0000_0001,
|
||||
0x0101_0000_0000_0001,
|
||||
0x8000_0001_0000_0000,
|
||||
0x1001_0001_0000_0001,
|
||||
];
|
||||
|
||||
/// # `iota` [FIPS-PUB-202 Algorithm 6]
|
||||
///
|
||||
/// For all triples `(x,y,z)` such that `0≤x<5`, `0≤y<5`, `0≤z<w`, let
|
||||
/// `A'[0,0,z]=A'[0,0,z] ⨁ RC[z]`. Otherwise, `A'[x,y,z] = A[x,y,z]`.
|
||||
fn iota(A: &mut State, ir: usize) {
|
||||
A[0][0] ^= RC[ir];
|
||||
}
|
||||
|
||||
/// The Keccak Round Function, `Rnd`, is the transformation that
|
||||
/// results from applying the step functions in order [FIPS-PUB-202
|
||||
/// part of Algorithm 7].
|
||||
fn Rnd(A: &mut State, ir: usize) {
|
||||
theta(A);
|
||||
rho(A);
|
||||
pi(A);
|
||||
chi(A);
|
||||
iota(A, ir);
|
||||
}
|
||||
|
||||
/// # `Keccak-p` [FIPS-PUB-202 Algorithm 7]
|
||||
///
|
||||
/// This function is specialized to `w = 64` and operates directly on
|
||||
/// `State`s.
|
||||
/// 1. For `ir` from `12+2l-nr` to `12+2l-1`, let `A = Rnd(A, ir)`.
|
||||
/// 2. Return `A`.
|
||||
fn Keccak_p(A: &mut State) {
|
||||
let l: usize = 6;
|
||||
let nr: usize = 24;
|
||||
for ir in (12 + 2 * l - nr)..(12 + 2 * l) {
|
||||
Rnd(A, ir);
|
||||
}
|
||||
}
|
||||
|
||||
/// FFI entrypoint for the `Keccak-p` function, specialized to `w = 64`.
|
||||
#[allow(clippy::not_unsafe_ptr_arg_deref)]
|
||||
#[allow(clippy::needless_range_loop)]
|
||||
#[export_name = "Keccak_p_FFI"]
|
||||
pub extern "C" fn Keccak_p_FFI(A_in: *const State, A_out: *mut State) {
|
||||
let A = unsafe { &mut *A_out };
|
||||
for x in 0..5usize {
|
||||
for y in 0..5usize {
|
||||
A[x][y] = unsafe { *A_in }[x][y];
|
||||
}
|
||||
}
|
||||
Keccak_p(A);
|
||||
}
|
||||
|
||||
/// # `pad10s1` [CSF-0.1 Section 2.1.2].
|
||||
///
|
||||
/// Appends a single 1 bit followed by the minimum number of 0 bits
|
||||
/// followed by a single 1 bit such that the length of the result is a
|
||||
/// multiple of the block length.
|
||||
fn pad10s1(rate_bytes: usize, mut message: Vec<u8>) -> Vec<u8> {
|
||||
// Apply `pad10*1` padding to the message
|
||||
let padding_length = rate_bytes - (message.len() % rate_bytes);
|
||||
if padding_length == 1 {
|
||||
message.push(0x81);
|
||||
} else {
|
||||
message.push(0x80); // Domain separator
|
||||
message.resize(message.len() + padding_length - 2, 0x00);
|
||||
message.push(0x01); // Final bit
|
||||
}
|
||||
message
|
||||
}
|
||||
|
||||
/// # `absorb` [CFS-0.1 Section 2.4.1].
|
||||
///
|
||||
/// `r`-bit input message blocks are `XORed` into the first `r` bits
|
||||
/// of the state, interleaved with applications of the function
|
||||
/// `Keccak-p`.
|
||||
fn absorb(rate_bytes: usize, padded_message: &[u8]) -> State {
|
||||
// Initialize the state
|
||||
let mut state: State = [[0u64; 5]; 5];
|
||||
|
||||
for block in padded_message.chunks(rate_bytes) {
|
||||
// Expand block to state
|
||||
for (i, chunk) in block.chunks(8).enumerate() {
|
||||
let mut value = 0u64;
|
||||
for (j, &byte) in chunk.iter().enumerate() {
|
||||
value |= u64::from(byte) << (8 * (7 - j));
|
||||
}
|
||||
state[i % 5][i / 5] ^= value;
|
||||
}
|
||||
Keccak_p(&mut state);
|
||||
}
|
||||
state
|
||||
}
|
||||
|
||||
/// # `squeeze` [CSF-0.1 Section 2.4.2]
|
||||
///
|
||||
/// Concatenation of the left-most `r` bits of compositions of
|
||||
/// `Keccak-p`.
|
||||
#[allow(clippy::needless_range_loop)]
|
||||
fn squeeze(rate_bytes: usize, digest_size: usize, mut state: State) -> Vec<u8> {
|
||||
assert!(
|
||||
rate_bytes.is_multiple_of(8),
|
||||
"Rate must be a multiple of 64."
|
||||
);
|
||||
let mut hash = Vec::new();
|
||||
while hash.len() < digest_size {
|
||||
for x in 0..5 {
|
||||
#[allow(clippy::needless_range_loop)]
|
||||
for y in 0..5 {
|
||||
if hash.len() < digest_size && (x * 5 * 8 + y * 8) < rate_bytes {
|
||||
hash.extend_from_slice(&state[y][x].to_be_bytes());
|
||||
}
|
||||
}
|
||||
}
|
||||
if hash.len() < digest_size {
|
||||
Keccak_p(&mut state);
|
||||
}
|
||||
}
|
||||
hash.truncate(digest_size);
|
||||
hash
|
||||
}
|
||||
|
||||
/// # `Keccak`
|
||||
///
|
||||
/// Implements the Keccak family of functions. This function uses the sponge
|
||||
/// construction with the `Keccak_p` permutation, `pad10*1` padding, and a
|
||||
/// specified rate `r` (1600 - capacity).
|
||||
///
|
||||
/// - `capacity`: The capacity of the sponge (in bits).
|
||||
/// - `digest_size`: The desired hash length in bytes.
|
||||
/// - `message`: The input message as a byte slice.
|
||||
///
|
||||
/// Returns the hash as a `Vec<u8>`.
|
||||
///
|
||||
/// # Panics
|
||||
///
|
||||
/// This function will panic is the capacity is out of range.
|
||||
#[must_use]
|
||||
pub fn Keccak(capacity: usize, digest_size: usize, message: &[u8]) -> Vec<u8> {
|
||||
const B: usize = 1600; // State size in bits
|
||||
let r = B - capacity; // Rate in bits
|
||||
let rate_bytes = r / 8;
|
||||
|
||||
assert!(capacity < B, "Capacity must be less than 1600 bits.");
|
||||
assert!(r >= 1, "Rate must be at least 1 bit.");
|
||||
assert!(r.is_multiple_of(8), "Rate must be a multiple of 8.");
|
||||
|
||||
let padded_message = pad10s1(rate_bytes, Vec::from(message));
|
||||
let state = absorb(rate_bytes, &padded_message);
|
||||
squeeze(rate_bytes, digest_size, state)
|
||||
}
|
||||
@@ -0,0 +1,72 @@
|
||||
from pathlib import Path
|
||||
import unittest
|
||||
from saw_client import *
|
||||
from saw_client.crucible import *
|
||||
from saw_client.mir import *
|
||||
from saw_client.proofscript import *
|
||||
from saw_client.mir_type import *
|
||||
|
||||
def ref_to_fresh(c : Contract, ty : MIRType, name : Optional[str] = None,
|
||||
read_only : bool = False) -> Tuple[FreshVar, SetupVal]:
|
||||
"""Add to ``Contract`` ``c`` an allocation of a reference of type ``ty`` initialized to an unknown fresh value.
|
||||
If ``read_only == True`` then the allocated memory is immutable.
|
||||
|
||||
:returns A fresh variable bound to the reference's initial value and the newly allocated reference. (The fresh
|
||||
variable will be assigned ``name`` if provided/available.)"""
|
||||
var = c.fresh_var(ty, name)
|
||||
ptr = c.alloc(ty, points_to = var, read_only = read_only)
|
||||
return (var, ptr)
|
||||
|
||||
# fn F(A: &mut State) {
|
||||
class mut_state_Contract(Contract):
|
||||
def __init__(self, F : CryptolTerm):
|
||||
super().__init__()
|
||||
self.F = F
|
||||
def specification(self):
|
||||
(A, A_ref) = ref_to_fresh(self, array_ty(5, array_ty(5, u64)), "A")
|
||||
self.execute_func(A_ref)
|
||||
self.points_to(A_ref, cry_f("{self.F} {A}"))
|
||||
self.returns(void)
|
||||
|
||||
def mut_state_verify(test, mod, F_rust, F_cryptol):
|
||||
""" Verify a function of type `fn F(A: &mut State)`."""
|
||||
result = mir_verify(mod, F_rust, mut_state_Contract(cry_f(F_cryptol)),
|
||||
script=ProofScript([rme]))
|
||||
test.assertIs(result.is_success(), True)
|
||||
return result
|
||||
|
||||
class Keccak_p_Contract(Contract):
|
||||
def specification(self):
|
||||
(A, A_ref) = ref_to_fresh(self, array_ty(5, array_ty(5, u64)), "A")
|
||||
self.execute_func(A_ref)
|
||||
self.points_to(A_ref, cry_f("toState (Keccak_p`{{w=64, nr=24}} (toString {A}))"))
|
||||
self.returns(void)
|
||||
|
||||
def Keccak_p_verify(test, mod, lemmas):
|
||||
result = mir_verify(mod, "Keccak::Keccak_p", Keccak_p_Contract(), lemmas,
|
||||
script=ProofScript([z3("θ ρ π χ".split())]))
|
||||
test.assertIs(result.is_success(), True)
|
||||
return result
|
||||
|
||||
class Keccak(unittest.TestCase):
|
||||
def test_Cipher(self):
|
||||
connect(reset_server=True)
|
||||
if __name__ == "__main__": view(LogResults(verbose_failure=True))
|
||||
|
||||
basedir = Path(__file__).absolute().parents[1] # Get absolute path to `Cargo.toml`
|
||||
StepMappings_crypath = basedir/"../StepMappings.cry"
|
||||
StateConversions_crypath = basedir/"../StateConversions.cry"
|
||||
mirpath = basedir/"linked-mir.json"
|
||||
|
||||
cryptol_load_file(str(StepMappings_crypath))
|
||||
cryptol_load_file(str(StateConversions_crypath))
|
||||
mod = mir_load_module(str(mirpath))
|
||||
|
||||
theta_result = mut_state_verify(self, mod, 'Keccak::theta', 'θ')
|
||||
rho_result = mut_state_verify(self, mod, 'Keccak::rho', 'ρ')
|
||||
pi_result = mut_state_verify(self, mod, 'Keccak::pi', 'π')
|
||||
chi_result = mut_state_verify(self, mod, 'Keccak::chi', 'χ')
|
||||
Keccak_p_result = Keccak_p_verify(self, mod, [theta_result, rho_result, pi_result, chi_result])
|
||||
|
||||
if __name__ == "__main__":
|
||||
unittest.main()
|
||||
@@ -0,0 +1,55 @@
|
||||
/*
|
||||
* This is a SAW script that guides SAW to prove the properties found
|
||||
* in `algorithms/Keccak/Main.cry`.
|
||||
*/
|
||||
|
||||
// Include common SAW utilities.
|
||||
include "../../../shared/SAW/utils.saw";
|
||||
|
||||
// Import the Cryptol specification for Keccak's main functions.
|
||||
import "../Main.cry";
|
||||
|
||||
let verify_h2bTest : TopLevel Theorem =
|
||||
proveit {{ h2bTest }} rme;
|
||||
|
||||
let verify_h2bInvertsb2h (n : Int) : TopLevel Theorem =
|
||||
proveit {{ h2bInvertsb2h`{n} }} rme;
|
||||
|
||||
let verify_b2hInvertsh2b (n : Int, m : Int) : TopLevel Theorem =
|
||||
proveit {{ b2hInvertsh2b`{n, m} }} rme;
|
||||
|
||||
let verify_bitReorderingIsAnInvolution (a : Int) : TopLevel Theorem =
|
||||
proveit {{ bitReorderingIsAnInvolution`{a} }} rme;
|
||||
|
||||
let verify_bitReorderingInfIssue : TopLevel Theorem =
|
||||
proveit {{ bitReorderingInfIssue }} rme;
|
||||
|
||||
/*
|
||||
* Verify public properties of `algorithms::Keccak::Main`.
|
||||
*/
|
||||
let main : TopLevel [Theorem] = do {
|
||||
h2bTest_lemma <- verify_h2bTest;
|
||||
h2bInvertsb2h_lemmas <- for [ 0, 1, 10 ] verify_h2bInvertsb2h;
|
||||
b2hInvertsh2b_lemmas <- for [ ( 0, 0 )
|
||||
, ( 0, 1 )
|
||||
, ( 1, 1 )
|
||||
, ( 7, 1 )
|
||||
, ( 8, 1 )
|
||||
, ( 101, 33 )
|
||||
] verify_b2hInvertsh2b;
|
||||
bitReorderingIsAnInvolution_lemmas <-
|
||||
for [ 0, 1, 31, 32, 33, 100 ] verify_bitReorderingIsAnInvolution;
|
||||
bitReorderingInfIssue_lemma <- verify_bitReorderingInfIssue;
|
||||
|
||||
summarize_verification;
|
||||
|
||||
return
|
||||
(foldl concat [ ]
|
||||
[ [ h2bTest_lemma ]
|
||||
, h2bInvertsb2h_lemmas
|
||||
, b2hInvertsh2b_lemmas
|
||||
, bitReorderingIsAnInvolution_lemmas
|
||||
, [ bitReorderingInfIssue_lemma ]
|
||||
]
|
||||
);
|
||||
};
|
||||
@@ -0,0 +1,33 @@
|
||||
/*
|
||||
* This is a SAW script that guides SAW to prove the properties found
|
||||
* in `algorithms/Keccak/StateConversions.cry`.
|
||||
*/
|
||||
|
||||
// Include common SAW utilities.
|
||||
include "../../../shared/SAW/utils.saw";
|
||||
|
||||
// Import the Cryptol specification for Keccak's `State` conversion functions.
|
||||
import "../StateConversions.cry";
|
||||
|
||||
let verify_toStatetoStringProp (w : Int) : TopLevel Theorem =
|
||||
proveit {{ toStatetoStringProp`{w} }} rme;
|
||||
|
||||
let verify_toStringtoStateProp (w : Int) : TopLevel Theorem =
|
||||
proveit {{ toStringtoStateProp`{w} }} rme;
|
||||
|
||||
/*
|
||||
* Verify public properties of `algorithms::Keccak::StateConversions`.
|
||||
*/
|
||||
let main : TopLevel [Theorem] = do {
|
||||
toStatetoStringProp_lemmas <- for [32, 64] verify_toStatetoStringProp;
|
||||
toStringtoStateProp_lemmas <- for [32, 64] verify_toStatetoStringProp;
|
||||
|
||||
summarize_verification;
|
||||
|
||||
return
|
||||
(foldl concat []
|
||||
[ toStatetoStringProp_lemmas
|
||||
, toStringtoStateProp_lemmas
|
||||
]
|
||||
);
|
||||
};
|
||||
@@ -0,0 +1,38 @@
|
||||
/*
|
||||
* This is a SAW script that guides SAW to prove the properties found
|
||||
* in `algorithms/Keccak`.
|
||||
*/
|
||||
|
||||
// Include common SAW utilities.
|
||||
include "../../../shared/SAW/utils.saw";
|
||||
|
||||
include "Main.saw";
|
||||
let Main_main = main;
|
||||
|
||||
include "derived.saw";
|
||||
let derived_main = main;
|
||||
|
||||
include "StateConversions.saw";
|
||||
let StateConversions_main = main;
|
||||
|
||||
/*
|
||||
* Script to run on command line:
|
||||
* `saw all.saw`
|
||||
* Return:
|
||||
* `TopLevel [Theorem]` verifying all lemmas used throughout `algorithms/Keccak`.
|
||||
*/
|
||||
let main : TopLevel [Theorem] = do {
|
||||
Main_lemmas <- Main_main;
|
||||
derived_lemmas <- derived_main;
|
||||
StateConversions_lemmas <- StateConversions_main;
|
||||
|
||||
summarize_verification;
|
||||
|
||||
return
|
||||
(foldl concat []
|
||||
[ Main_lemmas
|
||||
, derived_lemmas
|
||||
, StateConversions_lemmas
|
||||
]
|
||||
);
|
||||
};
|
||||
@@ -0,0 +1,35 @@
|
||||
/*
|
||||
* This is a SAW script that guides SAW to prove the properties found
|
||||
* in `algorithms/Keccak/derived.cry`.
|
||||
*/
|
||||
|
||||
// Include common SAW utilities.
|
||||
include "../../../shared/SAW/utils.saw";
|
||||
|
||||
// Import the Cryptol specification for Keccak's derived functions.
|
||||
import "../derived.cry";
|
||||
|
||||
let verify_right_encode_example : TopLevel Theorem =
|
||||
proveit {{ right_encode_example }} rme;
|
||||
|
||||
let verify_left_encode_example : TopLevel Theorem =
|
||||
proveit {{ left_encode_example }} rme;
|
||||
|
||||
let verify_encode_string_example : TopLevel Theorem =
|
||||
proveit {{ encode_string_example }} rme;
|
||||
|
||||
/*
|
||||
* Verify public properties of `algorithms::Keccak::derived`.
|
||||
*/
|
||||
let main : TopLevel [Theorem] = do {
|
||||
right_encode_example_lemma <- verify_right_encode_example;
|
||||
left_encode_example_lemma <- verify_left_encode_example;
|
||||
encode_string_example_lemma <- verify_encode_string_example;
|
||||
|
||||
summarize_verification;
|
||||
|
||||
return [ right_encode_example_lemma
|
||||
, left_encode_example_lemma
|
||||
, encode_string_example_lemma
|
||||
];
|
||||
};
|
||||
@@ -0,0 +1,15 @@
|
||||
/*
|
||||
* Description: This is a Cryptol specification for the KWAE and KWAD
|
||||
* functions [NIST-800-38F], specialized to AES-128.
|
||||
*/
|
||||
module algorithms::KeyWrapping::AES128 where
|
||||
|
||||
import algorithms::KeyWrapping::KW as KW
|
||||
import algorithms::KeyWrapping::KWP as KWP
|
||||
import algorithms::AES::Main (AES128)
|
||||
|
||||
KWAE KEK = KW::KWAE (AES128.Encrypt KEK)
|
||||
KWAD KEK = KW::KWAD (AES128.Decrypt KEK)
|
||||
|
||||
KWPAE KEK = KWP::KWPAE (AES128.Encrypt KEK)
|
||||
KWPAD KEK = KWP::KWPAD (AES128.Decrypt KEK)
|
||||
@@ -0,0 +1,15 @@
|
||||
/*
|
||||
* Description: This is a Cryptol specification for the KWAE and KWAD
|
||||
* functions [NIST-800-38F], specialized to AES-192.
|
||||
*/
|
||||
module algorithms::KeyWrapping::AES192 where
|
||||
|
||||
import algorithms::KeyWrapping::KW as KW
|
||||
import algorithms::KeyWrapping::KWP as KWP
|
||||
import algorithms::AES::Main (AES192)
|
||||
|
||||
KWAE KEK = KW::KWAE (AES192.Encrypt KEK)
|
||||
KWAD KEK = KW::KWAD (AES192.Decrypt KEK)
|
||||
|
||||
KWPAE KEK = KWP::KWPAE (AES192.Encrypt KEK)
|
||||
KWPAD KEK = KWP::KWPAD (AES192.Decrypt KEK)
|
||||
Loaded 100 of 241 files, more files were not shown because too many files have changed in this diff.
Show more
Reference in new issue
Block a user