Skip to content

Commit d042829

Browse files
ajewellamzajewellamz
committed
m
1 parent f6d6e37 commit d042829

File tree

3 files changed

+169
-93
lines changed

3 files changed

+169
-93
lines changed

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

+113-40
Original file line numberDiff line numberDiff line change
@@ -109,6 +109,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
109109

110110
// Fail unless the field exists, and is a binary terminal
111111
function method {:opaque} GetBinary(data : AuthList, path : Path): (result: Result<StructuredDataTerminal, Error>)
112+
ensures result.Success? ==> exists x :: x in data && x.key == path
112113
{
113114
var data := FindAuth(data, path);
114115

@@ -250,6 +251,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
250251
ensures result.origKey == data.key
251252
ensures result.data == data.data
252253
ensures result.action == data.action
254+
ensures SameAuth(data, result)
253255
{
254256
CanonAuthItem(Paths.CanonPath(tableName, data.key), data.key, data.data, data.action)
255257
}
@@ -259,7 +261,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
259261
: (ret : Result<CanonCryptoList, Error>)
260262
ensures ret.Success? ==>
261263
&& (forall k <- data :: Paths.ValidPath(k.key))
262-
&& (forall k <- data :: (exists x :: x in ret.value && x.origKey == k.key))
264+
&& (forall k <- data :: (exists x :: x in ret.value && x.origKey == k.key && k.data == x.data))
263265
&& |data| == |ret.value|
264266
&& (forall k <- ret.value :: Paths.ValidPath(k.origKey))
265267
&& (forall k <- ret.value :: k.key == Paths.CanonPath(tableName, k.origKey))
@@ -269,7 +271,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
269271

270272
assert |canonList| == |data|;
271273
assert forall i | 0 <= i < |data| :: canonList[i] == MakeCanon(tableName, data[i]);
272-
assert forall k <- data :: (exists x :: x in canonList && k.key == x.origKey);
274+
assert forall k <- data :: (exists x :: x in canonList && k.key == x.origKey && k.data == x.data);
273275
assert forall k <- canonList :: Paths.ValidPath(k.origKey);
274276
assert forall k <- canonList :: k.key == Paths.CanonPath(tableName, k.origKey);
275277

@@ -304,6 +306,28 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
304306
&& x.data == y.data
305307
}
306308

309+
predicate method SameAuth(x : AuthItem, y : CanonAuthItem)
310+
{
311+
&& x.key == y.origKey
312+
&& x.data == y.data
313+
}
314+
315+
predicate method SameAuthCrypto(x : AuthItem, y : CanonCryptoItem)
316+
{
317+
&& x.key == y.origKey
318+
&& x.data == y.data
319+
}
320+
321+
lemma SameSame(x : AuthItem, y : CanonAuthItem, z : CanonCryptoItem)
322+
requires SameAuth(x, y)
323+
requires Same(y, z)
324+
ensures SameAuthCrypto(x, z)
325+
{}
326+
327+
lemma SameSame2(x : AuthItem, z : CanonCryptoItem)
328+
ensures exists y :: SameAuth(x, y) && Same(y, z) ==> SameAuthCrypto(x, z)
329+
{}
330+
307331
function method MakeCryptoItem(x : CanonAuthItem, action : CryptoAction) : (ret : CanonCryptoItem)
308332
ensures Same(x, ret)
309333
{
@@ -339,7 +363,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
339363
: (ret : Result<CanonCryptoList, Error>)
340364
ensures ret.Success? ==>
341365
&& (forall k <- data :: Paths.ValidPath(k.key))
342-
&& (forall k <- data :: (exists x :: x in ret.value && x.origKey == k.key))
366+
&& (forall k <- data :: (exists x :: x in ret.value && k.key == x.origKey && k.data == x.data))
343367
&& |data| == |ret.value|
344368
&& (forall k <- ret.value :: Paths.ValidPath(k.origKey))
345369
&& (forall k <- ret.value :: k.key == Paths.CanonPath(tableName, k.origKey))
@@ -349,7 +373,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
349373

350374
assert |canonList| == |data|;
351375
assert forall i | 0 <= i < |data| :: canonList[i] == MakeCanonAuth(tableName, data[i]);
352-
assert forall k <- data :: (exists x :: x in canonList && k.key == x.origKey);
376+
assert forall k <- data :: (exists x :: x in canonList && k.key == x.origKey && k.data == x.data);
353377
assert forall k <- canonList :: Paths.ValidPath(k.origKey);
354378
assert forall k <- canonList :: k.key == Paths.CanonPath(tableName, k.origKey);
355379

@@ -360,7 +384,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
360384
assert forall k <- canonList :: k in canonSorted;
361385
assert forall k <- canonSorted :: k in multiset(canonSorted);
362386
assert forall k <- canonSorted :: k in canonList;
363-
assert forall k <- data :: (exists x :: x in canonSorted && k.key == x.origKey);
387+
assert forall k <- data :: (exists x :: x in canonSorted && k.key == x.origKey && k.data == x.data);
364388
assert forall k <- canonSorted :: Paths.ValidPath(k.origKey);
365389
assert forall k <- canonSorted :: k.key == Paths.CanonPath(tableName, k.origKey);
366390

@@ -371,7 +395,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
371395
var canonResolved :- ResolveLegend(canonSorted, legend, canonSorted, acc);
372396

373397
assert |canonResolved| == |data|;
374-
assert forall k <- data :: (exists x :: x in canonResolved && k.key == x.origKey);
398+
assert forall k <- data :: (exists x :: x in canonResolved && k.key == x.origKey && k.data == x.data);
375399
assert forall k <- canonResolved :: Paths.ValidPath(k.origKey);
376400
assert forall k <- canonResolved :: k.key == Paths.CanonPath(tableName, k.origKey);
377401

@@ -400,7 +424,8 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
400424
Find(haystack[1..], needle)
401425
}
402426

