Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Refactoring AES crypto code #56

Merged
merged 19 commits into from
Oct 24, 2019
Merged

Refactoring AES crypto code #56

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
19 commits
Select commit Hold shift + click to select a range
4a636fe
Refactoring AES crypto code
MatthewBennington Oct 3, 2019
e5dcfa6
Merge branch 'develop' of github.com:awslabs/aws-encryption-sdk-dafny…
MatthewBennington Oct 3, 2019
e00db9f
Addressing PR comments
MatthewBennington Oct 3, 2019
c3a39bb
Addressing PR comments, and adding explainations for AESEncryption ha…
MatthewBennington Oct 4, 2019
b400edd
Addressing PR comments. Mostly to seperate the ciphertext and authtag…
MatthewBennington Oct 7, 2019
bf84ede
Addressing PR comments. Mostly moving and refactoring WrappingAlgorit…
MatthewBennington Oct 7, 2019
1711ca5
Removing AESWrappingSuite
MatthewBennington Oct 7, 2019
6601113
Removing Dafny class from AESEncryption, misc fixes to AESKeyring
MatthewBennington Oct 9, 2019
29e3ed3
Removing uses of except for the output of AESEncrypt
MatthewBennington Oct 11, 2019
cc65208
Remove AES Mode datatype
MatthewBennington Oct 15, 2019
9a0720a
Merge branch 'develop' of github.com:awslabs/aws-encryption-sdk-dafny…
MatthewBennington Oct 15, 2019
5de67bf
Generalizing AESUtils
MatthewBennington Oct 17, 2019
33c7dcf
Fix make build
MatthewBennington Oct 17, 2019
ad8be28
Address PR comments, propagate Params.Valid() predicate.
MatthewBennington Oct 18, 2019
f82cbce
Remove the `mode` field from EncryptionAlgorithms.Params.
MatthewBennington Oct 21, 2019
52f55a9
Remove old comment
MatthewBennington Oct 21, 2019
f57321c
Rename `Params` to `EncryptionAlgorithm`.
MatthewBennington Oct 21, 2019
313f647
EncryptionAlgorithm(s) -> EncryptionSuite(s)
MatthewBennington Oct 23, 2019
70c1643
Make Main.dfy verify
MatthewBennington Oct 24, 2019
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
4 changes: 2 additions & 2 deletions src/Crypto/AESEncryption.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,11 +22,11 @@ module {:extern "AESEncryption"} AESEncryption {
res := AES.AESDecrypt(params, key, ctxt, iv, aad);
}

method AESEncrypt(params: AESUtils.Params, iv : seq<uint8>, key : seq<uint8>, msg : seq<uint8>, aad : seq<uint8>)
method AESEncrypt(params: AESUtils.Params, iv: seq<uint8>, key: seq<uint8>, msg: seq<uint8>, aad: seq<uint8>)
returns (res : Result<seq<uint8>>)
requires |iv| == params.ivLen as int
requires |key| == params.keyLen as int
ensures res.Success? ==> |res.value| > params.tagLen as int
ensures res.Success? ==> params.tagLen as int < |res.value|
{
res := AES.AESEncrypt(params, iv, key, msg, aad);
}
Expand Down
6 changes: 3 additions & 3 deletions src/Crypto/AESUtils.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,8 +14,8 @@ module {:extern "AESUtils"} AESUtils {

function method KeyLengthOfCipher(m: Mode): uint8 {
match m
case AES256 => 32 as uint8
case AES192 => 24 as uint8
case AES128 => 16 as uint8
case AES256 => 32 as uint8
case AES192 => 24 as uint8
case AES128 => 16 as uint8
MatthewBennington marked this conversation as resolved.
Show resolved Hide resolved
}
}
8 changes: 4 additions & 4 deletions src/Crypto/WrappingAlgorithmSuite.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,14 +14,14 @@ module WrappingAlgorithmSuite {

const VALID_ALGORITHMS := {AES_GCM_128, AES_GCM_192, AES_GCM_256}

method GenIV(p: AES.Params) returns (s : seq<uint8>)
ensures |s| == p.ivLen as int
method GenIV(p: AES.Params) returns (s: seq<uint8>)
ensures |s| == p.ivLen as int
{
s := RNG.GenBytes(p.ivLen as uint16);
}

method GenKey(p: AES.Params) returns (s : seq<uint8>)
ensures |s| == p.keyLen as int
method GenKey(p: AES.Params) returns (s: seq<uint8>)
ensures |s| == p.keyLen as int
{
s := RNG.GenBytes(p.keyLen as uint16);
}
Expand Down
4 changes: 2 additions & 2 deletions src/SDK/Keyring/AESKeyring.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,8 +31,8 @@ module AESKeyringDef {

predicate Valid() reads this {
Repr == {this} &&
(|wrappingKey| == wrappingAlgorithm.keyLen as int) &&
(wrappingAlgorithm in WrappingSuite.VALID_ALGORITHMS) &&
|wrappingKey| == wrappingAlgorithm.keyLen as int &&
wrappingAlgorithm in WrappingSuite.VALID_ALGORITHMS &&
StringIs8Bit(keyNamespace) && StringIs8Bit(keyName)
}

Expand Down
2 changes: 1 addition & 1 deletion src/SDK/ToyClient.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -87,7 +87,7 @@ module ToyClientDef {
case Some(dk) =>
if |dk| == 32 && |e.ctxt| > 12 {
var cipherText := e.ctxt[WrappingAlgorithmSuite.AES_GCM_256.ivLen ..];
var iv := e.ctxt[0 .. WrappingAlgorithmSuite.AES_GCM_256.ivLen];
var iv := e.ctxt[.. WrappingAlgorithmSuite.AES_GCM_256.ivLen];
var msg := AESEncryption.AESDecrypt(WrappingAlgorithmSuite.AES_GCM_256, dk, cipherText, iv, []);
return msg;
} else {
Expand Down