main.spthy

theory proto_main_module

begin

builtins: signing




//define(`hosted-signature-based', 1)
//  # define(`compromise-merchant-processor', 1)
//  define(`compromise-client-merchant', 1)
//  # define(`compromise-client-processor', 1)

// # --- Channels Implementations Below
include(channels/secure.spthy)
include(channels/plaintext.spthy)
include(channels/config.spthy)


// # --- Utils
include(utils/tampering.spthy)
include(utils/memory.spthy)


// # --- Classes Implementations Below
ifdef(`direct:signature',`include(classes/direct:signature.spthy)',)
ifdef(`direct:encrypted',`include(classes/direct:encrypted.spthy)',)
ifdef(`direct:simple',`include(classes/direct:simple.spthy)',)
ifdef(`delegated:simple',`include(classes/delegated:simple.spthy)',)
ifdef(`delegated:ctoken',`include(classes/delegated:ctoken.spthy)',)
ifdef(`delegated:signature',`include(classes/delegated:signature.spthy)',)
ifdef(`delegated:mtoken',`include(classes/delegated:mtoken.spthy)',)
ifdef(`delegated:ctoken:encrypted',`include(classes/delegated:ctoken:encrypted.spthy)',)


// # --- Generic Lemmas Below
include(lemmas/sanity-check.spthy)
include(lemmas/intercept-card-data.spthy)
include(lemmas/forge-payment-processor-confirmation.spthy)
include(lemmas/validate-shown-price.spthy)
include(lemmas/hijack-transaction.spthy)
include(lemmas/forge-merchant-confirmation.spthy)
include(lemmas/client-tampers-price.spthy)
include(lemmas/merchant-replays-transaction.spthy)
include(lemmas/mitm-tampers-price.spthy)
include(lemmas/merchant-tampers-price.spthy)
end