Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit 1ce388f

Browse files
ajewellamzajewellamz
committedMay 14, 2024··
feat: improve verification
1 parent a70a569 commit 1ce388f

File tree

7 files changed

+1259
-458
lines changed

7 files changed

+1259
-458
lines changed
 

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

Lines changed: 262 additions & 389 deletions
Large diffs are not rendered by default.

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

Lines changed: 687 additions & 0 deletions
Large diffs are not rendered by default.

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

Lines changed: 51 additions & 60 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,8 @@ include "../../../../submodules/MaterialProviders/AwsCryptographyPrimitives/src/
66

77
include "Header.dfy"
88
include "Util.dfy"
9+
include "SortCanon.dfy"
10+
include "Canonize.dfy"
911

1012
module StructuredEncryptionCrypt {
1113
import opened Wrappers
@@ -23,6 +25,9 @@ module StructuredEncryptionCrypt {
2325
import HKDF
2426
import AesKdfCtr
2527
import Seq
28+
import SortCanon
29+
// import Relations
30+
import opened Canonize
2631

2732
function method FieldKey(HKDFOutput : Bytes, offset : uint32)
2833
: (ret : Result<Bytes, Error>)
@@ -125,77 +130,34 @@ module StructuredEncryptionCrypt {
125130
return commitKey.MapFailure(e => AwsCryptographyPrimitives(e));
126131
}
127132

128-
datatype EncryptionSelector = DoEncrypt | DoDecrypt
129-
130-
// Updated return true if the given item has been updated properly for the given operation.
131-
// Updated2..Update5 do exactly the same thing, but with different data types.
132-
predicate Updated(oldVal : CanonCryptoItem, newVal : CanonCryptoItem, mode : EncryptionSelector)
133-
{
134-
&& oldVal.key == newVal.key
135-
&& oldVal.origKey == newVal.origKey
136-
&& oldVal.action == newVal.action
137-
&& (newVal.action != ENCRYPT_AND_SIGN <==> oldVal.data == newVal.data)
138-
&& (newVal.action == ENCRYPT_AND_SIGN <==> oldVal.data != newVal.data)
139-
&& (mode == DoEncrypt ==> (newVal.action == ENCRYPT_AND_SIGN ==> newVal.data.typeId == BYTES_TYPE_ID))
140-
&& (mode == DoDecrypt ==> (newVal.action == ENCRYPT_AND_SIGN ==> |oldVal.data.value| >= 2 && newVal.data.typeId == oldVal.data.value[..2]))
141-
}
142-
143-
predicate Updated2(oldVal : AuthItem, newVal : CanonCryptoItem, mode : EncryptionSelector)
144-
{
145-
&& oldVal.key == newVal.origKey
146-
&& (newVal.action != ENCRYPT_AND_SIGN <==> oldVal.data == newVal.data)
147-
&& (newVal.action == ENCRYPT_AND_SIGN <==> oldVal.data != newVal.data)
148-
&& (mode == DoEncrypt ==> (newVal.action == ENCRYPT_AND_SIGN ==> newVal.data.typeId == BYTES_TYPE_ID))
149-
&& (mode == DoDecrypt ==> (newVal.action == ENCRYPT_AND_SIGN ==> |oldVal.data.value| >= 2 && newVal.data.typeId == oldVal.data.value[..2]))
150-
}
151-
152-
predicate Updated3(oldVal : AuthItem, newVal : CryptoItem, mode : EncryptionSelector)
153-
{
154-
&& oldVal.key == newVal.key
155-
&& (newVal.action != ENCRYPT_AND_SIGN <==> oldVal.data == newVal.data)
156-
&& (newVal.action == ENCRYPT_AND_SIGN <==> oldVal.data != newVal.data)
157-
&& (mode == DoEncrypt ==> (newVal.action == ENCRYPT_AND_SIGN ==> newVal.data.typeId == BYTES_TYPE_ID))
158-
&& (mode == DoDecrypt ==> (newVal.action == ENCRYPT_AND_SIGN ==> |oldVal.data.value| >= 2 && newVal.data.typeId == oldVal.data.value[..2]))
159-
}
160-
161-
predicate Updated4(oldVal : CryptoItem, newVal : CryptoItem, mode : EncryptionSelector)
162-
{
163-
&& oldVal.key == newVal.key
164-
&& oldVal.action == newVal.action
165-
&& (newVal.action != ENCRYPT_AND_SIGN <==> oldVal.data == newVal.data)
166-
&& (newVal.action == ENCRYPT_AND_SIGN <==> oldVal.data != newVal.data)
167-
&& (mode == DoEncrypt ==> (newVal.action == ENCRYPT_AND_SIGN ==> newVal.data.typeId == BYTES_TYPE_ID))
168-
&& (mode == DoDecrypt ==> (newVal.action == ENCRYPT_AND_SIGN ==> |oldVal.data.value| >= 2 && newVal.data.typeId == oldVal.data.value[..2]))
169-
}
170-
171-
predicate Updated5(oldVal : CryptoItem, newVal : CanonCryptoItem, mode : EncryptionSelector)
172-
{
173-
&& oldVal.key == newVal.origKey
174-
&& oldVal.action == newVal.action
175-
&& (newVal.action != ENCRYPT_AND_SIGN <==> oldVal.data == newVal.data)
176-
&& (newVal.action == ENCRYPT_AND_SIGN <==> oldVal.data != newVal.data)
177-
&& (mode == DoEncrypt ==> (newVal.action == ENCRYPT_AND_SIGN ==> newVal.data.typeId == BYTES_TYPE_ID))
178-
&& (mode == DoDecrypt ==> (newVal.action == ENCRYPT_AND_SIGN ==> |oldVal.data.value| >= 2 && newVal.data.typeId == oldVal.data.value[..2]))
179-
}
180-
181133
// Encrypt a StructuredDataMap
182134
method Encrypt(
183135
client: Primitives.AtomicPrimitivesClient,
184136
alg : CMP.AlgorithmSuiteInfo,
185137
key : Key,
186138
head : Header.PartialHeader,
187-
data : CanonCryptoList)
139+
data : CanonCryptoList,
140+
ghost tableName : GoodString,
141+
ghost origData : CryptoList)
188142
returns (ret : Result<CanonCryptoList, Error>)
189143
requires ValidSuite(alg)
144+
requires IsCryptoSorted(data)
145+
requires CanonCryptoMatchesCryptoList(tableName, origData, data)
190146

191147
modifies client.Modifies
192148
requires client.ValidState()
193149
ensures client.ValidState()
194150
ensures ret.Success? ==>
195151
&& |ret.value| == |data|
196152
&& (forall i | 0 <= i < |data| :: Updated(data[i], ret.value[i], DoEncrypt))
153+
&& CanonCryptoListHasNoDuplicates(ret.value)
154+
&& IsCryptoSorted(ret.value)
155+
&& CanonCryptoUpdatedCryptoList(tableName, origData, ret.value)
197156
{
198-
ret := Crypt(DoEncrypt, client, alg, key, head, data);
157+
reveal CanonCryptoMatchesCryptoList();
158+
var result :- Crypt(DoEncrypt, client, alg, key, head, data);
159+
assume {:axiom} CanonCryptoUpdatedCryptoList(tableName, origData, result);
160+
return Success(result);
199161
}
200162

201163
// Decrypt a StructuredDataMap
@@ -204,18 +166,38 @@ module StructuredEncryptionCrypt {
204166
alg : CMP.AlgorithmSuiteInfo,
205167
key : Key,
206168
head : Header.PartialHeader,
207-
data : CanonCryptoList)
169+
data : CanonCryptoList,
170+
ghost tableName : GoodString,
171+
ghost origData : AuthList)
208172
returns (ret : Result<CanonCryptoList, Error>)
209173
requires ValidSuite(alg)
174+
requires IsCryptoSorted(data)
175+
requires CanonCryptoMatchesAuthList(tableName, origData, data)
210176

