corekt.spthy

changequote(<!,!>)

theory corekt
begin

include(protocol/primitives.spthy)

include(protocol/kemtls_keygen.spthy)

rule Action_Fact_API_declarations:
  []--[
    Replayable('tid', 'stage') // need this since it's only defined in PDK variants but is used in reachability lemmas, and Tamarin will complain when running without the PDK variant included
  ]->[]

include(protocol/kemtls_sauth_defines.spthy)

#ifdef INCLUDE_KEMTLS_SAUTH_OR_MUTUAL
include(protocol/kemtls_sauth_or_mutual_client.spthy)
#endif

#ifdef INCLUDE_KEMTLS_SAUTH
include(protocol/kemtls_sauth_client.spthy)
include(protocol/kemtls_sauth_server.spthy)
#endif

include(protocol/kemtls_mutual_defines.spthy)
#ifdef INCLUDE_KEMTLS_MUTUAL
include(protocol/kemtls_mutual_client.spthy)
include(protocol/kemtls_mutual_server.spthy)
#endif

include(protocol/kemtls_pdk_sauth_defines.spthy)
#ifdef INCLUDE_KEMTLS_PDK_SAUTH
include(protocol/kemtls_pdk_sauth_client.spthy)
include(protocol/kemtls_pdk_sauth_server.spthy)
#endif

include(protocol/kemtls_pdk_mutual_defines.spthy)
#ifdef INCLUDE_KEMTLS_PDK_MUTUAL
include(protocol/kemtls_pdk_mutual_client.spthy)
include(protocol/kemtls_pdk_mutual_server.spthy)
#endif

include(model/oracles.spthy)

include(lemmas/reachable.spthy)
include(lemmas/attacker_works.spthy)
include(lemmas/match_security.spthy)
include(lemmas/sk_security.spthy)
include(lemmas/malicious_acceptance.spthy)

end