403-
function method {:opaque} FindAuth(haystack : AuthList, needle : Path) : Option<AuthItem>
427+
function method {:opaque} FindAuth(haystack : AuthList, needle : Path) : (result : Option<AuthItem>)
428+
ensures result.Some? ==> exists x :: x in haystack && x.key == needle
404429
{
405430
if |haystack| == 0 then
406431
None
@@ -964,9 +989,6 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
964989
}
965990

966991
method {:vcs_split_on_every_assert} DecryptPathStructure (config: InternalConfig, input: DecryptPathStructureInput)
967-
//= specification/structured-encryption/decrypt-path-structure.md#construct-decrypted-structured-data
968-
//= type=implication
969-
//# This operation MUST output a [Structured Data](#structured-data) with the following specifics:
970992
returns (output: Result<DecryptPathStructureOutput, Error>)
971993

972994
ensures output.Success? ==>
@@ -978,6 +1000,11 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
9781000
//# this operation MUST access the [Terminal Data](./structures.md#terminal-data)
9791001
//# at the "aws_dbe_head"
9801002

1003+
//= specification/structured-encryption/decrypt-path-structure.md#auth-list
1004+
//= type=implication
1005+
//# This Auth List MUST contain data located at the [header index](./header.md#header-index)
1006+
//# and the [footer index](./footer.md#footer-index).
1007+
9811008
//= specification/structured-encryption/decrypt-path-structure.md#parse-the-header
9821009
//= type=implication
9831010
//# The [Terminal Type Id](./structures.md#terminal-type-id) on this Terminal Data MUST be `0xFFFF`.
@@ -994,6 +1021,10 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
9941021
&& GetBinary(encRecord, FooterPath).Success?
9951022
&& var footerSerialized := GetBinary(encRecord, FooterPath).value;
9961023

1024+
//= specification/structured-encryption/decrypt-path-structure.md#auth-list
1025+
//= type=implication
1026+
//# The Auth List MUST include at least one [SIGN Authenticate Action](./structures.md#sign);
1027+
//# otherwise, this operation MUST yield an error.
9971028
&& (exists x :: (x in encRecord && x.action == SIGN))
9981029

9991030
//= specification/structured-encryption/decrypt-path-structure.md#parse-the-header
@@ -1002,30 +1033,64 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
10021033
//# according to the [header format](./header.md).
10031034
&& Header.PartialDeserialize(headerSerialized.value).Success?
10041035