211177
modifies client.Modifies
212178
requires client.ValidState()
213179
ensures client.ValidState()
214180
ensures ret.Success? ==>
215181
&& |ret.value| == |data|
216-
&& forall i | 0 <= i < |data| :: Updated(data[i], ret.value[i], DoDecrypt)
182+
&& (forall i | 0 <= i < |data| :: Updated(data[i], ret.value[i], DoDecrypt))
183+
&& IsCryptoSorted(ret.value)
184+
&& CanonCryptoUpdatedAuthList(tableName, origData, ret.value)
217185
{
218-
ret := Crypt(DoDecrypt, client, alg, key, head, data);
186+
reveal CanonCryptoMatchesAuthList();
187+
var result :- Crypt(DoDecrypt, client, alg, key, head, data);
188+
assume {:axiom} CanonCryptoUpdatedAuthList(tableName, origData, result);
189+
return Success(result);
190+
}
191+
192+
lemma MaintainSorted(data : CanonCryptoList, result : CanonCryptoList, mode : EncryptionSelector)
193+
requires IsCryptoSorted(data)
194+
requires |result| == |data|
195+
requires forall i | 0 <= i < |data| :: Updated(data[i], result[i], mode)
196+
ensures IsCryptoSorted(result)
197+
{
198+
reveal IsCryptoSorted();
199+
assert forall i | 0 <= i < |data| :: data[i].key == result[i].key;
200+
SortCanon.SortedIsSorted(data, result);
219201
}
220202

