Refactoring AES crypto code #56
Conversation
… into aes-crypto-review
…ndles authentication tags
src/Crypto/AESEncryption.dfy
Outdated
|
|
||
| //Note: AESDecrypt expects the message authentication tag (also known as MAC) to be present as the last n bytes of ctxt. | ||
| // n = params.tagLen | ||
| method AESDecrypt(params: AESUtils.Params, key: seq<uint8>, ctxt: seq<uint8>, iv: seq<uint8>, aad: seq<uint8>) |
There was a problem hiding this comment.
I think we should be more descriptive than params. encryptionParams? AESAlgorithm? encryptionAlg? algProperties? Naming is hard.
… returned by AES.
…hmSuite -> AESWrappingSuite
src/Crypto/AESEncryption.dfy
Outdated
| EncryptionArtifacts(s[.. |s| - p.tagLen as int], s[|s| - p.tagLen as int ..]) | ||
| } | ||
|
|
||
| method {:extern "AESEncryption.AES_GCM", "AESEncrypt"} AESEncrypt(params: EncryptionParameters.Params, iv: seq<uint8>, key: seq<uint8>, msg: seq<uint8>, aad: seq<uint8>) |
There was a problem hiding this comment.
Now that EncryptionParameters can represent more than just AES/GCM, we should change how we are passing this data in. A couple options I see:
- Add preconditions here to ensure that the params being passed in have "AES" and "GCM"
- Create a new datatype that is a subtype of Params, i.e. Params that have "AES" and "GCM"
(2) would be my preference, but I'm unsure how friendly dafny will be for that option, or if there are other considerations elsewhere in this PR that I may be missing. Thoughts?
There was a problem hiding this comment.
I looked into this initially, I couldn't figure out a decent was of sub typing a datatype. I'll go with option #1 in the next revision. We can discuss further in today's sync.
There was a problem hiding this comment.
Instead of a subtype, we could move GCM to a field of the AES Algorithm datatype.
The field now resides inside the AES datatype.
MatthewBennington
dismissed stale reviews from RustanLeino and lavaleri
via
70c1643
Issue #, if available: Partially addresses #36 (refactoring of
Cipher.dfy)Description of changes:
Cipher.dfyinto two files:WrappingAlgorithmSuite.dfy, andAESUtils.dfyAESEncryption.dfyinline with style, and added export set.Note: This PR does not address tests, or serialization/deserialization of the authentication tag. These are coming in my next PR.
Testing:
make allIt may make sense to wait for #47 before merging this PR.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.