config.mpv

#pragma once
(*
 * TODO:
 *
 * - The way KDF is setup currently leads to exponential debug output sizes; reformulate for linear output size
 * - Capture nonce reuse being forbidden
 * - Capture key reuse being forbidden
 * - Capture that deriving keys from bitss is insecure
 * - Capture CPAKEM CPA security
 * - Capture standard security notions
 * - Capture DOS/Termination security notions
 * - Capture key construction from other types being insecure
 * - Simulate ning & hülsing version to show differences
 * - Key compromise impersonation
 * - Unknown keyshare
 * - Record expected results
 *)

(* TODO: Are there any usages of natural numbers beyond succ()? If not, replace
   with a succ() function for cryptoverif compat *)

//restriction p:Atom, gc:N, lc:N, n:Atom;
//  table(OracleCtr(Fsetup_psk, p, gc, 1, n));
//  table(OracleCtr(Fsetup_server, p, gc, 2, n));
//  table(OracleCtr(Finitiator, p, gc, 3, n));
//  table(OracleCtr(Finit_hello, p, gc, 3, n));
//  table(OracleCtr(Finit_conf, p, gc, 3, n)).

#ifndef CHAINING_KEY_EVENTS
#define CHAINING_KEY_EVENTS 1
#endif

#ifndef MESSAGE_TRANSMISSION_EVENTS
#define MESSAGE_TRANSMISSION_EVENTS 1
#endif

#ifndef SESSION_START_EVENTS
#define SESSION_START_EVENTS 1
#endif

// Disabling randomized call ids has some effect on the repeatability of queries:
// Without randomized ("new call:Atom") ids the call id is based on the sum of all
// parameters; this means that a call can be resubmitted provided the parameters are
// exactly the same; this is not a problem for secrecy queries; it is however a problem
// for the queries validating that the same session can not be started twice (replay attack resistance).
#ifndef RANDOMIZED_CALL_IDS
#define RANDOMIZED_CALL_IDS 1
#endif

#define INITIATOR_BOUND unbounded
#define RESPONDER_BOUND unbounded
#define SIMPLE_MODEL 0
#define FULL_MODEL !SIMPLE_MODEL

set inductionQueries=true.
set nounifIgnoreAFewTimes=auto.
set abbreviateClauses=true.
set removeUselessClausesBeforeDisplay=true.
set preciseActions=true.
set movenew=false.
set movelet=true.
set expandSimplifyIfCst=true.
set unifyDerivation=true.
set privateCommOnPublicTerms=false.

#define VERBOSE false
set verboseRules=VERBOSE.
set verboseTerm=VERBOSE.
set verboseDestructors=VERBOSE.
set verboseRedundant=VERBOSE.
set verboseCompleted=VERBOSE.

#if CHAINING_KEY_EVENTS
#define CK_EV(...) __VA_ARGS__
#else
#define CK_EV(...)
#endif

#if MESSAGE_TRANSMISSION_EVENTS
#define MTX_EV(...) __VA_ARGS__
#else
#define MTX_EV(...)
#endif

#if SESSION_START_EVENTS
#define SES_EV(...) __VA_ARGS__
#else
#define SES_EV(...)
#endif


(* TODO: Authentication timing properties *)
(* TODO: Proof that every adversary submitted package is equivalent to one generated by the proper algorithm using different coins. This probably requires introducing an oracle that extracts the coins used and explicitly adding the notion of coins used for Packet->Packet steps and an inductive RNG notion. *)
(* TODO: Proper retransmission resistance modeling using state packing instead of this linear structure: There are no two packet acceptance events such that the packet is the same but the before states are different (unless talking about InitHello). There is no two RespHello acceptance events such that the associated before and after states are excatly the same. *)