Skip to content

Commit 0ce9d55

Browse files
ajewellamzajewellamz
committed
m
1 parent 1ce388f commit 0ce9d55

File tree

5 files changed

+191
-69
lines changed

5 files changed

+191
-69
lines changed

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

+6-6
Original file line numberDiff line numberDiff line change
@@ -101,6 +101,8 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
101101
assert AuthListHasNoDuplicates(input.authActions);
102102
var head :- Header.PartialDeserialize(input.headerBytes);
103103
:- Need(ValidString(input.tableName), E("Bad Table Name"));
104+
:- Need(exists x :: x in input.authActions && x.key == HeaderPath, E("Header Required"));
105+
:- Need(exists x :: x in input.authActions && x.key == FooterPath, E("Footer Required"));
104106
var canonData :- ForDecrypt(input.tableName, input.authActions, head.legend);
105107
reveal CanonCryptoMatchesAuthList();
106108
return Success(ResolveAuthActionsOutput(cryptoActions := UnCanon(canonData)));
@@ -493,7 +495,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
493495
ensures forall k <- finalData :: |k.key| == 1
494496
{
495497
reveal EncryptPathFinal();
496-
reveal CryptoUpdatedCryptoList();
498+
reveal CryptoUpdatedCryptoListHeader();
497499
reveal NewCryptoUpdatedCrypto();
498500
}
499501

@@ -560,8 +562,6 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
560562
return Success(plainOutput);
561563
}
562564

563-
const HeaderPaths : seq<Path> := [HeaderPath, FooterPath]
564-
565565
//= specification/structured-encryption/encrypt-path-structure.md#encrypted-structured-data
566566
//= type=implication
567567
//# - for every entry in the input [Crypto List](#crypto-list)
@@ -572,7 +572,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
572572
ensures forall k <- origData :: (exists x :: x in finalData && x.key == k.key)
573573
{
574574
reveal EncryptPathFinal();
575-
reveal CryptoUpdatedCryptoList();
575+
reveal CryptoUpdatedCryptoListHeader();
576576
reveal CryptoUpdatedNewCrypto();
577577
}
578578

@@ -596,7 +596,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
596596
ensures forall k <- origData :: (exists x :: x in finalData && Updated4(k, x, DoDecrypt))
597597
{
598598
reveal EncryptPathFinal();
599-
reveal CryptoUpdatedCryptoList();
599+
reveal CryptoUpdatedCryptoListHeader();
600600
reveal CryptoUpdatedNewCrypto();
601601
}
602602

@@ -609,7 +609,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
609609
ensures forall k <- finalData[..(|finalData|-2)] :: (exists x :: x in origData && x.key == k.key)
610610
{
611611
reveal EncryptPathFinal();
612-
reveal CryptoUpdatedCryptoList();
612+
reveal CryptoUpdatedCryptoListHeader();
613613
reveal NewCryptoUpdatedCrypto();
614614
}
615615

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