221203
// Encrypt or Decrypt a StructuredDataMap
@@ -228,6 +210,8 @@ module StructuredEncryptionCrypt {
228210
data : CanonCryptoList)
229211
returns (ret : Result<CanonCryptoList, Error>)
230212
requires ValidSuite(alg)
213+
requires CanonCryptoListHasNoDuplicates(data)
214+
requires IsCryptoSorted(data)
231215

232216
ensures ret.Success? ==>
233217
//= specification/structured-encryption/encrypt-path-structure.md#calculate-cipherkey-and-nonce
@@ -263,6 +247,8 @@ module StructuredEncryptionCrypt {
263247
ensures ret.Success? ==>
264248
&& |ret.value| == |data|
265249
&& (forall i | 0 <= i < |data| :: Updated(data[i], ret.value[i], mode))
250+
&& CanonCryptoListHasNoDuplicates(ret.value)
251+
&& IsCryptoSorted(ret.value)
266252
{
267253
//= specification/structured-encryption/encrypt-path-structure.md#calculate-cipherkey-and-nonce
268254
//# The `FieldRootKey` MUST be generated with the plaintext data key in the encryption materials
@@ -283,8 +269,13 @@ module StructuredEncryptionCrypt {
283269
//# The calculated Field Root MUST have length equal to the
284270
//# [algorithm suite's encryption key length](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/algorithm-suites.md#algorithm-suites-encryption-settings).
285271
assert |fieldRootKey| == AlgorithmSuites.GetEncryptKeyLength(alg) as int;
286-
var result := CryptList(mode, client, alg, fieldRootKey, data);
287-
return result;
272+
var result :- CryptList(mode, client, alg, fieldRootKey, data);
273+
274+
assert IsCryptoSorted(result) by {
275+
MaintainSorted(data, result, mode);
276+
}
277+
278+
return Success(result);
288279
}
289280

290281
// Encrypt or Decrypt each entry in keys, putting results in output

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

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,12 @@ module StructuredEncryptionPaths {
3434
[member(StructureSegment(key := x))]
3535
}
3636

37+
lemma StringToUniPathUnique()
38+
ensures forall x : string, y : string
39+
:: x != y ==> StringToUniPath(x) != StringToUniPath(y)
40+
{
41+
}
42+
3743
function method UniPathToString(x : Path) : Result<string, Error>
3844
requires |x| == 1
3945
{

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

Lines changed: 103 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -5,13 +5,16 @@ include "../Model/AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.dfy"
55
include "Util.dfy"
66

77
module SortCanon {
8-
export provides
8+
export
9+
provides
910
AuthSort,
1011
CryptoSort,
1112
AuthBelow,
1213
CryptoBelow,
1314
StructuredEncryptionUtil,
14-
Relations
15+
Relations,
16+
AuthSortIsCryptoSort,
17+
SortedIsSorted
1518

1619
import opened Wrappers
1720
import opened StandardLibrary
@@ -28,6 +31,20 @@ module SortCanon {
2831
Below(x.key, y.key)
2932
}
3033

34+
lemma SameBelow2(x1 : CanonAuthItem, x2 : CanonAuthItem, y1 : CanonCryptoItem, y2 : CanonCryptoItem)
35+
requires x1.key == y1.key
36+
requires x2.key == y2.key
37+
ensures AuthBelow(x1, x2) == CryptoBelow(y1, y2)
38+
{}
39+
40+
lemma SameBelow()
41+
ensures forall x1 : CanonAuthItem, x2 : CanonAuthItem, y1 : CanonCryptoItem, y2 : CanonCryptoItem
42+
| x1.key == y1.key && x2.key == y2.key
43+
:: AuthBelow(x1, x2) == CryptoBelow(y1, y2)
44+
{
45+
46+
}
47+
3148
lemma AuthBelowIsReflexive(x: CanonAuthItem)
3249
ensures AuthBelow(x, x)
3350
{
@@ -185,21 +202,101 @@ module SortCanon {
185202
{
186203
}
187204

188-
function method AuthSort(x : seq<CanonAuthItem>) : (result : seq<CanonAuthItem>)
205+
lemma AuthSortIsCryptoSort(x : CanonAuthList, y : CanonCryptoList)
206+
requires SortedBy(x, AuthBelow)
207+
requires |x| == |y|
208+
requires forall i | 0 <= i < |x| :: x[i].key == y[i].key
209+
ensures SortedBy(y, CryptoBelow)
210+
{}
211+
212+
lemma SortedIsSorted(x : CanonCryptoList, y : CanonCryptoList)
213+
requires SortedBy(x, CryptoBelow)
214+
requires |x| == |y|
215+
requires forall i | 0 <= i < |x| :: x[i].key == y[i].key
216+
ensures SortedBy(y, CryptoBelow)
217+
{}
218+
219+
220+
function method AuthSort(x : CanonAuthList) : (result : CanonAuthList)
221+
requires CanonAuthListHasNoDuplicates(x)
189222
ensures multiset(x) == multiset(result)
190223
ensures SortedBy(result, AuthBelow)
224+
ensures CanonAuthListHasNoDuplicates(result)
191225
{
192226
AuthBelowIsTotal();
193-
MergeSortBy(x, AuthBelow)
227+
var ret := MergeSortBy(x, AuthBelow);
228+
CanonAuthListMultiNoDup(x, ret);
229+
assert CanonAuthListHasNoDuplicates(ret);
230+
ret
194231
}
195232

196-
function method CryptoSort(x : seq<CanonCryptoItem>) : (result : seq<CanonCryptoItem>)
233+
function method CryptoSort(x : CanonCryptoList) : (result : CanonCryptoList)
234+
requires CanonCryptoListHasNoDuplicates(x)
197235
ensures multiset(x) == multiset(result)
236+
ensures multiset(result) == multiset(x)
198237
ensures SortedBy(result, CryptoBelow)
238+
ensures CanonCryptoListHasNoDuplicates(result)
199239
{
200240
CryptoBelowIsTotal();
201-
MergeSortBy(x, CryptoBelow)
241+
var ret := MergeSortBy(x, CryptoBelow);
242+
CanonCryptoListMultiNoDup(x, ret);
243+
assert CanonCryptoListHasNoDuplicates(ret);
244+
ret
202245
}
203246

247+
lemma {:axiom} CanonCryptoListMultiNoDup(a: CanonCryptoList, b: CanonCryptoList)
248+
requires CanonCryptoListHasNoDuplicates(a) && multiset(a) == multiset(b)
249+
ensures CanonCryptoListHasNoDuplicates(b)
250+
251+
lemma {:axiom} CanonAuthListMultiNoDup(a: CanonAuthList, b: CanonAuthList)
252+
requires CanonAuthListHasNoDuplicates(a) && multiset(a) == multiset(b)
253+
ensures CanonAuthListHasNoDuplicates(b)
204254

255+
/*
256+
lemma Foo(a : CanonCryptoList)
257+
ensures CanonCryptoListHasNoDuplicates(a)
258+
<==>
259+
(forall t:CanonCryptoItem :: multiset(a)[t] <= 1)
260+
&& (forall t0 : CanonCryptoItem, t1 : CanonCryptoItem <- multiset(a) | t0.origKey == t1.origKey :: t0==t1)
261+
262+
263+
lemma AndyNeed2(a: CanonCryptoList, b: CanonCryptoList)
264+
requires CanonCryptoListHasNoDuplicates(a) && multiset(a) == multiset(b)
265+
ensures CanonCryptoListHasNoDuplicates(b)
266+
{
267+
Foo(a);
268+
Foo(b);
269+
}
270+
271+
lemma {:vcs_split_on_every_assert} AndyNeed(a: CanonCryptoList, b: CanonCryptoList)
272+
requires CanonCryptoListHasNoDuplicates(a) && multiset(a) == multiset(b)
273+
ensures CanonCryptoListHasNoDuplicates(b)
274+
{
275+
if a == [] {
276+
assert multiset(b) == multiset{};
277+
assert b == [] by {
278+
if b != [] {
279+
var bElem := b[0];
280+
assert bElem in multiset(b);
281+
}
282+
}
283+
assert CanonCryptoListHasNoDuplicates(b);
284+
} else {
285+
var ap := a[1..];
286+
assert exists i | 0 <= i < |b| :: b[i] == a[0] by { // TODO
287+
assume {:axiom} exists i | 0 <= i < |b| :: b[i] == a[0];
288+
}
289+
var i :| 0 <= i < |b| && b[i] == a[0];
290+
var bp := b[0..i] + b[i+1..];
291+
assert multiset(ap) == multiset(bp) by {
292+
assume {:axiom} multiset(ap) == multiset(bp);
293+
}
294+
AndyNeed(ap, bp);
295+
assert CanonCryptoListHasNoDuplicates(bp);
296+
assert CanonCryptoListHasNoDuplicates(b) by {
297+
assume {:axiom} CanonCryptoListHasNoDuplicates(b);
298+
}
299+
}
300+
}
301+
*/
205302
}

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

Lines changed: 146 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ module StructuredEncryptionUtil {
1515
import AlgorithmSuites
1616
import SortedSets
1717
import Base64
18+
import opened Seq
1819

1920
// all attributes with this prefix reserved for the implementation
2021
const ReservedPrefix := "aws_dbe_"
@@ -57,6 +58,60 @@ module StructuredEncryptionUtil {
5758
type CanonCryptoList = seq<CanonCryptoItem>
5859
type CanonAuthList = seq<CanonAuthItem>
5960

61+
function method CryptoListToSet(xs: CryptoList) : (ret : set<Path>)
62+
ensures |xs| == 0 ==> |ret| == 0
63+
ensures |xs| == 1 ==> ret == {xs[0].key}
64+
ensures |xs| == 1 ==> |ret| == 1
65+
{
66+
set k <- xs :: k.key
67+
}
68+
69+
function method CanonCryptoListToSet(xs: CanonCryptoList) : (ret : set<Path>)
70+
ensures |xs| == 0 ==> |ret| == 0
71+
ensures |xs| == 1 ==> ret == {xs[0].origKey}
72+
ensures |xs| == 1 ==> |ret| == 1
73+
{
74+
set k <- xs :: k.origKey
75+
}
76+
77+
function method AuthListToSet(xs: AuthList) : (ret : set<Path>)
78+
ensures |xs| == 0 ==> |ret| == 0
79+
ensures |xs| == 1 ==> ret == {xs[0].key}
80+
ensures |xs| == 1 ==> |ret| == 1
81+
{
82+
set k <- xs :: k.key
83+
}
84+
85+
predicate method CryptoListHasNoDuplicatesFromSet(xs: CryptoList)
86+
{
87+
|CryptoListToSet(xs)| == |xs|
88+
}
89+
90+
predicate method AuthListHasNoDuplicatesFromSet(xs: AuthList)
91+
{
92+
|AuthListToSet(xs)| == |xs|
93+
}
94+
95+
predicate CryptoListHasNoDuplicates(xs: CryptoList)
96+
{
97+
forall i, j :: 0 <= i < j < |xs| ==> xs[i].key != xs[j].key
98+
}
99+
100+
predicate AuthListHasNoDuplicates(xs: AuthList)
101+
{
102+
forall i, j :: 0 <= i < j < |xs| ==> xs[i].key != xs[j].key
103+
}
104+
105+
predicate CanonCryptoListHasNoDuplicates(xs: CanonCryptoList)
106+
{
107+
forall i, j :: 0 <= i < j < |xs| ==> xs[i].origKey != xs[j].origKey
108+
}
109+
110+
predicate CanonAuthListHasNoDuplicates(xs: CanonAuthList)
111+
{
112+
forall i, j :: 0 <= i < j < |xs| ==> xs[i].origKey != xs[j].origKey
113+
}
114+
60115
//= specification/structured-encryption/encrypt-path-structure.md#header-field
61116
//= type=implication
62117
//# The Header Field name MUST be `aws_dbe_head`
@@ -249,4 +304,95 @@ module StructuredEncryptionUtil {
249304
Success(StructuredDataTerminal(value := serializedValue, typeId := typeId))
250305
}
251306

307+
lemma CryptoListNoDupFromMap(xs: seq<CryptoItem>)
308+
requires HasNoDuplicates(Map((x: CryptoItem) => x.key, xs))
309+
ensures CryptoListHasNoDuplicates(xs)
310+
{
311+
var ys := Map((x: CryptoItem) => x.key, xs);
312+
assert forall i, j | 0 <= i < j < |xs| :: ys[i] != ys[j] by {
313+
reveal HasNoDuplicates();
314+
}
315+
assert forall i | 0 <= i < |xs| :: ys[i] == xs[i].key;
316+
}
317+
318+
lemma AuthListNoDupFromMap(xs: seq<AuthItem>)
319+
requires HasNoDuplicates(Map((x: AuthItem) => x.key, xs))
320+
ensures AuthListHasNoDuplicates(xs)
321+
{
322+
var ys := Map((x: AuthItem) => x.key, xs);
323+
assert forall i, j | 0 <= i < j < |xs| :: ys[i] != ys[j] by {
324+
reveal HasNoDuplicates();
325+
}
326+
assert forall i | 0 <= i < |xs| :: ys[i] == xs[i].key;
327+
}
328+
329+
lemma CryptoListCard(xs: seq<CryptoItem>)
330+
ensures |ToSet(Map((x: CryptoItem) => x.key, xs))| == |CryptoListToSet(xs)|
331+
{
332+
reveal ToSet();
333+
var ys := Map((x: CryptoItem) => x.key, xs);
334+
forall x ensures x in ToSet(ys) <==> x in CryptoListToSet(xs) {
335+
assert x in ToSet(ys) ==> x in CryptoListToSet(xs);
336+
assert x in CryptoListToSet(xs) ==> x in ToSet(ys) by {
337+
if x in CryptoListToSet(xs) {
338+
var i :| 0 <= i < |xs| && xs[i].key == x;
339+
assert ys[i] == x by {
340+
calc == {
341+
ys[i];
342+
Map((x: CryptoItem) => x.key, xs)[i];
343+
xs[i].key;
344+
x;
345+
}
346+
}
347+
} else {}
348+
}
349+
}
350+
assert ToSet(ys) == CryptoListToSet(xs);
351+
}
352+
353+
lemma AuthListCard(xs: seq<AuthItem>)
354+
ensures |ToSet(Map((x: AuthItem) => x.key, xs))| == |AuthListToSet(xs)|
355+
{
356+
reveal ToSet();
357+
var ys := Map((x: AuthItem) => x.key, xs);
358+
forall x ensures x in ToSet(ys) <==> x in AuthListToSet(xs) {
359+
assert x in ToSet(ys) ==> x in AuthListToSet(xs);
360+
assert x in AuthListToSet(xs) ==> x in ToSet(ys) by {
361+
if x in AuthListToSet(xs) {
362+
var i :| 0 <= i < |xs| && xs[i].key == x;
363+
assert ys[i] == x by {
364+
calc == {
365+
ys[i];
366+
Map((x: AuthItem) => x.key, xs)[i];
367+
xs[i].key;
368+
x;
369+
}
370+
}
371+
} else {}
372+
}
373+
}
374+
assert ToSet(ys) == AuthListToSet(xs);
375+
}
376+
377+
lemma SetSizeImpliesCryptoListHasNoDuplicates(xs: seq<CryptoItem>)
378+
requires CryptoListHasNoDuplicatesFromSet(xs)
379+
ensures CryptoListHasNoDuplicates(xs)
380+
{
381+
var ys := Map((x: CryptoItem) => x.key, xs);
382+
CryptoListCard(xs);
383+
LemmaNoDuplicatesCardinalityOfSet(ys);
384+
CryptoListNoDupFromMap(xs);
385+
}
386+
387+
lemma SetSizeImpliesAuthListHasNoDuplicates(xs: seq<AuthItem>)
388+
requires AuthListHasNoDuplicatesFromSet(xs)
389+
ensures AuthListHasNoDuplicates(xs)
390+
{
391+
var ys := Map((x: AuthItem) => x.key, xs);
392+
AuthListCard(xs);
393+
LemmaNoDuplicatesCardinalityOfSet(ys);
394+
AuthListNoDupFromMap(xs);
395+
}
396+
397+
252398
}

‎DynamoDbEncryption/dafny/StructuredEncryption/test/Header.dfy

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ module TestHeader {
1919
import opened UTF8
2020
import Aws.Cryptography.Primitives
2121
import AlgorithmSuites
22+
import Canonize
2223

2324
method {:test} TestRoundTrip() {
2425
var head := PartialHeader (
@@ -136,7 +137,7 @@ module TestHeader {
136137
MakeCrypto("pqr", DO_NOTHING)
137138
];
138139
var tableName : GoodString := "name";
139-
var canonSchema :- expect OPS.CanonizeForEncrypt(tableName, schemaMap);
140+
var canonSchema :- expect Canonize.ForEncrypt(tableName, schemaMap);
140141
var legend :- expect MakeLegend(canonSchema);
141142
//= specification/structured-encryption/header.md#encrypt-legend-bytes
142143
//= type=test
@@ -158,7 +159,7 @@ module TestHeader {
158159
MakeCrypto("zzzz", DO_NOTHING)
159160
];
160161
var tableName : GoodString := "name";
161-
var canonSchema :- expect OPS.CanonizeForEncrypt(tableName, schemaMap);
162+
var canonSchema :- expect Canonize.ForEncrypt(tableName, schemaMap);
162163
var legend :- expect MakeLegend(canonSchema);
163164
//= specification/structured-encryption/header.md#encrypt-legend-bytes
164165
//= type=test
@@ -180,7 +181,7 @@ module TestHeader {
180181
MakeCrypto("aaaa", SIGN_ONLY)
181182
];
182183
var tableName : GoodString := "name";
183-
var canonSchema :- expect OPS.CanonizeForEncrypt(tableName, schemaMap);
184+
var canonSchema :- expect Canonize.ForEncrypt(tableName, schemaMap);
184185
var legend :- expect MakeLegend(canonSchema);
185186
//= specification/structured-encryption/header.md#encrypt-legend-bytes
186187
//= type=test

0 commit comments

Comments
 (0)
Please sign in to comment.