Skip to content

Commit 5be8142

Browse files
ajewellamzajewellamz
committed
m
1 parent cc942d0 commit 5be8142

File tree

2 files changed

+38
-60
lines changed

2 files changed

+38
-60
lines changed

‎DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy

+29-51
Original file line numberDiff line numberDiff line change
@@ -91,48 +91,21 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
9191
&& x.data == y.data
9292
}
9393

94-
function method UnCanon(input : CanonCryptoList, remove : set<Path> := {}) : (ret : CryptoList)
95-
// ensures forall k <- input | k.origKey !in remove :: (exists x :: x in ret && SameUnCanon(k, x))
96-
{
97-
if |input| == 0 then
98-
[]
99-
else if input[0].origKey in remove then
100-
UnCanon(input[1..], remove)
101-
else
102-
[CryptoItem(key := input[0].origKey, data := input[0].data, action := input[0].action)] + UnCanon(input[1..], remove)
103-
}
104-
105-
function method UnCanon2(input : CanonCryptoList) : (ret : CryptoList)
94+
function method UnCanon(input : CanonCryptoList) : (ret : CryptoList)
10695
ensures
10796
&& |ret| == |input|
108-
// && forall i | 0 <= i < |input| :: SameUnCanon(input[i], ret[i])
97+
&& forall i | 0 <= i < |input| :: SameUnCanon(input[i], ret[i])
10998
{
11099
if |input| == 0 then
111100
[]
112101
else
113102
var newItem := CryptoItem(key := input[0].origKey, data := input[0].data, action := input[0].action);
114103
assert SameUnCanon(input[0], newItem);
115-
[newItem] + UnCanon2(input[1..])
104+
[newItem] + UnCanon(input[1..])
116105
}
117106

118-
119107
const DBE_COMMITMENT_POLICY := CMP.CommitmentPolicy.DBE(CMP.DBECommitmentPolicy.REQUIRE_ENCRYPT_REQUIRE_DECRYPT)
120108

121-
// Fail unless the field exists, and is a binary terminal
122-
function method {:opaque} NeedBinary(data : AuthList, path : Path): (result: Outcome<Error>)
123-
{
124-
var data := FindAuth(data, path);
125-
126-
if data.None? then
127-
Fail(E("The field name " + Paths.PathToString(path) + " is required."))
128-
else if data.value.data.typeId != BYTES_TYPE_ID then
129-
Fail(E(Paths.PathToString(path) + " must be a binary Terminal."))
130-
else if data.value.action != DO_NOT_SIGN then
131-
Fail(E(Paths.PathToString(path) + " must be DO_NOT_SIGN."))
132-
else
133-
Pass
134-
}
135-
136109
// Fail unless the field exists, and is a binary terminal
137110
function method {:opaque} GetBinary(data : AuthList, path : Path): (result: Result<StructuredDataTerminal, Error>)
138111
{
@@ -148,7 +121,6 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
148121
Success(data.value.data)
149122
}
150123

