next up previous
Next: About this document Up: Using Isabelle to Prove Previous: References

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


next up previous
Next: About this document Up: Using Isabelle to Prove Previous: References

Giampaolo Bella
Mon Aug 4 18:43:12 BST 1997