Theory Agents

(*******************************************************************************

  Agents and nonces (partly based on Paulson's Message.thy)


*******************************************************************************)

section ‹Atomic messages›

theory Agents imports Main 
begin

text ‹The definitions below are moved here from the message theory, since
the higher levels of protocol abstraction do not know about cryptographic 
messages.›


(******************************************************************************)
subsection ‹Agents›
(******************************************************************************)

type_synonym as = nat  (* We allow any number of agents (ASes). *)

type_synonym aso = "as option"

type_synonym ases = "as set"


locale compromised =
fixes 
  bad :: "as set"			      ― ‹compromised ASes›
begin

abbreviation 
  good :: "as set"
where
  "good ≡ -bad"
end
        
(******************************************************************************)
subsection ‹Nonces and keys›
(******************************************************************************)

text ‹We have an unspecified type of freshness identifiers. 
For executability, we may need to assume that this type is infinite.›

typedecl fid_t

datatype fresh_t = 
  mk_fresh "fid_t" "nat"      (infixr ‹$› 65) 

fun fid :: "fresh_t ⇒ fid_t" where
  "fid (f $ n) = f"

fun num :: "fresh_t ⇒ nat" where
  "num (f $ n) = n"


text ‹Nonces›

type_synonym 
  nonce = "fresh_t"



end