Appendix: Specifying Kerberos in Isabelle

 kerberos :: event list set

inductive kerberos



Nil     []  kerberos



Fake    [| evs : kerberos; B ~: Spy; X : synth(analz(sees Spy evs)) |]

	 ==>  Says Spy B X # evs : kerberos



K1      [| evs : kerberos; A ~: Kas |]

         ==> Says A Kas {|Agent A, Agent Tgs, Timestamp (CT evs)|} # evs : kerberos



K2 	[| evs : kerberos; A ~: Kas; Key AuthKey ~: used evs;
	   Says A' Kas {|Agent A, Agent Tgs, Timestamp Ta|} : set_of_list evs |]

	==>  Says Kas A (Crypt (shrK A)
		 		 {|Key AuthKey, Agent Tgs, Timestamp (CT evs),
		 		   (Crypt (shrK Tgs)
		 		 		 {|Agent A, Agent Tgs, Key AuthKey,
		 		 		 Timestamp (CT evs)|})
		 		 |})
		 # evs : kerberos



K3 	[| evs : kerberos; A ~: Tgs;
	   Says A Kas {|Agent A, Agent Tgs, Timestamp Ta|} : set_of_list evs;
	   Says Kas' A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Timestamp Tk, AuthTicket|})
	     : set_of_list evs;
 	   Tk <= Ta + RecentResp |]

	==>  Says A Tgs {|AuthTicket, (Crypt AuthKey {|Agent A, Timestamp (CT evs)|}), Agent B |}
		 # evs : kerberos



K4      [| evs : kerberos; A ~: Tgs; Key ServKey ~: used evs;
           Says A' Tgs {|(Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Timestamp Tk|}),
		 		  (Crypt AuthKey {|Agent A, Timestamp Ta1)|}), Agent B |}
	      : set_of_list evs;
	    (CT evs) <= Tk + AuthLife;
	    (CT evs) <= Ta1 + RecentAuth |]

	 ==> Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Timestamp (CT evs),
                           (Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Timestamp (CT evs)|})

		 	|})
	       # evs : kerberos



K5      [| evs : kerberos; A ~: B;
           Says A Tgs {|AuthTicket, (Crypt AuthKey {|Agent A, Timestamp Ta1|}), Agent B|}
	      : set_of_list evs;
	    Says Tgs' A (Crypt AuthKey {|Key ServKey, Agent B, Timestamp Tt, ServTicket|})
	      : set_of_list evs;
	    Tt <= Ta1 + RecentResp |]

	==>  Says A B {|ServTicket, (Crypt ServKey {|Agent A, Timestamp (CT evs)|})|}
	        # evs : kerberos



K6 	[| evs : kerberos; A ~: B;
	   Says A' B {|(Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Timestamp Tt|}),
		 	   (Crypt ServKey {|Agent A, Timestamp Ta2|})|}
	     : set_of_list evs;
	   (CT evs) <= Tt + ServLife;
	   (CT evs) <= Ta2 + RecentAuth |]

	==>  Says B A (Crypt ServKey (Timestamp Ta2)) # evs : kerberos



Oops1 	 [| evs : kerberos; A ~: Spy:
	    Says Kas' A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Timestamp Tk, AuthTicket|})
	      : set_of_list evs |]

	 ==> Says A Spy {|Agent A, Agent Tgs, Timestamp Tk, Key AuthKey|} # evs :  kerberos



Oops2    [| evs : kerberos; A ~: Spy;
	    Says Tgs' A (Crypt AuthKey {|Key ServKey, Agent B, Timestamp Tt, ServTicket|})
              : set_of_list evs |]

	 ==> Says A Spy {|Agent A, Agent B, Timestamp Tt, Key ServKey|} # evs : kerberos