Skip to content

CBMC Proofs for HKDF  #126

Open
Open
@ttjsu-aws

Description

@ttjsu-aws

This is in relation to the HKDF tests and CBMC proofs. Looks like the CBMC tests written for HKDF are specific to the APIs introduced in v 1.1.1 of openssl which we donot use.

Note that our library supports HKDF for openssl versions 1.0.2+. We currently use the HKDF APIs introduced in v 1.1.0 which is significantly different from v 1.1.1 in that HKDF modes were introduced later, and for versions less than 1.1.0 we have our own implementation of RFC 5869 which we use. We definitely would like to have the proofs for all HKDF versions.

Metadata

Metadata

Assignees

No one assigned

    Labels

    cbmcCBMC proof related workmaintenanceNecessary maintenance

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions