@@ -14,21 +14,16 @@ module DynamoDbGetEncryptedDataKeyDescriptionTest {
14
14
import EdkWrapping
15
15
import AlgorithmSuites
16
16
17
+ // THIS IS A TESTING RESOURCE DO NOT USE IN A PRODUCTION ENVIRONMENT
17
18
const testVersion : Version := 1
18
-
19
19
const testFlavor : Flavor := 1
20
-
21
20
const testMsgID : MessageID := [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32]
22
-
23
21
const testLegend : Legend := [0x65, 0x73]
24
-
25
22
const testEncContext : CMPEncryptionContext := map [EncodeAscii ("abc") := EncodeAscii ("def")]
26
-
27
23
const testAwsKmsDataKey := CMP. EncryptedDataKey (
28
24
keyProviderId := EncodeAscii("aws-kms") ,
29
25
keyProviderInfo := EncodeAscii ("keyproviderInfo"),
30
26
ciphertext := [1, 2, 3, 4, 5])
31
-
32
27
const testAwsKmsHDataKey := CMP. EncryptedDataKey (
33
28
keyProviderId := EncodeAscii("aws-kms-hierarchy") ,
34
29
keyProviderInfo := EncodeAscii ("keyproviderInfo"),
@@ -43,19 +38,16 @@ module DynamoDbGetEncryptedDataKeyDescriptionTest {
43
38
107, 5, 120, 20, 95, 78, 70, 2, 49, 84, 39, 50, 40, 40, 115,
44
39
114, 76, 18, 103, 84, 34, 123, 1, 125, 61, 33, 13, 18, 81,
45
40
24, 53, 53, 26, 60, 52, 85, 81, 96, 85, 72])
46
-
47
41
const testRawRsaDataKey := CMP. EncryptedDataKey (
48
42
keyProviderId := EncodeAscii("raw-rsa") ,
49
43
keyProviderInfo := [1, 2, 3, 4, 5],
50
44
ciphertext := [6, 7, 8, 9])
51
-
52
45
const testAwsKmsRsaDataKey := CMP. EncryptedDataKey (
53
46
keyProviderId := EncodeAscii("aws-kms-rsa") ,
54
47
keyProviderInfo := EncodeAscii ("keyproviderInfo"),
55
48
ciphertext := [1, 2, 3, 4, 5])
56
-
57
49
const algorithmSuite := AlgorithmSuites. DBE_ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384_SYMSIG_HMAC_SHA384
58
-
50
+
59
51
method CreatePartialHeader (version : Version , flavor : Flavor , msgID : MessageID , legend : Legend , encContext : CMPEncryptionContext , dataKeyList : CMPEncryptedDataKeyList )
60
52
returns (result: PartialHeader)
61
53
ensures result. version == version
@@ -79,24 +71,19 @@ module DynamoDbGetEncryptedDataKeyDescriptionTest {
79
71
{
80
72
var expectedHead := CreatePartialHeader (testVersion, testFlavor, testMsgID, testLegend, testEncContext, [testAwsKmsDataKey]);
81
73
var serializedHeader := expectedHead. serialize () + expectedHead. msgID;
82
-
83
74
var ddbEncResources :- expect DynamoDbEncryption. DynamoDbEncryption ();
84
-
85
75
var inputVariable: Types. GetEncryptedDataKeyDescriptionInput :=
86
76
Types. GetEncryptedDataKeyDescriptionInput (
87
77
input := Types.header(header := serializedHeader)
88
78
);
89
-
90
79
var actualDataKeyDescription := ddbEncResources. GetEncryptedDataKeyDescription (inputVariable);
91
80
92
81
expect UTF8. Decode (expectedHead.dataKeys[0].keyProviderId). Success?;
93
82
expect UTF8. Decode (expectedHead.dataKeys[0].keyProviderInfo). Success?;
94
83
expect actualDataKeyDescription. Success?;
95
84
expect |actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput| > 0;
96
-
97
85
expect |actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput| == |expectedHead. dataKeys|;
98
86
expect actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput[0]. keyProviderId == UTF8. Decode (expectedHead.dataKeys[0].keyProviderId). Extract ();
99
-
100
87
expect actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput[0]. keyProviderInfo. Some?;
101
88
expect actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput[0]. keyProviderInfo. Extract () == UTF8. Decode (expectedHead.dataKeys[0].keyProviderInfo). Extract ();
102
89
}
@@ -105,25 +92,20 @@ module DynamoDbGetEncryptedDataKeyDescriptionTest {
105
92
{
106
93
var expectedHead := CreatePartialHeader (testVersion, testFlavor, testMsgID, testLegend, testEncContext, [testAwsKmsHDataKey]);
107
94
var serializedHeader := expectedHead. serialize () + expectedHead. msgID;
108
-
109
95
var expectedBranchKeyVersion := getBranchKeyVersion (expectedHead);
110
96
var ddbEncResources :- expect DynamoDbEncryption. DynamoDbEncryption ();
111
-
112
97
var inputVariable: Types. GetEncryptedDataKeyDescriptionInput :=
113
98
Types. GetEncryptedDataKeyDescriptionInput (
114
99
input := Types.header(header := serializedHeader)
115
100
);
116
-
117
101
var actualDataKeyDescription := ddbEncResources. GetEncryptedDataKeyDescription (inputVariable);
118
102
119
103
expect UTF8. Decode (expectedHead.dataKeys[0].keyProviderId). Success?;
120
104
expect UTF8. Decode (expectedHead.dataKeys[0].keyProviderInfo). Success?;
121
105
expect actualDataKeyDescription. Success?;
122
106
expect |actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput| > 0;
123
-
124
107
expect |actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput| == |expectedHead. dataKeys|;
125
108
expect actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput[0]. keyProviderId == UTF8. Decode (expectedHead.dataKeys[0].keyProviderId). Extract ();
126
-
127
109
expect actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput[0]. keyProviderInfo. Some?;
128
110
expect actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput[0]. keyProviderInfo. Extract () == UTF8. Decode (expectedHead.dataKeys[0].keyProviderInfo). Extract ();
129
111
@@ -140,24 +122,19 @@ module DynamoDbGetEncryptedDataKeyDescriptionTest {
140
122
{
141
123
var expectedHead := CreatePartialHeader (testVersion, testFlavor, testMsgID, testLegend, testEncContext, [testRawRsaDataKey]);
142
124
var serializedHeader := expectedHead. serialize () + expectedHead. msgID;
143
-
144
125
var ddbEncResources :- expect DynamoDbEncryption. DynamoDbEncryption ();
145
-
146
126
var inputVariable: Types. GetEncryptedDataKeyDescriptionInput :=
147
127
Types. GetEncryptedDataKeyDescriptionInput (
148
128
input := Types.header(header := serializedHeader)
149
129
);
150
-
151
130
var actualDataKeyDescription := ddbEncResources. GetEncryptedDataKeyDescription (inputVariable);
152
131
153
132
expect UTF8. Decode (expectedHead.dataKeys[0].keyProviderId). Success?;
154
133
expect UTF8. Decode (expectedHead.dataKeys[0].keyProviderInfo). Success?;
155
134
expect actualDataKeyDescription. Success?;
156
135
expect |actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput| > 0;
157
-
158
136
expect |actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput| == |expectedHead. dataKeys|;
159
137
expect actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput[0]. keyProviderId == UTF8. Decode (expectedHead.dataKeys[0].keyProviderId). Extract ();
160
-
161
138
expect actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput[0]. keyProviderInfo. Some?;
162
139
expect actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput[0]. keyProviderInfo. Extract () == UTF8. Decode (expectedHead.dataKeys[0].keyProviderInfo). Extract ();
163
140
}
@@ -166,24 +143,19 @@ module DynamoDbGetEncryptedDataKeyDescriptionTest {
166
143
{
167
144
var expectedHead := CreatePartialHeader (testVersion, testFlavor, testMsgID, testLegend, testEncContext, [testAwsKmsRsaDataKey]);
168
145
var serializedHeader := expectedHead. serialize () + expectedHead. msgID;
169
-
170
146
var ddbEncResources :- expect DynamoDbEncryption. DynamoDbEncryption ();
171
-
172
147
var inputVariable: Types. GetEncryptedDataKeyDescriptionInput :=
173
148
Types. GetEncryptedDataKeyDescriptionInput (
174
149
input := Types.header(header := serializedHeader)
175
150
);
176
-
177
151
var actualDataKeyDescription := ddbEncResources. GetEncryptedDataKeyDescription (inputVariable);
178
152
179
153
expect UTF8. Decode (expectedHead.dataKeys[0].keyProviderId). Success?;
180
154
expect UTF8. Decode (expectedHead.dataKeys[0].keyProviderInfo). Success?;
181
155
expect actualDataKeyDescription. Success?;
182
156
expect |actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput| > 0;
183
-
184
157
expect |actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput| == |expectedHead. dataKeys|;
185
158
expect actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput[0]. keyProviderId == UTF8. Decode (expectedHead.dataKeys[0].keyProviderId). Extract ();
186
-
187
159
expect actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput[0]. keyProviderInfo. Some?;
188
160
expect actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput[0]. keyProviderInfo. Extract () == UTF8. Decode (expectedHead.dataKeys[0].keyProviderInfo). Extract ();
189
161
}
@@ -193,7 +165,6 @@ module DynamoDbGetEncryptedDataKeyDescriptionTest {
193
165
{
194
166
var expectedHead := CreatePartialHeader (testVersion, testFlavor, testMsgID, testLegend, testEncContext, [testAwsKmsDataKey]);
195
167
var serializedHeader := expectedHead. serialize () + expectedHead. msgID;
196
-
197
168
var attr := map ["aws_dbe_head" := ComAmazonawsDynamodbTypes. AttributeValue. B (serializedHeader)];
198
169
var ddbEncResources :- expect DynamoDbEncryption. DynamoDbEncryption ();
199
170
@@ -203,15 +174,12 @@ module DynamoDbGetEncryptedDataKeyDescriptionTest {
203
174
);
204
175
205
176
var actualDataKeyDescription := ddbEncResources. GetEncryptedDataKeyDescription (inputVariable);
206
-
207
177
expect UTF8. Decode (expectedHead.dataKeys[0].keyProviderId). Success?;
208
178
expect UTF8. Decode (expectedHead.dataKeys[0].keyProviderInfo). Success?;
209
179
expect actualDataKeyDescription. Success?;
210
180
expect |actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput| > 0;
211
-
212
181
expect |actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput| == |expectedHead. dataKeys|;
213
182
expect actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput[0]. keyProviderId == UTF8. Decode (expectedHead.dataKeys[0].keyProviderId). Extract ();
214
-
215
183
expect actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput[0]. keyProviderInfo. Some?;
216
184
expect actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput[0]. keyProviderInfo. Extract () == UTF8. Decode (expectedHead.dataKeys[0].keyProviderInfo). Extract ();
217
185
}
@@ -220,33 +188,27 @@ module DynamoDbGetEncryptedDataKeyDescriptionTest {
220
188
{
221
189
var expectedHead := CreatePartialHeader (testVersion, testFlavor, testMsgID, testLegend, testEncContext, [testAwsKmsHDataKey]);
222
190
var serializedHeader := expectedHead. serialize () + expectedHead. msgID;
223
-
224
191
var expectedBranchKeyVersion := getBranchKeyVersion (expectedHead);
225
192
var attr := map ["aws_dbe_head" := ComAmazonawsDynamodbTypes. AttributeValue. B (serializedHeader)];
226
193
var ddbEncResources :- expect DynamoDbEncryption. DynamoDbEncryption ();
227
-
228
194
var inputVariable: Types. GetEncryptedDataKeyDescriptionInput :=
229
195
Types. GetEncryptedDataKeyDescriptionInput (
230
196
input := Types.plaintextItem(plaintextItem := attr)
231
197
);
232
-
233
198
var actualDataKeyDescription := ddbEncResources. GetEncryptedDataKeyDescription (inputVariable);
234
199
235
200
expect UTF8. Decode (expectedHead.dataKeys[0].keyProviderId). Success?;
236
201
expect UTF8. Decode (expectedHead.dataKeys[0].keyProviderInfo). Success?;
237
202
expect actualDataKeyDescription. Success?;
238
203
expect |actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput| > 0;
239
-
240
204
expect |actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput| == |expectedHead. dataKeys|;
241
205
expect actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput[0]. keyProviderId == UTF8. Decode (expectedHead.dataKeys[0].keyProviderId). Extract ();
242
-
243
206
expect actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput[0]. keyProviderInfo. Some?;
244
207
expect actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput[0]. keyProviderInfo. Extract () == UTF8. Decode (expectedHead.dataKeys[0].keyProviderInfo). Extract ();
245
208
246
209
if actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput[0]. keyProviderId == "aws- kms- hierarchy" {
247
210
expect actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput[0]. branchKeyId. Some?;
248
211
expect actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput[0]. branchKeyVersion. Some?;
249
-
250
212
expect actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput[0]. branchKeyId. Extract () == UTF8. Decode (expectedHead.dataKeys[0].keyProviderInfo). Extract ();
251
213
expect actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput[0]. branchKeyVersion. Extract () == expectedBranchKeyVersion;
252
214
}
@@ -256,26 +218,20 @@ module DynamoDbGetEncryptedDataKeyDescriptionTest {
256
218
{
257
219
var expectedHead := CreatePartialHeader (testVersion, testFlavor, testMsgID, testLegend, testEncContext, [testRawRsaDataKey]);
258
220
var serializedHeader := expectedHead. serialize () + expectedHead. msgID;
259
-
260
221
var attr := map ["aws_dbe_head" := ComAmazonawsDynamodbTypes. AttributeValue. B (serializedHeader)];
261
222
var ddbEncResources :- expect DynamoDbEncryption. DynamoDbEncryption ();
262
-
263
-
264
223
var inputVariable: Types. GetEncryptedDataKeyDescriptionInput :=
265
224
Types. GetEncryptedDataKeyDescriptionInput (
266
225
input := Types.plaintextItem(plaintextItem := attr)
267
- );
268
-
226
+ );
269
227
var actualDataKeyDescription := ddbEncResources. GetEncryptedDataKeyDescription (inputVariable);
270
228
271
229
expect UTF8. Decode (expectedHead.dataKeys[0].keyProviderId). Success?;
272
230
expect UTF8. Decode (expectedHead.dataKeys[0].keyProviderInfo). Success?;
273
231
expect actualDataKeyDescription. Success?;
274
232
expect |actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput| > 0;
275
-
276
233
expect |actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput| == |expectedHead. dataKeys|;
277
234
expect actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput[0]. keyProviderId == UTF8. Decode (expectedHead.dataKeys[0].keyProviderId). Extract ();
278
-
279
235
expect actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput[0]. keyProviderInfo. Some?;
280
236
expect actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput[0]. keyProviderInfo. Extract () == UTF8. Decode (expectedHead.dataKeys[0].keyProviderInfo). Extract ();
281
237
}
@@ -284,26 +240,20 @@ module DynamoDbGetEncryptedDataKeyDescriptionTest {
284
240
{
285
241
var expectedHead := CreatePartialHeader (testVersion, testFlavor, testMsgID, testLegend, testEncContext, [testAwsKmsRsaDataKey]);
286
242
var serializedHeader := expectedHead. serialize () + expectedHead. msgID;
287
-
288
243
var attr := map ["aws_dbe_head" := ComAmazonawsDynamodbTypes. AttributeValue. B (serializedHeader)];
289
244
var ddbEncResources :- expect DynamoDbEncryption. DynamoDbEncryption ();
290
-
291
-
292
245
var inputVariable: Types. GetEncryptedDataKeyDescriptionInput :=
293
246
Types. GetEncryptedDataKeyDescriptionInput (
294
247
input := Types.plaintextItem(plaintextItem := attr)
295
248
);
296
-
297
249
var actualDataKeyDescription := ddbEncResources. GetEncryptedDataKeyDescription (inputVariable);
298
250
299
251
expect UTF8. Decode (expectedHead.dataKeys[0].keyProviderId). Success?;
300
252
expect UTF8. Decode (expectedHead.dataKeys[0].keyProviderInfo). Success?;
301
253
expect actualDataKeyDescription. Success?;
302
254
expect |actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput| > 0;
303
-
304
255
expect |actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput| == |expectedHead. dataKeys|;
305
256
expect actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput[0]. keyProviderId == UTF8. Decode (expectedHead.dataKeys[0].keyProviderId). Extract ();
306
-
307
257
expect actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput[0]. keyProviderInfo. Some?;
308
258
expect actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput[0]. keyProviderInfo. Extract () == UTF8. Decode (expectedHead.dataKeys[0].keyProviderInfo). Extract ();
309
259
}
@@ -312,14 +262,11 @@ module DynamoDbGetEncryptedDataKeyDescriptionTest {
312
262
{
313
263
var expectedHead := CreatePartialHeader (testVersion, testFlavor, testMsgID, testLegend, testEncContext, [testAwsKmsDataKey, testAwsKmsRsaDataKey]);
314
264
var serializedHeader := expectedHead. serialize () + expectedHead. msgID;
315
-
316
265
var ddbEncResources :- expect DynamoDbEncryption. DynamoDbEncryption ();
317
-
318
266
var inputVariable: Types. GetEncryptedDataKeyDescriptionInput :=
319
267
Types. GetEncryptedDataKeyDescriptionInput (
320
268
input := Types.header(header := serializedHeader)
321
269
);
322
-
323
270
var actualDataKeyDescription := ddbEncResources. GetEncryptedDataKeyDescription (inputVariable);
324
271
325
272
expect actualDataKeyDescription. Success?;
@@ -343,18 +290,13 @@ module DynamoDbGetEncryptedDataKeyDescriptionTest {
343
290
{
344
291
var expectedHead := CreatePartialHeader (testVersion, testFlavor, testMsgID, testLegend, testEncContext, [testAwsKmsDataKey, testAwsKmsRsaDataKey]);
345
292
var serializedHeader := expectedHead. serialize () + expectedHead. msgID;
346
-
347
293
var attr := map ["aws_dbe_head" := ComAmazonawsDynamodbTypes. AttributeValue. B (serializedHeader)];
348
294
var ddbEncResources :- expect DynamoDbEncryption. DynamoDbEncryption ();
349
-
350
-
351
295
var inputVariable: Types. GetEncryptedDataKeyDescriptionInput :=
352
296
Types. GetEncryptedDataKeyDescriptionInput (
353
297
input := Types.plaintextItem(plaintextItem := attr)
354
298
);
355
-
356
299
var actualDataKeyDescription := ddbEncResources. GetEncryptedDataKeyDescription (inputVariable);
357
-
358
300
expect actualDataKeyDescription. Success?;
359
301
expect |actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput| == |expectedHead. dataKeys|;
360
302
expect |actualDataKeyDescription. Extract (). EncryptedDataKeyDescriptionOutput| > 0;
@@ -377,13 +319,9 @@ module DynamoDbGetEncryptedDataKeyDescriptionTest {
377
319
{
378
320
expect EdkWrapping. GetProviderWrappedMaterial (expectedHead.dataKeys[0].ciphertext, algorithmSuite). Success?;
379
321
var providerWrappedMaterial := EdkWrapping. GetProviderWrappedMaterial (expectedHead.dataKeys[0].ciphertext, algorithmSuite). Extract ();
380
-
381
322
expect |providerWrappedMaterial| >= (28 + 16);
382
-
383
323
var expectedBranchKeyVersionResult := UUID. FromByteArray (providerWrappedMaterial[28 .. (28 + 16)]);
384
-
385
324
expect expectedBranchKeyVersionResult. Success?;
386
-
387
325
expectedBranchKeyVersion := expectedBranchKeyVersionResult. Extract ();
388
326
}
389
327
}
0 commit comments