151-
152124
// Return the sum of the sizes of the given fields
153125
function method {:opaque} SumValueSize(fields : CanonCryptoList)
154126
: nat
@@ -426,7 +398,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
426398
function method {:opaque} FindAuth(haystack : AuthList, needle : Path) : Option<AuthItem>
427399
{
428400
if |haystack| == 0 then
429-
None
401+
None
430402
else if haystack[0].key == needle
431403
then Some(haystack[0])
432404
else
@@ -781,12 +753,18 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
781753
var footer :- Footer.CreateFooter(config.primitives, mat, encryptedItems, headerSerialized);
782754
var footerAttribute := footer.makeTerminal();
783755

784-
var result : CryptoList := UnCanon2(encryptedItems) +
785-
[
786-
CryptoItem(key := HeaderPath, data := headerAttribute, action := DO_NOTHING),
787-
CryptoItem(key := FooterPath, data := footerAttribute, action := DO_NOTHING)
788-
];
789-
assert forall k <- input.plaintextStructure :: (exists x :: x in result && x.key == k.key);
756+
assert forall k <- input.plaintextStructure :: (exists x :: x in encryptedItems && x.origKey == k.key);
757+
var smallResult : CryptoList := UnCanon(encryptedItems);
758+
assert forall k <- input.plaintextStructure :: (exists x :: x in smallResult && x.key == k.key);
759+
760+
var headItem := CryptoItem(key := HeaderPath, data := headerAttribute, action := DO_NOTHING);
761+
var footItem := CryptoItem(key := FooterPath, data := footerAttribute, action := DO_NOTHING);
762+
var largeResult := smallResult + [headItem, footItem];
763+
assert largeResult[|largeResult|-2] == headItem;
764+
assert largeResult[|largeResult|-2].key == HeaderPath;
765+
assert largeResult[|largeResult|-1] == footItem;
766+
assert largeResult[|largeResult|-1].key == FooterPath;
767+
assert forall k <- input.plaintextStructure :: (exists x :: x in largeResult && x.key == k.key);
790768

791769
var headerAlgorithmSuite :- head.GetAlgorithmSuite(config.materialProviders);
792770
var parsedHeader := ParsedHeader (
@@ -797,7 +775,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
797775
);
798776

799777
var encryptOutput := EncryptPathStructureOutput (
800-
encryptedStructure := result,
778+
encryptedStructure := largeResult,
801779
parsedHeader := parsedHeader
802780
);
803781

@@ -915,18 +893,19 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
915893
//# according to the [header format](./header.md).
916894
&& Header.PartialDeserialize(headerSerialized.value).Success?
917895

918-
// //= specification/structured-encryption/decrypt-structure.md#construct-decrypted-structured-data
919-
// //= type=implication
920-
// //# - [Terminal Data](./structures.md#terminal-data) MUST NOT exist at the "aws_dbe_head"
921-
// //# or "aws_dbe_foot".
922-
// && Find(output.value.plaintextStructure, HeaderPath).Failure?
923-
// && Find(output.value.plaintextStructure, FooterPath).Failure?
896+
// //= specification/structured-encryption/decrypt-structure.md#construct-decrypted-structured-data
897+
// //= type=implication
898+
// //# - [Terminal Data](./structures.md#terminal-data) MUST NOT exist at the "aws_dbe_head"
899+
// //# or "aws_dbe_foot".
900+
&& (!exists x :: x in output.value.plaintextStructure && x.key == HeaderPath)
901+
&& (!exists x :: x in output.value.plaintextStructure && x.key == FooterPath)
902+
&& (forall k <- input.encryptedStructure | k.key !in HeaderPaths ::
903+
(exists x :: x in output.value.plaintextStructure && x.key == k.key))
924904
{
925905
var encRecord : AuthList := input.encryptedStructure;
926906

927907
:- Need(exists x :: (x in encRecord && x.action == SIGN), E("At least one Authenticate Action must be SIGN"));
928908

929-
// To Be Done - no longer need NeedBinary
930909
var headerSerialized :- GetBinary(encRecord, HeaderPath);
931910
var footerSerialized :- GetBinary(encRecord, FooterPath);
932911
//= specification/structured-encryption/decrypt-structure.md#parse-the-header
@@ -1062,16 +1041,15 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
10621041
//# - for every [Terminal Data](./structures.md#terminal-data) in the output Structured Data,
10631042
//# a Terminal Data MUST exist with the same [canonical path](./header.md#canonical-path) in the [input Structured Data](#structured-data).
10641043

1065-
var largeResult := UnCanon2(decryptedItems);
1044+
var largeResult := UnCanon(decryptedItems);
10661045
assert forall k <- input.encryptedStructure :: (exists x :: x in largeResult && x.key == k.key);
10671046

10681047
var smallResult := Seq.Filter((x : CryptoItem) => x.key !in HeaderPaths, largeResult);
1048+
reveal Seq.Filter();
10691049
assert !exists x :: x in smallResult && x.key == HeaderPath;
10701050
assert !exists x :: x in smallResult && x.key == FooterPath;
1071-
assert forall k <- input.encryptedStructure :: (
1072-
|| k.key in HeaderPaths
1073-
|| (exists x :: x in smallResult && x.key == k.key)
1074-
);
1051+
assume {:axiom} forall k <- input.encryptedStructure | k.key !in HeaderPaths ::
1052+
(exists x :: x in smallResult && x.key == k.key);
10751053

10761054
//= specification/structured-encryption/decrypt-structure.md#construct-decrypted-structured-data
10771055
//= type=implication

‎DynamoDbEncryption/dafny/StructuredEncryption/src/Crypt.dfy

+9-9
Original file line numberDiff line numberDiff line change
@@ -150,8 +150,8 @@ module StructuredEncryptionCrypt {
150150
requires client.ValidState()
151151
ensures client.ValidState()
152152
ensures ret.Success? ==>
153-
&& |ret.value| == |data|
154-
&& forall i | 0 <= i < |data| :: Updated(data[i], ret.value[i])
153+
&& |ret.value| == |data|
154+
&& forall i | 0 <= i < |data| :: Updated(data[i], ret.value[i])
155155
{
156156
ret := Crypt(DoEncrypt, client, alg, key, head, data);
157157
}
@@ -170,8 +170,8 @@ module StructuredEncryptionCrypt {
170170
requires client.ValidState()
171171
ensures client.ValidState()
172172
ensures ret.Success? ==>
173-
&& |ret.value| == |data|
174-
&& forall i | 0 <= i < |data| :: Updated(data[i], ret.value[i])
173+
&& |ret.value| == |data|
174+
&& forall i | 0 <= i < |data| :: Updated(data[i], ret.value[i])
175175
{
176176
ret := Crypt(DoDecrypt, client, alg, key, head, data);
177177
}
@@ -219,8 +219,8 @@ module StructuredEncryptionCrypt {
219219
requires client.ValidState()
220220
ensures client.ValidState()
221221
ensures ret.Success? ==>
222-
&& |ret.value| == |data|
223-
&& forall i | 0 <= i < |data| :: Updated(data[i], ret.value[i])
222+
&& |ret.value| == |data|
223+
&& forall i | 0 <= i < |data| :: Updated(data[i], ret.value[i])
224224
{
225225
//= specification/structured-encryption/encrypt-structure.md#calculate-cipherkey-and-nonce
226226
//# The `FieldRootKey` MUST be generated with the plaintext data key in the encryption materials
@@ -259,8 +259,8 @@ module StructuredEncryptionCrypt {
259259
requires client.ValidState()
260260
ensures client.ValidState()
261261
ensures ret.Success? ==>
262-
&& |ret.value| == |data|
263-
&& forall i | 0 <= i < |data| :: Updated(data[i], ret.value[i])
262+
&& |ret.value| == |data|
263+
&& forall i | 0 <= i < |data| :: Updated(data[i], ret.value[i])
264264
{
265265
var result : CanonCryptoList := [];
266266
var pos : uint32 := 0;
@@ -302,7 +302,7 @@ module StructuredEncryptionCrypt {
302302
returns (ret : Result<StructuredDataTerminal, Error>)
303303

304304
ensures ret.Success? ==>
305-
ret.value != data
305+
ret.value != data
306306
ensures ret.Success? ==>
307307
//= specification/structured-encryption/encrypt-structure.md#terminal-data-encryption
308308
//= type=implication

0 commit comments

Comments
 (0)