From 1c4996009e4f8bb8e35539c573b230569e987925 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Tue, 13 Aug 2024 10:23:57 -0400 Subject: [PATCH 1/2] chore: add documentation to externs --- AwsCryptographyPrimitives/src/Digest.dfy | 7 +++---- AwsCryptographyPrimitives/src/ECDH.dfy | 19 +++++++++++++++++++ AwsCryptographyPrimitives/src/Signature.dfy | 8 ++++++++ 3 files changed, 30 insertions(+), 4 deletions(-) diff --git a/AwsCryptographyPrimitives/src/Digest.dfy b/AwsCryptographyPrimitives/src/Digest.dfy index e97509c7a..b3ad11eb1 100644 --- a/AwsCryptographyPrimitives/src/Digest.dfy +++ b/AwsCryptographyPrimitives/src/Digest.dfy @@ -13,10 +13,9 @@ module Digest { function method Length(digestAlgorithm: Types.DigestAlgorithm): nat { match digestAlgorithm - case SHA_512 => 64 - case SHA_384 => 48 - case SHA_256 => 32 - case SHA_1 => 20 + case SHA_512() => 64 + case SHA_384() => 48 + case SHA_256() => 32 } method Digest(input: Types.DigestInput) diff --git a/AwsCryptographyPrimitives/src/ECDH.dfy b/AwsCryptographyPrimitives/src/ECDH.dfy index acc3664dc..1244d387d 100644 --- a/AwsCryptographyPrimitives/src/ECDH.dfy +++ b/AwsCryptographyPrimitives/src/ECDH.dfy @@ -107,37 +107,56 @@ module {:extern "ECDH"} ECDH { )); } + // Generate an ECDH key pair + // Return the private key as UTF8 of PEM of Rfc5915 Der format + // Return the public key as UTF8 of PEM of X.509 SubjectPublicKeyInfo DER format method {:extern "ECDH.KeyGeneration", "GenerateKeyPair"} ExternEccKeyGen( s: Types.ECDHCurveSpec ) returns (res: Result) ensures res.Success? ==> 1 < |res.value.publicKey| <= 8192 + // Given a private key, return the associated public key + // Input private key is in PEM format + // Output public key is X.509 SubjectPublicKeyInfo DER format, but not PEM formatted method {:extern "ECDH.ECCUtils", "GetPublicKey"} ExternGetPublicKeyFromPrivate( curveAlgorithm: Types.ECDHCurveSpec, privateKey: Types.ECCPrivateKey ) returns (res: Result, Types.Error>) + // Ensure that this public key follows 5.6.2.3.3 ECC Full Public-Key Validation Routine from + // https://nvlpubs.nist.gov/nistpubs/SpecialPublications/NIST.SP.800-56Ar3.pdf#page=55 + // Input public key is X.509 SubjectPublicKeyInfo DER format, but not PEM formatted + // Result is never Success(false), it's either Success(true) or Failure() method {:extern "ECDH.ECCUtils", "ValidatePublicKey"} ExternValidatePublicKey( curveAlgorithm: Types.ECDHCurveSpec, publicKey: seq ) returns (res: Result) + // Calculate a shared secret from the keys + // Private key is PEM formatted UTF8 + // Input public key is X.509 SubjectPublicKeyInfo DER format, but not PEM formatted method {:extern "ECDH.DeriveSharedSecret", "CalculateSharedSecret"} ExternDeriveSharedSecret( curveAlgorithm: Types.ECDHCurveSpec, privateKey: Types.ECCPrivateKey, publicKey: Types.ECCPublicKey ) returns (res: Result, Types.Error>) + // Convert X.509 encoded public key to compressed X9.62 format + // input is not pem formatted method {:extern "ECDH.ECCUtils", "CompressPublicKey"} ExternCompressPublicKey( publicKey: seq, curveAlgorithm: Types.ECDHCurveSpec ) returns (res: Result, Types.Error>) + // Convert X9.62 encoded public key to X.509 format + // input is not pem formatted method {:extern "ECDH.ECCUtils", "DecompressPublicKey"} ExternDecompressPublicKey( publicKey: seq, curveAlgorithm: Types.ECDHCurveSpec ) returns (res: Result, Types.Error>) + // Ensure that this public key is in X.509 SubjectPublicKeyInfo DER format + // input is not pem formatted method {:extern "ECDH.ECCUtils", "ParsePublicKey"} ExternParsePublicKey( publicKey: seq ) returns (res: Result, Types.Error>) diff --git a/AwsCryptographyPrimitives/src/Signature.dfy b/AwsCryptographyPrimitives/src/Signature.dfy index b550b9fda..b3f3f4af0 100644 --- a/AwsCryptographyPrimitives/src/Signature.dfy +++ b/AwsCryptographyPrimitives/src/Signature.dfy @@ -55,11 +55,16 @@ module {:extern "Signature"} Signature { )); } + // Generate an ECDSA key pair + // Verification key, a.k.a public key, is in X9.62 compressed format + // Signing Key, a.k.a private key, is in der format method {:extern "Signature.ECDSA", "ExternKeyGen"} ExternKeyGen( s: Types.ECDSASignatureAlgorithm ) returns (res: Result) ensures res.Success? ==> IsValidSignatureKeyPair(res.value) + // sign the message with the key + // private signing key is in der format method {:extern "Signature.ECDSA", "Sign"} Sign( s: Types.ECDSASignatureAlgorithm, key: seq, @@ -67,6 +72,9 @@ module {:extern "Signature"} Signature { ) returns (sig: Result, Types.Error>) ensures sig.Success? ==> IsSigned(key, msg, sig.value) + // Verify that these bytes created this signature + // Public verification key is in X9.62 DER format + // If signature does not match Success(false) is returned // This is a valid function // because the same inputs will result in the same outputs. function method {:extern "Signature.ECDSA", "Verify"} Verify( From af054ed1a69155aaf9df16d9cb2ea92ef1e79314 Mon Sep 17 00:00:00 2001 From: Andrew Jewell <107044381+ajewellamz@users.noreply.github.com> Date: Tue, 13 Aug 2024 14:48:10 -0400 Subject: [PATCH 2/2] Apply suggestions from code review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: José Corella <39066999+josecorella@users.noreply.github.com> --- AwsCryptographyPrimitives/src/ECDH.dfy | 20 +++++++++----------- AwsCryptographyPrimitives/src/Signature.dfy | 8 ++++---- 2 files changed, 13 insertions(+), 15 deletions(-) diff --git a/AwsCryptographyPrimitives/src/ECDH.dfy b/AwsCryptographyPrimitives/src/ECDH.dfy index 1244d387d..f099c92a6 100644 --- a/AwsCryptographyPrimitives/src/ECDH.dfy +++ b/AwsCryptographyPrimitives/src/ECDH.dfy @@ -108,8 +108,8 @@ module {:extern "ECDH"} ECDH { } // Generate an ECDH key pair - // Return the private key as UTF8 of PEM of Rfc5915 Der format - // Return the public key as UTF8 of PEM of X.509 SubjectPublicKeyInfo DER format + // Return the private key as UTF8 PEM-encoded Rfc5915 format, + // Return the public key as DER-encoded X.509 SubjectPublicKeyInfo bytes method {:extern "ECDH.KeyGeneration", "GenerateKeyPair"} ExternEccKeyGen( s: Types.ECDHCurveSpec ) returns (res: Result) @@ -117,7 +117,7 @@ module {:extern "ECDH"} ECDH { // Given a private key, return the associated public key // Input private key is in PEM format - // Output public key is X.509 SubjectPublicKeyInfo DER format, but not PEM formatted + // Output public key is DER-encoded X.509 SubjectPublicKeyInfo method {:extern "ECDH.ECCUtils", "GetPublicKey"} ExternGetPublicKeyFromPrivate( curveAlgorithm: Types.ECDHCurveSpec, privateKey: Types.ECCPrivateKey @@ -125,7 +125,7 @@ module {:extern "ECDH"} ECDH { // Ensure that this public key follows 5.6.2.3.3 ECC Full Public-Key Validation Routine from // https://nvlpubs.nist.gov/nistpubs/SpecialPublications/NIST.SP.800-56Ar3.pdf#page=55 - // Input public key is X.509 SubjectPublicKeyInfo DER format, but not PEM formatted + // Input public key is DER-encoded X.509 SubjectPublicKeyInfo bytes // Result is never Success(false), it's either Success(true) or Failure() method {:extern "ECDH.ECCUtils", "ValidatePublicKey"} ExternValidatePublicKey( curveAlgorithm: Types.ECDHCurveSpec, @@ -134,29 +134,27 @@ module {:extern "ECDH"} ECDH { // Calculate a shared secret from the keys // Private key is PEM formatted UTF8 - // Input public key is X.509 SubjectPublicKeyInfo DER format, but not PEM formatted + // Input public key is DER-encoded X.509 SubjectPublicKeyInfo bytes method {:extern "ECDH.DeriveSharedSecret", "CalculateSharedSecret"} ExternDeriveSharedSecret( curveAlgorithm: Types.ECDHCurveSpec, privateKey: Types.ECCPrivateKey, publicKey: Types.ECCPublicKey ) returns (res: Result, Types.Error>) - // Convert X.509 encoded public key to compressed X9.62 format - // input is not pem formatted + // Convert DER-encoded X.509 SubjectPublicKeyInfo public key bytes to compressed X9.62 format method {:extern "ECDH.ECCUtils", "CompressPublicKey"} ExternCompressPublicKey( publicKey: seq, curveAlgorithm: Types.ECDHCurveSpec ) returns (res: Result, Types.Error>) - // Convert X9.62 encoded public key to X.509 format - // input is not pem formatted + // Convert X9.62 encoded public key bytes to DER-encoded X.509 SubjectPublicKeyInfo format + // input is not PEM-encoded method {:extern "ECDH.ECCUtils", "DecompressPublicKey"} ExternDecompressPublicKey( publicKey: seq, curveAlgorithm: Types.ECDHCurveSpec ) returns (res: Result, Types.Error>) - // Ensure that this public key is in X.509 SubjectPublicKeyInfo DER format - // input is not pem formatted + // Ensure that this public key is DER-encoded X.509 SubjectPublicKeyInfo format method {:extern "ECDH.ECCUtils", "ParsePublicKey"} ExternParsePublicKey( publicKey: seq ) returns (res: Result, Types.Error>) diff --git a/AwsCryptographyPrimitives/src/Signature.dfy b/AwsCryptographyPrimitives/src/Signature.dfy index b3f3f4af0..c87d33469 100644 --- a/AwsCryptographyPrimitives/src/Signature.dfy +++ b/AwsCryptographyPrimitives/src/Signature.dfy @@ -57,14 +57,14 @@ module {:extern "Signature"} Signature { // Generate an ECDSA key pair // Verification key, a.k.a public key, is in X9.62 compressed format - // Signing Key, a.k.a private key, is in der format + // Signing Key, a.k.a private key, is in DER-encoded method {:extern "Signature.ECDSA", "ExternKeyGen"} ExternKeyGen( s: Types.ECDSASignatureAlgorithm ) returns (res: Result) ensures res.Success? ==> IsValidSignatureKeyPair(res.value) - // sign the message with the key - // private signing key is in der format + // sign the message with the private key + // private signing key is DER-encoded method {:extern "Signature.ECDSA", "Sign"} Sign( s: Types.ECDSASignatureAlgorithm, key: seq, @@ -73,7 +73,7 @@ module {:extern "Signature"} Signature { ensures sig.Success? ==> IsSigned(key, msg, sig.value) // Verify that these bytes created this signature - // Public verification key is in X9.62 DER format + // Public verification key is DER-encoded X9.62 format // If signature does not match Success(false) is returned // This is a valid function // because the same inputs will result in the same outputs.