Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
20 commits
Select commit Hold shift + click to select a range
48dad61
Added lab on new module system
WeeknightMVP Sep 27, 2022
f58ae03
Replaced tabs with spaces
WeeknightMVP Sep 27, 2022
9e4f1cb
Add lab on new module system
WeeknightMVP Nov 18, 2023
eb582ac
Add AES exercises and test vectors
WeeknightMVP Dec 8, 2023
842abdd
Remove properties section and correct some formatting
WeeknightMVP Dec 8, 2023
6c5061b
Merge remote-tracking branch 'origin' into new-module-system
WeeknightMVP Dec 8, 2023
da47f97
Comment out specs that depend on unfinished exercises
WeeknightMVP Dec 10, 2023
8438e55
Fix typo in `labs/NewModuleSystem`
WeeknightMVP Oct 30, 2024
14cc534
Clarify term for `generator expression` in `labs/NewModuleSystem`
WeeknightMVP Oct 30, 2024
d9a59bd
Reroute recommended paths; add multi-lab landing page for module system
WeeknightMVP Oct 30, 2024
2a32fc3
Merge remote-tracking branch 'origin' into new-module-system
WeeknightMVP Oct 30, 2024
d9a5fbb
Merge branch 'master' of https://github.com/weaversa/cryptol-course i…
WeeknightMVP Oct 31, 2024
e9b8839
Merge remote-tracking branch 'refs/remotes/origin/new-module-system' …
WeeknightMVP Oct 31, 2024
cc1804d
Merge remote-tracking branch 'origin' into new-module-system
WeeknightMVP Oct 31, 2024
644b1a8
Update `Suggested Lab Order` in `README.md`
WeeknightMVP Oct 31, 2024
6893e14
Correct graphic in Module System landing page
WeeknightMVP Oct 31, 2024
87d7587
Restore `Key Wrapping` lab description in `README.md`
WeeknightMVP Oct 31, 2024
5c2c104
Promote `Key Wrapping` back into recommended path
WeeknightMVP Nov 4, 2024
79f855f
Compact course graph
WeeknightMVP Nov 4, 2024
e7bf083
Correct course navigation
WeeknightMVP Nov 4, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 13 additions & 6 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -126,16 +126,23 @@ first lab walks you through [installing and running Cryptol](INSTALL.md).
* [Continuous Reasoning with SAW](./labs/SAW/SAW.md): Learn how to
use Python to drive SAW and enforce formal invariants on
cryptographic implementations at every check-in to a repository.
8. [Methods for Key Wrapping](./labs/KeyWrapping/KeyWrapping.md):
8. [Module System](./labs/ModuleSystem.md):
Parameterize modules to reuse cores of related specifications.
* [Parameterized Modules: Simon and Speck](./SimonSpeck/SimonSpeck.md)
Cut your teeth on Cryptol modules with the Simon/Speck family of
related block ciphers.
* [New Module System: Block Cipher Modes](./NewModuleSystem/NewModuleSystem.md)
Unleash the full power of Cryptol 3's new module system on
modes of operation for any compatible block cipher.
9. [Methods for Key Wrapping](./labs/KeyWrapping/KeyWrapping.md):
Create a Cryptol specification of NIST's [SP800-38F key wrap
standard](https://csrc.nist.gov/publications/detail/sp/800-38f/final).
* [Parameterized Modules: Simon and Speck](./labs/SimonSpeck/SimonSpeck.md):
Learn about Cryptol's parameterized modules by creating a
Cryptol specification of NSA's Speck block cipher.
9. [Capstone: Putting it all together](./labs/LoremIpsum/LoremIpsum.md):
standard](https://csrc.nist.gov/publications/detail/sp/800-38f/final)
by combining most concepts learned throughout the course.
10. [Capstone: Putting it all together](./labs/LoremIpsum/LoremIpsum.md):
Use components and techniques from other labs to decrypt a series
of secret messages by feeding wrapped keys into the anomalous KLI20
cryptographic engine.


## Graphical View of the Course

Expand Down
2 changes: 1 addition & 1 deletion labs/CryptoProofs/CryptoProofs.md
Original file line number Diff line number Diff line change
Expand Up @@ -377,7 +377,7 @@ https://github.com/weaversa/cryptol-course/issues
||||
|-:|:-:|-|
|| [ ^ Course README](../../README.md) ||
| [< Salsa20](../Salsa20/Salsa20.md) | **Cryptographic Properties** | [Key Wrapping >](../KeyWrapping/KeyWrapping.md) |
| [< Salsa20](../Salsa20/Salsa20.md) | **Cryptographic Properties** | [Module System >](../ModuleSystem.md) |
|| [! Cryptographic Properties (Answers)](./CryptoProofsAnswers.md) ||
||||
|| [+ Salsa20 Properties](../Salsa20/Salsa20Props.md) ||
Expand Down
2 changes: 1 addition & 1 deletion labs/CryptoProofs/CryptoProofsAnswers.md
Original file line number Diff line number Diff line change
Expand Up @@ -471,7 +471,7 @@ https://github.com/weaversa/cryptol-course/issues
||||
|-:|:-:|-|
|| [ ^ Course README](../../README.md) ||
| [< Salsa20](../Salsa20/Salsa20.md) | **Cryptographic Properties (Answers)** | [Key Wrapping >](../KeyWrapping/KeyWrapping.md) |
| [< Salsa20](../Salsa20/Salsa20.md) | **Cryptographic Properties (Answers)** | [Module System >](../ModuleSystem.md) |
|| [? Cryptographic Properties](./CryptoProofs.md) ||
||||
|| [+ Salsa20 Properties](../Salsa20/Salsa20Props.md) ||
Expand Down
2 changes: 1 addition & 1 deletion labs/KeyWrapping/KeyWrapping.md
Original file line number Diff line number Diff line change
Expand Up @@ -1121,7 +1121,7 @@ https://github.com/weaversa/cryptol-course/issues
||||
|-:|:-:|-|
|| [ ^ Course README](../../README.md) ||
| [< Cryptographic Properties](../CryptoProofs/CryptoProofs.md) | **Key Wrapping** | [Capstone >](../LoremIpsum/LoremIpsum.md) |
| [< Module System](../ModuleSystem.md) | **Key Wrapping** | [Capstone >](../LoremIpsum/LoremIpsum.md) |
|| [! Key Wrapping (Answers)](./KeyWrappingAnswers.md) ||
||||
|| [+ Parameterized Modules](../SimonSpeck/SimonSpeck.md) ||
25 changes: 25 additions & 0 deletions labs/ModuleSystem.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
# Module System

* [Parameterized Modules](./SimonSpeck/SimonSpeck.md)
Cut your teeth on Cryptol modules with the Simon/Speck family of
related block ciphers.
* [New Module System](./NewModuleSystem/NewModuleSystem.md)
Unleash the full power of Cryptol 3's new module system on
modes of operation for any compatible block cipher.

<a href="../misc/ModuleSystem.gv.svg">
<img class="center" src="../misc/ModuleSystem.gv.svg" alt="Module System - Suggested Flow">
</a>

# Solicitation

How was your experience with this lab? Suggestions are welcome in the
form of a ticket on the course GitHub page:
https://github.com/weaversa/cryptol-course/issues

# From here, you can go somewhere!

||||
|-:|:-:|-|
| [< Cryptographic Properties](./CryptoProofs/CryptoProofs.md) | **Module System** | [Key Wrapping >](./KeyWrapping/KeyWrapping.md) ||
|| [v Parameterized Modules](./SimonSpeck/SimonSpeck.md) ||
Loading