Skip to content

Commit

Permalink
chore: add documentation to externs (#590)
Browse files Browse the repository at this point in the history
* chore: add documentation to externs
  • Loading branch information
ajewellamz authored Aug 13, 2024
1 parent c07a51f commit bd44ca8
Show file tree
Hide file tree
Showing 3 changed files with 28 additions and 4 deletions.
7 changes: 3 additions & 4 deletions AwsCryptographyPrimitives/src/Digest.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
17 changes: 17 additions & 0 deletions AwsCryptographyPrimitives/src/ECDH.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -107,37 +107,54 @@ module {:extern "ECDH"} ECDH {
));
}

// Generate an ECDH key pair
// 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<EccKeyPair, Types.Error>)
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 DER-encoded X.509 SubjectPublicKeyInfo
method {:extern "ECDH.ECCUtils", "GetPublicKey"} ExternGetPublicKeyFromPrivate(
curveAlgorithm: Types.ECDHCurveSpec,
privateKey: Types.ECCPrivateKey
) returns (res: Result<seq<uint8>, 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 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,
publicKey: seq<uint8>
) returns (res: Result<bool, Types.Error>)

// Calculate a shared secret from the keys
// Private key is PEM formatted UTF8
// 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<seq<uint8>, Types.Error>)

// Convert DER-encoded X.509 SubjectPublicKeyInfo public key bytes to compressed X9.62 format
method {:extern "ECDH.ECCUtils", "CompressPublicKey"} ExternCompressPublicKey(
publicKey: seq<uint8>,
curveAlgorithm: Types.ECDHCurveSpec
) returns (res: Result<seq<uint8>, Types.Error>)

// 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<uint8>,
curveAlgorithm: Types.ECDHCurveSpec
) returns (res: Result<seq<uint8>, Types.Error>)

// Ensure that this public key is DER-encoded X.509 SubjectPublicKeyInfo format
method {:extern "ECDH.ECCUtils", "ParsePublicKey"} ExternParsePublicKey(
publicKey: seq<uint8>
) returns (res: Result<seq<uint8>, Types.Error>)
Expand Down
8 changes: 8 additions & 0 deletions AwsCryptographyPrimitives/src/Signature.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -55,18 +55,26 @@ 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-encoded
method {:extern "Signature.ECDSA", "ExternKeyGen"} ExternKeyGen(
s: Types.ECDSASignatureAlgorithm
) returns (res: Result<SignatureKeyPair, Types.Error>)
ensures res.Success? ==> IsValidSignatureKeyPair(res.value)

// sign the message with the private key
// private signing key is DER-encoded
method {:extern "Signature.ECDSA", "Sign"} Sign(
s: Types.ECDSASignatureAlgorithm,
key: seq<uint8>,
msg: seq<uint8>
) returns (sig: Result<seq<uint8>, Types.Error>)
ensures sig.Success? ==> IsSigned(key, msg, sig.value)

// Verify that these bytes created this signature
// 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.
function method {:extern "Signature.ECDSA", "Verify"} Verify(
Expand Down

0 comments on commit bd44ca8

Please sign in to comment.