1005-
// //= specification/structured-encryption/decrypt-path-structure.md#construct-decrypted-structured-data
1006-
// //= type=implication
1007-
// //# - [Terminal Data](./structures.md#terminal-data) MUST NOT exist at the "aws_dbe_head"
1008-
// //# or "aws_dbe_foot".
1036+
//= specification/structured-encryption/decrypt-path-structure.md#construct-decrypted-structured-data
1037+
//= type=implication
1038+
//# - An entry MUST NOT exist with the key "aws_dbe_head" or "aws_dbe_foot".
10091039
&& (!exists x :: x in output.value.plaintextStructure && x.key == HeaderPath)
10101040
&& (!exists x :: x in output.value.plaintextStructure && x.key == FooterPath)
1041+
1042+
//= specification/structured-encryption/decrypt-path-structure.md#construct-decrypted-structured-data
1043+
//= type=implication
1044+
//# - For every entry in the [input Auth List](#auth-list), other than the header and footer,
1045+
//# an entry MUST exist with the same key in the output Crypto List.
10111046
&& (forall k <- input.encryptedStructure | k.key !in HeaderPaths ::
10121047
(exists x :: x in output.value.plaintextStructure && x.key == k.key))
1048+
1049+
//= specification/structured-encryption/decrypt-path-structure.md#construct-decrypted-structured-data
1050+
//= type=implication
1051+
//# - The output Crypto List MUST NOT have any additional entries.
1052+
&& |output.value.plaintextStructure| == |input.encryptedStructure| - 2
1053+
1054+
//= specification/structured-encryption/decrypt-path-structure.md#construct-decrypted-structured-data
1055+
//= type=implication
1056+
//# If the action is [ENCRYPT_AND_SIGN](./structures.md#encryptandsign)
1057+
//# this Terminal Data MUST have [Terminal Type ID](./structures.md#terminal-type-id)
1058+
//# equal to the first two bytes of the input Terminal Data's value,
1059+
//# and a value equal to the [decryption](#terminal-data-decryption) of the input Terminal Data's value.
1060+
1061+
//= specification/structured-encryption/decrypt-path-structure.md#construct-decrypted-structured-data
1062+
//= type=implication
1063+
//# Otherwise, this Terminal Data MUST have [Terminal Type ID](./structures.md#terminal-type-id) and
1064+
//# [Terminal Value](./structures.md#terminal-value) equal to the input Terminal Data.
1065+
&& (forall k <- input.encryptedStructure | k.key !in HeaderPaths ::
1066+
(exists x ::
1067+
&& x in output.value.plaintextStructure
1068+
&& x.key == k.key
1069+
&& (
1070+
|| x.action == ENCRYPT_AND_SIGN
1071+
|| x.data == k.data
1072+
)))
1073+
10131074
{
1014-
var encRecord : AuthList := input.encryptedStructure;
1075+
:- Need(exists x :: (x in input.encryptedStructure && x.action == SIGN), E("At least one Authenticate Action must be SIGN"));
10151076

1016-
:- Need(exists x :: (x in encRecord && x.action == SIGN), E("At least one Authenticate Action must be SIGN"));
1077+
var headerSerialized :- GetBinary(input.encryptedStructure, HeaderPath);
1078+
var footerSerialized :- GetBinary(input.encryptedStructure, FooterPath);
1079+
assert exists x :: x in input.encryptedStructure && x.key == HeaderPath;
1080+
assert exists x :: x in input.encryptedStructure && x.key == FooterPath;
10171081

1018-
var headerSerialized :- GetBinary(encRecord, HeaderPath);
1019-
var footerSerialized :- GetBinary(encRecord, FooterPath);
10201082
//= specification/structured-encryption/decrypt-path-structure.md#parse-the-header
10211083
//# This operation MUST deserialize the header bytes
10221084
//# according to the [header format](./header.md).
10231085
var head :- Header.PartialDeserialize(headerSerialized.value);
10241086
var headerAlgorithmSuite :- head.GetAlgorithmSuite(config.materialProviders);
10251087

10261088
:- Need(ValidString(input.tableName), E("Bad Table Name"));
1027-
var canonData :- CanonizeForDecrypt(input.tableName, encRecord, head.legend);
1028-
assert forall k <- input.encryptedStructure :: (exists x :: x in canonData && x.origKey == k.key);
1089+
var canonData :- CanonizeForDecrypt(input.tableName, input.encryptedStructure, head.legend);
1090+
assert forall k <- input.encryptedStructure :: (exists x :: x in canonData && k.key == x.origKey && k.data == x.data);
1091+
assert |canonData| == |input.encryptedStructure|;
1092+
assert exists x :: x in canonData && x.origKey == HeaderPath;
1093+
assert exists x :: x in canonData && x.origKey == FooterPath;
10291094

10301095
assume {:axiom} input.cmm.Modifies !! {config.materialProviders.History};
10311096

@@ -1126,13 +1191,6 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
11261191
//# The header field value MUST be [verified](header.md#commitment-verification)
11271192
var ok :- head.verifyCommitment(config.primitives, postCMMAlg, commitKey, headerSerialized.value);
11281193

1129-
//= specification/structured-encryption/decrypt-path-structure.md#calculate-signed-and-encrypted-field-lists
1130-
//= type=implication
1131-
//# Decryption MUST fail if the length of this list does not equal the
1132-
//# length of the header's [Encrypt Legend](header.md.#encrypt-legend).
1133-
// this assert can be an implication, because it is explicitly ensuring an intermediate state.
1134-
// assert |head.legend| == |canonData.signedFields_c|;
1135-
11361194
//= specification/structured-encryption/decrypt-path-structure.md#verify-signatures
11371195
//# This operation MUST deserialize the bytes in [Terminal Value](./structures.md#terminal-value)
11381196
//# according to the [footer format](./footer.md).
@@ -1145,27 +1203,44 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
11451203
//# Decryption MUST fail immediately if verification fails.
11461204
var _ :- footer.validate(config.primitives, mat, head.dataKeys, canonData, headerSerialized.value);
11471205
var decryptedItems : CanonCryptoList :- Crypt.Decrypt(config.primitives, postCMMAlg, key, head, canonData);
1148-
1149-
//= specification/structured-encryption/decrypt-path-structure.md#construct-decrypted-structured-data
1150-
//# - For every [input Terminal Data](./structures.md#terminal-data) in the [input Structured Data](#structured-data)
1151-
//# (aside from the header and footer),
1152-
//# a Terminal Data MUST exist with the same [canonical path](./header.md#canonical-path) in the output Structured Data.
1153-
// at this point both result and encRecord have header and footer
1206+
assert |decryptedItems| == |input.encryptedStructure|;
11541207
assert forall k <- input.encryptedStructure :: (exists x :: x in decryptedItems && x.origKey == k.key);
1208+
assert exists x :: x in decryptedItems && x.origKey == HeaderPath;
1209+
assert exists x :: x in decryptedItems && x.origKey == FooterPath;
11551210

1156-
//= specification/structured-encryption/decrypt-path-structure.md#construct-decrypted-structured-data
1157-
//# - for every [Terminal Data](./structures.md#terminal-data) in the output Structured Data,
1158-
//# a Terminal Data MUST exist with the same [canonical path](./header.md#canonical-path) in the [input Structured Data](#structured-data).
1211+
assert (forall k <- input.encryptedStructure ::
1212+
(exists x ::
1213+
&& x in decryptedItems
1214+
&& x.origKey == k.key
1215+
&& Crypt.Updated2(k, x, Crypt.DoDecrypt)
1216+
));
11591217

11601218
var largeResult := UnCanon(decryptedItems);
1219+
assert |largeResult| == |input.encryptedStructure|;
11611220
assert forall k <- input.encryptedStructure :: (exists x :: x in largeResult && x.key == k.key);
1221+
assert (forall k <- input.encryptedStructure ::
1222+
(exists x ::
1223+
&& x in largeResult
1224+
&& x.key == k.key
1225+
&& Crypt.Updated3(k, x, Crypt.DoDecrypt)
1226+
));
11621227

1228+
assert exists x :: x in largeResult && x.key == HeaderPath;
1229+
assert exists x :: x in largeResult && x.key == FooterPath;
11631230
var smallResult := Seq.Filter((x : CryptoItem) => x.key !in HeaderPaths, largeResult);
11641231
reveal Seq.Filter();
11651232
assert !exists x :: x in smallResult && x.key == HeaderPath;
11661233
assert !exists x :: x in smallResult && x.key == FooterPath;
1167-
assume {:axiom} forall k <- input.encryptedStructure | k.key !in HeaderPaths ::
1168-
(exists x :: x in smallResult && x.key == k.key);
1234+
assume {:axiom} forall k <- largeResult | k.key !in HeaderPaths :: (exists x :: x in smallResult && x == k);
1235+
:- Need(|smallResult| == |input.encryptedStructure| - 2, E("Internal Error."));
1236+
assert |smallResult| == |input.encryptedStructure| - 2;
1237+
1238+
assert (forall k <- input.encryptedStructure | k.key !in HeaderPaths ::
1239+
(exists x ::
1240+
&& x in smallResult
1241+
&& x.key == k.key
1242+
&& Crypt.Updated3(k, x, Crypt.DoDecrypt)
1243+
));
11691244

11701245
//= specification/structured-encryption/decrypt-path-structure.md#construct-decrypted-structured-data
11711246
//= type=implication
@@ -1183,8 +1258,6 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
11831258
parsedHeader := parsedHeader
11841259
);
11851260

1186-
// assert forall k <- decryptOutput.plaintextStructure :: k in encRecord;
1187-
11881261
output := Success(decryptOutput);
11891262
}
11901263

0 commit comments

Comments
 (0)