Changing "lost" from a parameter of protocol definitions to a constant.
Advantages: no "lost" argument everywhere; fewer Vars in subgoals;
less need for specially instantiated rules
Disadvantage: can no longer prove "Agent_not_see_encrypted_key", but this
theorem was never used, and its original proof was also broken
the introduction of the "Notes" constructor.
(* Title: HOL/Auth/Message
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
Datatypes of agents and messages;
Inductive relations "parts", "analz" and "synth"
*)
Message = Arith +
(*Is there a difference between a nonce and arbitrary numerical data?
Do we need a type of nonces?*)
types
key = nat
consts
invKey :: key=>key
rules
invKey "invKey (invKey K) = K"
(*The inverse of a symmetric key is itself;
that of a public key is the private key and vice versa*)
constdefs
isSymKey :: key=>bool
"isSymKey K == (invKey K = K)"
datatype (*We allow any number of friendly agents*)
agent = Server | Friend nat | Spy
datatype (*Messages are agent names, nonces, keys, pairs and encryptions*)
msg = Agent agent
| Nonce nat
| Key key
| Hash msg
| MPair msg msg
| Crypt key msg
(*Allows messages of the form {|A,B,NA|}, etc...*)
syntax
"@MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})")
translations
"{|x, y, z|}" == "{|x, {|y, z|}|}"
"{|x, y|}" == "MPair x y"
constdefs
(*Message Y, paired with a MAC computed with the help of X*)
HPair :: "[msg,msg]=>msg" ("(4Hash[_] /_)" [0, 1000])
"Hash[X] Y == {| Hash{|X,Y|}, Y|}"
(*Keys useful to decrypt elements of a message set*)
keysFor :: msg set => key set
"keysFor H == invKey `` {K. EX X. Crypt K X : H}"
(** Inductive definition of all "parts" of a message. **)
consts parts :: msg set => msg set
inductive "parts H"
intrs
Inj "X: H ==> X: parts H"
Fst "{|X,Y|} : parts H ==> X : parts H"
Snd "{|X,Y|} : parts H ==> Y : parts H"
Body "Crypt K X : parts H ==> X : parts H"
(** Inductive definition of "analz" -- what can be broken down from a set of
messages, including keys. A form of downward closure. Pairs can
be taken apart; messages decrypted with known keys. **)
consts analz :: msg set => msg set
inductive "analz H"
intrs
Inj "X: H ==> X: analz H"
Fst "{|X,Y|} : analz H ==> X : analz H"
Snd "{|X,Y|} : analz H ==> Y : analz H"
Decrypt "[| Crypt K X : analz H; Key(invKey K): analz H |] ==> X : analz H"
(** Inductive definition of "synth" -- what can be built up from a set of
messages. A form of upward closure. Pairs can be built, messages
encrypted with known keys. Agent names may be quoted. **)
consts synth :: msg set => msg set
inductive "synth H"
intrs
Inj "X: H ==> X: synth H"
Agent "Agent agt : synth H"
Hash "X: synth H ==> Hash X : synth H"
MPair "[| X: synth H; Y: synth H |] ==> {|X,Y|} : synth H"
Crypt "[| X: synth H; Key(K) : H |] ==> Crypt K X : synth H"
end