From d572ae7448172cbb9615f6b76351d0bd6b340164 Mon Sep 17 00:00:00 2001 From: svenfeld Date: Thu, 25 Apr 2024 09:40:40 +0200 Subject: [PATCH 1/4] Update rules for https://github.com/tink-crypto/tink-java 1.13 --- Tink/src/DeterministicAeadKeyTemplates.crysl | 16 ---------------- Tink/src/KeyTemplate.crysl | 16 +++++++--------- Tink/src/KeysetHandle.crysl | 12 +++++++++--- ...redefinedDeterministicAeadParameters.crysl | 14 ++++++++++++++ Tink/src/PredefinedMacParameters.crysl | 19 +++++++++++++++++++ 5 files changed, 49 insertions(+), 28 deletions(-) create mode 100644 Tink/src/PredefinedDeterministicAeadParameters.crysl create mode 100644 Tink/src/PredefinedMacParameters.crysl diff --git a/Tink/src/DeterministicAeadKeyTemplates.crysl b/Tink/src/DeterministicAeadKeyTemplates.crysl index 4a102210..ed7db5d5 100644 --- a/Tink/src/DeterministicAeadKeyTemplates.crysl +++ b/Tink/src/DeterministicAeadKeyTemplates.crysl @@ -1,19 +1,3 @@ -/* - * This is a CrySL specification for the Google Tink implementation of - * the class DeterministicAeadKeyTemplates. - * - * Note: in this case, we are not specifying the correct usage of the - * API, but actually guaranteeing that the Google Tink API implementation - * actually exposes some key templates as static attributes. This - * information simplifies the specification of other properties for - * correctly using the API. - * - * - * It constraints the use of the API to the following key templates: - * - * - aes256_siv - */ - SPEC com.google.crypto.tink.daead.DeterministicAeadKeyTemplates OBJECTS diff --git a/Tink/src/KeyTemplate.crysl b/Tink/src/KeyTemplate.crysl index 8af95660..07c575fa 100644 --- a/Tink/src/KeyTemplate.crysl +++ b/Tink/src/KeyTemplate.crysl @@ -1,14 +1,12 @@ -/* - * A CrySL specification for using the AEAD Factory - * of the Google Google library. - */ -SPEC com.google.crypto.tink.proto.KeyTemplate +SPEC com.google.crypto.tink.KeyTemplate OBJECTS - int x; + com.google.crypto.tink.KeyTemplate template + com.google.crypto.tink.Parameters params + EVENTS - evt : newBuilder(); + cre: template = createFrom(params) ORDER - evt* + cre+ ENSURES - readyForInstantiating[this]; + genKeyTemplate[template] diff --git a/Tink/src/KeysetHandle.crysl b/Tink/src/KeysetHandle.crysl index d670c759..2d51df0e 100644 --- a/Tink/src/KeysetHandle.crysl +++ b/Tink/src/KeysetHandle.crysl @@ -9,21 +9,27 @@ SPEC com.google.crypto.tink.KeysetHandle OBJECTS - com.google.crypto.tink.proto.KeyTemplate kt; + com.google.crypto.tink.KeyTemplate kt; com.google.crypto.tink.KeysetHandle publicKeysetHandle; + com.google.crypto.tink.mac.HmacParameters hmacParams; + EVENTS gen_evt : generateNew(kt); + gen_hmac_evt : generateNew(hmacParams); gen_public_evt : publicKeysetHandle = getPublicKeysetHandle(); read_evt : read(_, _); export_evt : write(_, _); + get_prim : getPrimitive(_); ORDER - (gen_evt | read_evt), gen_public_evt?, export_evt? + (gen_evt | read_evt), gen_public_evt?, export_evt?, get_prim* REQUIRES - keyTemplate[kt]; + genKeyTemplate[kt]; + hmacParams[hmacParams]; + ENSURES generatedKeySet[this]; diff --git a/Tink/src/PredefinedDeterministicAeadParameters.crysl b/Tink/src/PredefinedDeterministicAeadParameters.crysl new file mode 100644 index 00000000..56373a0a --- /dev/null +++ b/Tink/src/PredefinedDeterministicAeadParameters.crysl @@ -0,0 +1,14 @@ +SPEC com.google.crypto.tink.daead.PredefinedDeterministicAeadParameters + +OBJECTS + com.google.crypto.tink.daead.AesSivParameters params; + com.google.crypto.tink.daead.PredefinedDeterministicAeadParameters aeadParams; + +EVENTS + aead256: params = aeadParams.AES256_SIV; + +ORDER + con* + +ENSURES + genAeadParams[params]; diff --git a/Tink/src/PredefinedMacParameters.crysl b/Tink/src/PredefinedMacParameters.crysl new file mode 100644 index 00000000..37ac6214 --- /dev/null +++ b/Tink/src/PredefinedMacParameters.crysl @@ -0,0 +1,19 @@ +SPEC com.google.crypto.tink.mac.PredefinedMacParameters + +OBJECTS + com.google.crypto.tink.mac.HmacParameters hmacParams; + com.google.crypto.tink.mac.PredefinedMacParameters macParams + +EVENTS + hmac_sha256_128 : hmac_sha256 = macParams.HMAC_SHA256_128BITTAG + hmac_sha256_256 : hmac_sha256 = macParams.HMAC_SHA256_256BITTAG + Hmac_sha256: hmac_sha256_128 | hmac_sha256_256 + +ORDER + Hmac_sha256+ + +CONSTRAINTS + + +ENSURES + hmacParams[hmacParams] From ccd8ada4e70d5b8229f08a5b243ef9eb71aaeabb Mon Sep 17 00:00:00 2001 From: svenfeld Date: Mon, 3 Jun 2024 11:06:43 +0200 Subject: [PATCH 2/4] Add deprecated KeyTemplate KeySet Handle uses now the non deprecated version of KeyTemplate. If this old class is used a required predicate error will be shown --- Tink/src/KeyTemplateOld.crysl | 15 +++++++++++++++ Tink/src/PredefinedMacParameters.crysl | 3 --- 2 files changed, 15 insertions(+), 3 deletions(-) create mode 100644 Tink/src/KeyTemplateOld.crysl diff --git a/Tink/src/KeyTemplateOld.crysl b/Tink/src/KeyTemplateOld.crysl new file mode 100644 index 00000000..afc6b08e --- /dev/null +++ b/Tink/src/KeyTemplateOld.crysl @@ -0,0 +1,15 @@ +/* + * A CrySL specification for using the AEAD Factory + * of the Google Google library. + */ +SPEC com.google.crypto.tink.proto.KeyTemplate + +OBJECTS + int x; + +EVENTS + evt : newBuilder(); +ORDER + evt* +ENSURES + readyForInstantiating[this]; \ No newline at end of file diff --git a/Tink/src/PredefinedMacParameters.crysl b/Tink/src/PredefinedMacParameters.crysl index 37ac6214..893b1ea0 100644 --- a/Tink/src/PredefinedMacParameters.crysl +++ b/Tink/src/PredefinedMacParameters.crysl @@ -11,9 +11,6 @@ EVENTS ORDER Hmac_sha256+ - -CONSTRAINTS - ENSURES hmacParams[hmacParams] From 1f8a5c4c6f0e73eddbb6f7b71935ceb0f601b908 Mon Sep 17 00:00:00 2001 From: svenfeld Date: Mon, 3 Jun 2024 11:06:58 +0200 Subject: [PATCH 3/4] Readd previous deleted comments --- Tink/src/DeterministicAeadKeyTemplates.crysl | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/Tink/src/DeterministicAeadKeyTemplates.crysl b/Tink/src/DeterministicAeadKeyTemplates.crysl index ed7db5d5..4fa15e75 100644 --- a/Tink/src/DeterministicAeadKeyTemplates.crysl +++ b/Tink/src/DeterministicAeadKeyTemplates.crysl @@ -1,3 +1,20 @@ +/* + * This is a CrySL specification for the Google Tink implementation of + * the class DeterministicAeadKeyTemplates. + * + * Note: in this case, we are not specifying the correct usage of the + * API, but actually guaranteeing that the Google Tink API implementation + * actually exposes some key templates as static attributes. This + * information simplifies the specification of other properties for + * correctly using the API. + * + * + * It constraints the use of the API to the following key templates: + * + * - aes256_siv + */ + + SPEC com.google.crypto.tink.daead.DeterministicAeadKeyTemplates OBJECTS From ddc291fc2d1ab7580ebc70eb309f497dbf97f606 Mon Sep 17 00:00:00 2001 From: svenfeld <76941845+svenfeld@users.noreply.github.com> Date: Thu, 13 Jun 2024 09:33:54 +0200 Subject: [PATCH 4/4] MINOR --- Tink/src/DeterministicAeadKeyTemplates.crysl | 1 - 1 file changed, 1 deletion(-) diff --git a/Tink/src/DeterministicAeadKeyTemplates.crysl b/Tink/src/DeterministicAeadKeyTemplates.crysl index 4fa15e75..3631e274 100644 --- a/Tink/src/DeterministicAeadKeyTemplates.crysl +++ b/Tink/src/DeterministicAeadKeyTemplates.crysl @@ -33,4 +33,3 @@ CONSTRAINTS ENSURES keyTemplate[aes256_siv]; - \ No newline at end of file