Information Technology Reference
In-Depth Information
4. Gordon, M.J.C. and Melham, T.F.: Introduction to HOL: A Theorem Proving En-
vironment for Higher Order Logic. Cambridge University Press, New York (1993)
5. Butler Lampson and Martin Abadi and Michael Burrows and Edward Wobber:
Authentication in Distributed Systems: Theory and Practice. ACM Transactions
on Computer Systems, Vol. 10, no 4 (November 1992) 265-310
6. Robin Milner and Mads Tofte and Robert Harper and David MacQueen: The
Definition of Standard ML (Revised). MIT Press (1997)
7. Lawrence C. Paulson: Isabelle: A Generic Theorem Prover. Springer, Lecture Notes
in Computer Science 828 (1994)
8. Edward Wobber and Martin Abadi and Michael Burrows and Butler Lampson:
Authentication in the Taos Operating System. ACM Transactions on Computer
Systems, Vol. 12, no 1 (February 1994) 3-32
A Theorems
We include a partial list of the axioms and derivable theorems of the authenti-
cation logic we have proved in HOL. The axioms included here correspond to
those given in the appendix of [5].
val S2Thm =
∀s1 s2.
( ∀World w0 Ifn Jfn w1. (( World,w0,Ifn,Jfn),w1) MD s1) ∧
( ∀World w0 Ifn Jfn w1. (( World,w0,Ifn,Jfn),w1) MD ( s1 imps s2)) ⊃
∀World w0 Ifn Jfn w1. (( World,w0,Ifn,Jfn),w1) MD s2 : thm
val S3˙2Thm =
∀World w0 Ifn Jfn w1 P s1 s2.
(( World,w0,Ifn,Jfn),w1) MD
((( P says s1) ands P says s1 imps s2) imps P says s2) : thm
val S4Thm =
∀s.
( ∀World w0 Ifn Jfn w1. (( World,w0,Ifn,Jfn),w1) MD s) ⊃
∀P World w0 Ifn Jfn w1. (( World,w0,Ifn,Jfn),w1) MD ( P says s) : thm
val S5Thm =
∀P s1 s2 World w0 Ifn Jfn w1.
(( World,w0,Ifn,Jfn),w1) MD
(( P says s1 ands s2) eqs ( P says s1) ands P says s2) : thm
val P1Thm =
∀P Q s World w0 Ifn Jfn w1.
(( World,w0,Ifn,Jfn),w1) MD
((( P meet Q) says s) eqs ( P says s) ands Q says s) : thm
val P2Thm =
∀P Q s World w0 Ifn Jfn w1.
(( World,w0,Ifn,Jfn),w1) MD
((( P quoting Q) says s) eqs P says Q says s) : thm
val P3Thm =
∀P Q s World w0 Ifn Jfn w1.
(( World,w0,Ifn,Jfn),w1) MD
(( P eqp Q) imps ( P says s) eqs Q says s) : thm
Search WWH ::




Custom Search