+98-15
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ module Canonize {
1616
import SortCanon
1717
import Relations
1818

19-
predicate method {:opaque} IsValidPath(path : Path)
19+
predicate {:opaque} IsValidPath(path : Path)
2020
{
2121
Paths.ValidPath(path)
2222
}
@@ -163,11 +163,13 @@ module Canonize {
163163
function method {:opaque} ForEncrypt(tableName : GoodString, data : CryptoList)
164164
: (ret : Result<CanonCryptoList, Error>)
165165
requires CryptoListHasNoDuplicates(data)
166+
requires !exists x | x in data :: x.key in HeaderPaths
166167
ensures ret.Success? ==>
167168
&& CanonCryptoMatchesCryptoList(tableName, data, ret.value)
168169
&& IsCryptoSorted(ret.value)
169170
{
170-
:- Need(forall k <- data :: IsValidPath(k.key), E("Invalid Paths"));
171+
reveal IsValidPath();
172+
:- Need(forall k <- data :: Paths.ValidPath(k.key), E("Invalid Paths"));
171173
var canonList := CryptoToCanonCrypto(tableName, data);
172174
Success(CryptoSort(canonList, tableName, data))
173175
}
@@ -234,6 +236,8 @@ module Canonize {
234236

235237
predicate {:opaque} CanonAuthMatchesAuthList(tableName : GoodString, data : AuthList, canonList : CanonAuthList)
236238
{
239+
&& (exists x :: x in data && x.key == HeaderPath)
240+
&& (exists x :: x in data && x.key == FooterPath)
237241
&& (forall k <- data :: AuthExistsInCanonAuth(k, canonList))
238242
&& (forall k <- canonList :: CanonAuthExistsInAuth(k, data))
239243
&& |data| == |canonList|
@@ -244,6 +248,8 @@ module Canonize {
244248

245249
predicate {:opaque} CanonCryptoMatchesAuthList(tableName : GoodString, data : AuthList, canonList : CanonCryptoList)
246250
{
251+
&& (exists x :: x in data && x.key == HeaderPath)
252+
&& (exists x :: x in data && x.key == FooterPath)
247253
&& (forall k <- data :: AuthExistsInCanonCrypto(k, canonList))
248254
&& (forall k <- canonList :: CanonCryptoExistsInAuth(k, data))
249255
&& |data| == |canonList|
@@ -294,6 +300,8 @@ module Canonize {
294300

295301
predicate {:opaque} CanonCryptoUpdatedAuthList(tableName : GoodString, data : AuthList, canonList : CanonCryptoList)
296302
{
303+
&& (exists x :: x in data && x.key == HeaderPath)
304+
&& (exists x :: x in data && x.key == FooterPath)
297305
&& (forall k <- data :: AuthUpdatedCanonCrypto(k, canonList))
298306
&& (forall k <- canonList :: CanonCryptoUpdatedAuth(k, data))
299307
&& |data| == |canonList|
@@ -304,6 +312,8 @@ module Canonize {
304312

305313
predicate {:opaque} CryptoUpdatedAuthList(data : AuthList, canonList : CryptoList)
306314
{
315+
&& (exists x :: x in data && x.key == HeaderPath)
316+
&& (exists x :: x in data && x.key == FooterPath)
307317
&& (forall k <- data :: AuthUpdatedCrypto(k, canonList))
308318
&& (forall k <- canonList :: CryptoUpdatedAuth(k, data))
309319
&& |data| == |canonList|
@@ -322,6 +332,7 @@ module Canonize {
322332

323333
predicate {:opaque} CanonCryptoMatchesCryptoList(tableName : GoodString, data : CryptoList, canonList : CanonCryptoList)
324334
{
335+
&& (!exists x | x in data :: x.key in HeaderPaths)
325336
&& (forall k <- data :: CryptoExistsInCanonCrypto(k, canonList))
326337
&& (forall k <- canonList :: CanonCryptoExistsInCrypto(k, data))
327338
&& |data| == |canonList|
@@ -332,6 +343,7 @@ module Canonize {
332343

333344
predicate {:opaque} CanonCryptoUpdatedCryptoList(tableName : GoodString, data : CryptoList, canonList : CanonCryptoList)
334345
{
346+
&& (!exists x | x in data :: x.key in HeaderPaths)
335347
&& (forall k <- data :: CryptoUpdatedCanonCrypto(k, canonList))
336348
&& (forall k <- canonList :: CanonCryptoUpdatedCrypto(k, data))
337349
&& |data| == |canonList|
@@ -342,15 +354,28 @@ module Canonize {
342354

343355
predicate {:opaque} CryptoUpdatedCryptoList(data : CryptoList, canonList : CryptoList)
344356
{
357+
&& (!exists x | x in data :: x.key in HeaderPaths)
345358
&& (forall k <- data :: CryptoUpdatedNewCrypto(k, canonList))
346359
&& (forall k <- canonList :: NewCryptoUpdatedCrypto(k, data))
347360
&& |data| == |canonList|
348361
&& (forall k <- canonList :: IsValidPath(k.key))
349362
&& CryptoListHasNoDuplicates(canonList)
350363
}
351364

365+
predicate {:opaque} CryptoUpdatedCryptoListHeader(data : CryptoList, canonList : CryptoList)
366+
{
367+
&& (forall k <- data :: CryptoUpdatedNewCrypto(k, canonList))
368+
&& (forall k <- canonList :: NewCryptoUpdatedCrypto(k, data))
369+
&& |data| == |canonList|
370+
&& (forall k <- canonList :: IsValidPath(k.key))
371+
&& CryptoListHasNoDuplicates(canonList)
372+
}
373+
374+
352375
function method {:opaque} AuthToCanonAuth(tableName : GoodString, data : AuthList) : (ret : CanonAuthList)
353376
requires forall k <- data :: IsValidPath(k.key)
377+
requires exists x :: x in data && x.key == HeaderPath
378+
requires exists x :: x in data && x.key == FooterPath
354379
requires AuthListHasNoDuplicates(data)
355380
ensures CanonAuthMatchesAuthList(tableName, data, ret)
356381
{
@@ -379,6 +404,7 @@ module Canonize {
379404
function method {:opaque} CryptoToCanonCrypto(tableName : GoodString, data : CryptoList) : (ret : CanonCryptoList)
380405
requires forall k <- data :: IsValidPath(k.key)
381406
requires CryptoListHasNoDuplicates(data)
407+
requires !exists x | x in data :: x.key in HeaderPaths
382408
ensures CanonCryptoMatchesCryptoList(tableName, data, ret)
383409
{
384410
reveal CanonCryptoMatchesCryptoList();
@@ -448,7 +474,7 @@ module Canonize {
448474
assert (forall k <- canonSorted :: IsValidPath(k.origKey));
449475
assert (forall k <- canonSorted :: IsCanonPath(tableName, k.origKey, k.key));
450476
assert CanonAuthListHasNoDuplicates(canonSorted);
451-
assume {:axiom} CanonAuthMatchesAuthList(tableName, data, canonSorted);
477+
assert CanonAuthMatchesAuthList(tableName, data, canonSorted);
452478

453479
canonSorted
454480
}
@@ -488,7 +514,7 @@ module Canonize {
488514
assert (forall k <- canonSorted :: IsValidPath(k.origKey));
489515
assert (forall k <- canonSorted :: IsCanonPath(tableName, k.origKey, k.key));
490516
assert CanonCryptoListHasNoDuplicates(canonSorted);
491-
assume {:axiom} CanonCryptoMatchesCryptoList(tableName, data, canonSorted);
517+
assert CanonCryptoMatchesCryptoList(tableName, data, canonSorted);
492518

493519
canonSorted
494520
}
@@ -568,11 +594,14 @@ module Canonize {
568594
function method {:opaque} ForDecrypt(tableName : GoodString, data : AuthList, legend: Header.Legend)
569595
: (ret : Result<CanonCryptoList, Error>)
570596
requires AuthListHasNoDuplicates(data)
597+
requires exists x :: x in data && x.key == HeaderPath
598+
requires exists x :: x in data && x.key == FooterPath
571599
ensures ret.Success? ==>
572600
&& CanonCryptoMatchesAuthList(tableName, data, ret.value)
573601
&& IsCryptoSorted(ret.value)
574602
{
575-
:- Need(forall k <- data :: IsValidPath(k.key), E("Invalid Paths"));
603+
reveal IsValidPath();
604+
:- Need(forall k <- data :: Paths.ValidPath(k.key), E("Invalid Paths"));
576605
var canonList := AuthToCanonAuth(tableName, data);
577606
var canonSorted := AuthSort(canonList, tableName, data);
578607
DoResolveLegend(canonSorted, legend, tableName, data)
@@ -598,15 +627,71 @@ module Canonize {
598627
[newItem] + UnCanon(input[1..])
599628
}
600629

630+
/*
631+
predicate method SameUnCanon(x : CanonCryptoItem, y : CryptoItem)
632+
&& x.origKey == y.key
633+
&& x.data == y.data
634+
&& x.action == y.action
635+
*/
636+
637+
lemma SameUnCanonUpdatedAll23()
638+
ensures forall oldVal : AuthItem, x : CanonCryptoItem, y : CryptoItem ::
639+
SameUnCanon(x, y) && Updated2(oldVal, x, DoDecrypt) ==> Updated3(oldVal, y, DoDecrypt)
640+
{}
641+
642+
lemma SameUnCanonUpdatedAll32()
643+
ensures forall oldVal : AuthItem, x : CryptoItem, y : CanonCryptoItem ::
644+
SameUnCanon(y, x) && Updated3(oldVal, x, DoDecrypt) ==> Updated2(oldVal, y, DoDecrypt)
645+
{}
646+
647+
// predicate Updated2(oldVal : AuthItem, newVal : CanonCryptoItem, mode : EncryptionSelector)
648+
// predicate Updated3(oldVal : AuthItem, newVal : CryptoItem, mode : EncryptionSelector)
649+
650+
lemma AuthUpdatedCryptoMaps(origData : AuthList, input : CanonCryptoList, output : CryptoList)
651+
requires |input| == |output|
652+
requires forall k <- origData :: AuthUpdatedCanonCrypto(k, input)
653+
requires forall i | 0 <= i < |input| :: SameUnCanon(input[i], output[i])
654+
ensures forall k <- origData :: AuthUpdatedCrypto(k, output)
655+
{
656+
reveal AuthUpdatedCanonCrypto();
657+
reveal AuthUpdatedCrypto();
658+
assert forall k <- origData :: exists x :: x in output && Updated3(k, x, DoDecrypt) by {
659+
SameUnCanonUpdatedAll23();
660+
}
661+
}
662+
663+
lemma CryptoUpdatedAuthMaps(origData : AuthList, input : CanonCryptoList, output : CryptoList)
664+
requires |input| == |output|
665+
requires forall k <- input :: CanonCryptoUpdatedAuth(k, origData)
666+
requires forall i | 0 <= i < |input| :: SameUnCanon(input[i], output[i])
667+
ensures forall k <- output :: CryptoUpdatedAuth(k, origData)
668+
{
669+
reveal CanonCryptoUpdatedAuth();
670+
reveal CryptoUpdatedAuth();
671+
assume {:axiom} forall k <- output :: exists x :: x in origData && Updated3(x, k, DoDecrypt);
672+
// I don't know why this same trick doesn't work here.
673+
// by {
674+
// assert forall k <- input :: exists x :: x in origData && Updated2(x, k, DoDecrypt);
675+
// SameUnCanonUpdatedAll23();
676+
// }
677+
}
678+
601679
function method UnCanonDecrypt(input : CanonCryptoList, ghost tableName : GoodString, ghost origData : AuthList)
602680
: (ret : CryptoList)
603681
requires CanonCryptoUpdatedAuthList(tableName, origData, input)
604682
ensures CryptoUpdatedAuthList(origData, ret)
605683
{
606684
reveal CanonCryptoUpdatedAuthList();
607685
reveal CryptoUpdatedAuthList();
686+
687+
608688
var results := UnCanon(input);
609-
assume {:axiom} CryptoUpdatedAuthList(origData, results);
689+
assert (forall k <- origData :: AuthUpdatedCrypto(k, results)) by {
690+
AuthUpdatedCryptoMaps(origData, input, results);
691+
}
692+
assert (forall k <- results :: CryptoUpdatedAuth(k, origData)) by {
693+
CryptoUpdatedAuthMaps(origData, input, results);
694+
}
610695
results
611696
}
612697

@@ -617,28 +702,29 @@ module Canonize {
617702
{
618703
reveal CanonCryptoUpdatedCryptoList();
619704
reveal CryptoUpdatedCryptoList();
705+
620706
var results := UnCanon(input);
621-
assume {:axiom} CryptoUpdatedCryptoList(origData, results);
707+
assume {:axiom} (forall k <- origData :: CryptoUpdatedNewCrypto(k, results));
708+
assume {:axiom} (forall k <- results :: NewCryptoUpdatedCrypto(k, origData));
622709
results
623710
}
624711

625712
predicate {:opaque} EncryptPathFinal(origData : CryptoList, finalData : CryptoList)
626713
{
627714
&& |finalData| == |origData| + 2
628-
&& CryptoUpdatedCryptoList(origData, finalData[..(|finalData|-2)])
715+
&& CryptoUpdatedCryptoListHeader(origData, finalData[..(|finalData|-2)])
629716
&& finalData[|finalData|-2].key == HeaderPath
630717
&& finalData[|finalData|-1].key == FooterPath
631718
}
632719

633720
function method AddHeaders(input : CryptoList, headerData : StructuredDataTerminal, footerData : StructuredDataTerminal, ghost origData : CryptoList)
634721
: (ret : CryptoList)
635722
requires CryptoUpdatedCryptoList(origData, input)
636-
// requires !exists x :: x in input && x.key == HeaderPath
637-
// requires !exists x :: x in input && x.key == FooterPath
638723
ensures EncryptPathFinal(origData, ret)
639724
{
640725
reveal EncryptPathFinal();
641726
reveal CryptoUpdatedCryptoList();
727+
reveal CryptoUpdatedCryptoListHeader();
642728
var headItem := Types.CryptoItem(key := HeaderPath, data := headerData, action := DO_NOTHING);
643729
var footItem := Types.CryptoItem(key := FooterPath, data := footerData, action := DO_NOTHING);
644730
var largeResult := input + [headItem, footItem];
@@ -647,7 +733,6 @@ module Canonize {
647733

648734
predicate {:opaque} DecryptPathFinal(origData : AuthList, finalData : CryptoList)
649735
{
650-
&& |finalData| == |origData| - 2
651736
&& (!exists x :: x in finalData && x.key == HeaderPath)
652737
&& (!exists x :: x in finalData && x.key == FooterPath)
653738
&& (forall k <- origData :: (k.key in [HeaderPath, FooterPath]) || AuthUpdatedCrypto(k, finalData))
@@ -672,16 +757,14 @@ module Canonize {
672757
function method RemoveHeaders(input : CryptoList, ghost origData : AuthList)
673758
: (ret : CryptoList)
674759
requires CryptoUpdatedAuthList(origData, input)
675-
// requires exists x :: x in input && x.key == HeaderPath
676-
// requires exists x :: x in input && x.key == FooterPath
677760

678761
ensures DecryptPathFinal(origData, ret)
679762
{
680763
reveal CryptoUpdatedAuthList();
681764
reveal DecryptPathFinal();
765+
reveal AuthUpdatedCrypto();
682766
var finalData := RemoveHeaderPaths(input);
683-
assume {:axiom} |finalData| == |origData| - 2;
684-
assume {:axiom} forall k <- origData :: (k.key in [HeaderPath, FooterPath]) || AuthUpdatedCrypto(k, finalData);
767+
assert forall k <- origData :: (k.key in [HeaderPath, FooterPath]) || AuthUpdatedCrypto(k, finalData);
685768
finalData
686769
}
687770
}

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

+32-2
Original file line numberDiff line numberDiff line change
@@ -130,6 +130,19 @@ module StructuredEncryptionCrypt {
130130
return commitKey.MapFailure(e => AwsCryptographyPrimitives(e));
131131
}
132132

133+
lemma EncryptMaintains(tableName : GoodString, origData : CryptoList, data : CanonCryptoList, finalData : CanonCryptoList)
134+
requires CanonCryptoMatchesCryptoList(tableName, origData, data)
135+
requires |finalData| == |data|
136+
requires (forall i | 0 <= i < |data| :: Updated(data[i], finalData[i], DoEncrypt))
137+
ensures CanonCryptoUpdatedCryptoList(tableName, origData, finalData)
138+
{
139+
reveal CanonCryptoMatchesCryptoList();
140+
reveal CanonCryptoUpdatedCryptoList();
141+
142+
assume {:axiom} (forall k <- origData :: CryptoUpdatedCanonCrypto(k, finalData));
143+
assume {:axiom} (forall k <- finalData :: CanonCryptoUpdatedCrypto(k, origData));
144+
}
145+
133146
// Encrypt a StructuredDataMap
134147
method Encrypt(
135148
client: Primitives.AtomicPrimitivesClient,
@@ -156,10 +169,25 @@ module StructuredEncryptionCrypt {
156169
{
157170
reveal CanonCryptoMatchesCryptoList();
158171
var result :- Crypt(DoEncrypt, client, alg, key, head, data);
159-
assume {:axiom} CanonCryptoUpdatedCryptoList(tableName, origData, result);
172+
assert CanonCryptoUpdatedCryptoList(tableName, origData, result) by {
173+
EncryptMaintains(tableName, origData, data, result);
174+
}
160175
return Success(result);
161176
}
162177

178+
lemma DecryptMaintains(tableName : GoodString, origData : AuthList, data : CanonCryptoList, finalData : CanonCryptoList)
179+
requires CanonCryptoMatchesAuthList(tableName, origData, data)
180+
requires |finalData| == |data|
181+
requires (forall i | 0 <= i < |data| :: Updated(data[i], finalData[i], DoDecrypt))
182+
ensures CanonCryptoUpdatedAuthList(tableName, origData, finalData)
183+
{
184+
reveal CanonCryptoMatchesAuthList();
185+
reveal CanonCryptoUpdatedAuthList();
186+
187+
assume {:axiom} (forall k <- origData :: AuthUpdatedCanonCrypto(k, finalData));
188+
assume {:axiom} (forall k <- finalData :: CanonCryptoUpdatedAuth(k, origData));
189+
}
190+
163191
// Decrypt a StructuredDataMap
164192
method Decrypt(
165193
client: Primitives.AtomicPrimitivesClient,
@@ -185,7 +213,9 @@ module StructuredEncryptionCrypt {
185213
{
186214
reveal CanonCryptoMatchesAuthList();
187215
var result :- Crypt(DoDecrypt, client, alg, key, head, data);
188-
assume {:axiom} CanonCryptoUpdatedAuthList(tableName, origData, result);
216+
assert CanonCryptoUpdatedAuthList(tableName, origData, result) by {
217+
DecryptMaintains(tableName, origData, data, result);
218+
}
189219
return Success(result);
190220
}
191221

0 commit comments

Comments
 (0)