[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
SvO Logic imp.: Applying rule to tautologies only.
- To: pvs-help@csl.sri.com
- Subject: SvO Logic imp.: Applying rule to tautologies only.
- From: Justin Childs <childs@nu.cs.fsu.edu>
- Date: Thu, 13 Apr 2000 19:23:30 -0400 (EDT)
- Delivery-Date: Thu Apr 13 16:24:13 2000
I am attempting to adapt the Syverson van Oorschot cryptographic
protocol logic [1] so it can be utilized with PVS . The adaption of a
cyptographic protocol [2] has been done before with the BAN logic [3]. I
have attached a pvs file used to analyze a protocol with BAN logic in PVS.
In this specification, axioms are used to represent the logical postulates
of BAN.
The SvO logic has an additional features not present in BAN. It has
two inference rules and a list of axioms instead of one set of logical
postulates. The second inference rule in SvO called necessitation causes
a difficulty. Here is necessitation: From |- X infer |- P believes X.
Where X is a formula for specifying cryptographic properties and P is a
participant in the protocol. Here is a text fragment describing this
rule.
"`|-' is a metalinguitic symbol (usually pronounced turnstile). `X
|- Y' means that Y is derivable from the set of formulae X (and the
axioms stated below). `'|- Y' means that Y is a theorem, i.e.,
derivable from axioms alone. We describe derivability (i.e. proofs)
below in 1.3. Axioms are all instances of tautologies of classical
propositional calculus, and all instances of the following axiom
schemata:
Believing - For any principal P and formulae Y and Z,
1. P believes Y & P believes (Y -> Z) -> P believes Z
2. P believes Y -> P believes (P believes Y)
..."
In the BAN logic adaption to PVS, the axioms used to implement the
logical postulates could be attached to the conjecture for a cyptographic
protocol with the lemma rule of PVS. The SvO logic poses a problem
however, the necessitation rule can only be applied to theorems. It may
not be applied to any of the formulae found in the conjecture for a
protocol. This is the crux, what kind of structure or type would permit
the necessitation rule to be applied to the axioms of SvO without it being
applied to the formulae found in a conjecture? Any help, comments, or
suggestions are greatly appreciated. Web sites for the
[1] Paul F. Syverson and Paul C. van Oorschot. On Unifying Some
Cryptographic Protocol Logics. In Proceedings of the 1994 IEEE Computer
Society Symposium on Research in Security and Privacy, pages 14-28. IEEE
Computer Society Press, Los Alamitos, California, 1994.
http://chacs.nrl.navy.mil/publications/CHACS/1994/1994syverson-sp.ps
[2] A Framework for A Protocol Evaluation Workbench , Alec Yasinsac and Wm
A. Wulf, Proceedings of the Fourth IEEE International High Assurance
Systems Engineering Symposium (HASE) '99, Nov 17-19, 1999, Washington,
D.C., IEEE Computer Society Press.
http://www.cs.fsu.edu/~yasinsac/framewk.ps
[3] A logic of authentication. Michael Burrows, Martin Abadi, and Roger M.
Needham. (February, 1989). DEC research report. Also in other
presentations.
http://gatekeeper.dec.com/pub/DEC/SRC/research-reports/abstracts/src-rr-039.html
p.s. In case you are really feeling helpful I have included the proof
file for the above pvs file. I would appreciate suggestions that would
indicate ways of automating this proof in PVS.
Thank You.
Justin Childs CS Graduate Student
Florida State University Tallahassee, Florida
childs@cs.fsu.edu www.cs.fsu.edu/~childs
% PVS Entries for BAN Logic Rules
carl2ban : THEORY BEGIN
fresh: PRED[[bool]]
e,d,ep,dp,signature,cat: PRED[[bool,bool]]
believes,sees,said,controls,goodkey,pubkey: PRED[[bool,bool]]
goodkey,secret: PRED[[bool,bool,bool]]
B_B,A_A,S_Kab,B_Nib,A_Na,A_S,B_S,B_Nb,S_Kbs,S_Kas: bool
% Ban Rules of inference
msg_m1: AXIOM FORALL (P,Q,KPQ,X: bool):
believes(P,(goodkey(P,KPQ,Q))) AND sees(P,e(X,KPQ)) IMPLIES
believes(P,said(Q,X))
msg_m2: AXIOM FORALL (P,Q,PUB_Q, PUB_Q_INV, X:bool): % For public keys -
believes(P,pubkey(Q,PUB_Q)) and sees(P,e(X,PUB_Q_INV))
IMPLIES believes(P,said(Q,X))
% Note: I am not completely satisfied with msg_m2. May want to add assumed
% relationship between K and K-.
msg_m3: AXIOM FORALL (P,Q,Y,X:bool): % For shared secrets
believes(P,secret(Q,Y,P)) and sees(P,signature(X,Y)) IMPLIES
believes(P,said(Q,X))
N_verif: AXIOM FORALL (P,Q,X: bool):
believes(P,fresh(X)) and believes(P,said(Q,X)) IMPLIES
believes(P,believes(Q,X))
juris: AXIOM FORALL (P,Q,X: bool):
believes(P,controls(Q,X)) and believes(P,believes(Q,X))
IMPLIES believes(P,X)
sees1: AXIOM FORALL (P,X,Y: bool): sees(P,cat(X,Y)) IMPLIES
sees(P,X) and sees(P,Y)
sees2: AXIOM FORALL (P,X,Y: bool): sees(P,signature(X,Y)) IMPLIES sees(P,X)
sees3: AXIOM FORALL (P,Q,PUB_P,X: bool):
believes(P,pubkey(P,PUB_P)) and sees(P,e(X,PUB_P)) IMPLIES sees(P,X)
sees4: AXIOM FORALL (P,Q,X,KPQ: bool):
believes(P,goodkey(P,KPQ,Q)) and sees(P,e(X,KPQ)) IMPLIES sees(P,X)
sees5: AXIOM FORALL (P,Q,PUB_Q,PUB_Q_INV,X: bool):
believes(P,pubkey(Q,PUB_Q)) and sees(P,e(X,PUB_Q_INV)) IMPLIES
sees(P,X)
fresh1: AXIOM FORALL (P,X,Y: bool):
believes(P,fresh(X)) AND sees(P,cat(X,Y)) IMPLIES
believes(P,fresh(cat(X,Y)))
belief1: AXIOM FORALL (P, X, Y: bool):
believes(P, cat(X, Y)) IMPLIES believes(P, X) AND believes(P, Y)
belief2: AXIOM FORALL (P, Q, X, Y: bool):
believes(P, believes(Q, cat(X, Y))) IMPLIES
believes(P, believes(Q, X)) AND believes(P, believes(Q, Y))
belief_cat: AXIOM FORALL (P, X, Y: bool):
believes(P, X) AND believes(P, Y) IMPLIES believes(P, cat(X, Y))
said1: AXIOM FORALL (P, Q, X, Y: bool):
believes(P, said(Q, cat(X, Y))) IMPLIES
believes(P, said(Q, X)) AND believes(P, said(Q, Y))
% PVS Supplement for BAN Logic Rules
fresh1b: AXIOM FORALL (P,X,Y: bool):
believes(P, fresh(X)) OR believes(P,fresh(Y)) IMPLIES
believes(P,fresh(cat(X,Y)))
sees_enc: AXIOM FORALL (P,X,Y,K: bool):
sees(P,e(cat(X,Y),K)) IMPLIES sees(P,e(X,K)) and sees(P,e(Y,K))
belief_sym: AXIOM FORALL (P,Q,k: bool):
believes(P,goodkey(Q,k,P)) IMPLIES believes(P,goodkey(P,k,Q))
said_sym: AXIOM FORALL (P,Q,R,T,k:bool):
believes(P,said(Q,goodkey(R,k,T))) IMPLIES
believes(P,said(Q,goodkey(T,k,R)))
cont_sym: AXIOM FORALL (P,Q,R,k: bool):
believes(P,controls(Q,goodkey(P,k,R))) IMPLIES
believes(P,controls(Q,goodkey(R,k,P)))
carl2: CONJECTURE
(((((((((((((((((((((((((believes(B_B,believes(A_A,goodkey(A_A,S_Kab,B_B)))
or
not ((not (believes(B_B,said(A_A,B_Nib)))
or
believes(B_B,said(A_A,cat(B_Nib,goodkey(A_A,S_Kab,B_B))))))
)
or
not (sees(B_B,B_Nib))
)
or
not (sees(B_B,e(B_Nib,S_Kab)))
)
and
believes(A_A,believes(B_B,goodkey(A_A,S_Kab,B_B))))
or
not ((not (believes(A_A,said(B_B,A_Na)))
or
believes(A_A,said(B_B,cat(A_Na,goodkey(A_A,S_Kab,B_B))))))
)
or
not (sees(A_A,A_Na))
)
or
not ((not (believes(A_A,said(A_S,cat(A_Na,cat(B_B,S_Kab)))))
or
believes(A_A,said(A_S,cat(A_Na,cat(goodkey(A_A,S_Kab,B_B),fresh(goodkey(A_A,S_Kab,B_B))))))))
)
or
not (believes(A_A,controls(A_S,goodkey(A_A,S_Kab,B_B))))
)
or
not (believes(A_A,controls(A_S,fresh(goodkey(A_A,S_Kab,B_B)))))
)
or
not (sees(A_A,cat(A_Na,cat(B_B,S_Kab))))
)
or
not (sees(A_A,cat(e(cat(A_Na,cat(B_B,S_Kab)),S_Kas),cat(e(A_Na,S_Kab),B_Nib))))
)
or
not (sees(A_A,cat(e(cat(A_Na,cat(B_B,S_Kab)),S_Kas),cat(e(A_Na,S_Kab),B_Nib))))
)
or
not (believes(B_B,fresh(B_Nib)))
)
or
not (fresh(B_Nib))
)
or
not ((not (believes(B_B,said(B_S,cat(S_Kab,cat(B_Nb,A_A)))))
or
believes(B_B,said(B_S,cat(B_Nb,cat(goodkey(A_A,S_Kab,B_B),fresh(goodkey(A_A,S_Kab,B_B))))))))
)
or
not (believes(B_B,controls(B_S,goodkey(A_A,S_Kab,B_B))))
)
or
not (believes(B_B,controls(B_S,fresh(goodkey(A_A,S_Kab,B_B)))))
)
or
not (sees(B_B,cat(S_Kab,cat(B_Nb,A_A))))
)
or
not (sees(B_B,cat(e(cat(S_Kab,cat(B_Nb,A_A)),S_Kbs),e(cat(A_Na,cat(B_B,S_Kab)),S_Kas))))
)
or
not (believes(B_B,fresh(B_Nb)))
)
or
not (fresh(B_Nb))
)
or
not (believes(A_A,fresh(A_Na)))
)
or
not (fresh(A_Na))
)
or
not (believes(B_B,goodkey(B_B,S_Kbs,B_S)))
)
or
not (believes(A_A,goodkey(A_A,S_Kas,A_S)))
)
END carl2ban
(|carl2ban|
(|carl2| "" (FLATTEN)
(("" (SPLIT +)
(("1" (FLATTEN)
(("1"
(LEMMA "belief2"
("P" "B_B" "Q" "A_A" "X" "B_Nib" "Y"
"goodkey(A_A, S_Kab, B_B)"))
(("1" (SPLIT -1)
(("1" (FLATTEN) NIL NIL)
("2"
(LEMMA "N_verif"
("P" "B_B" "Q" "A_A" "X"
"cat(B_Nib, goodkey(A_A, S_Kab, B_B))"))
(("2" (SPLIT -1)
(("1" (PROPAX) NIL NIL)
("2"
(LEMMA "fresh1b"
("P" "B_B" "X" "B_Nib" "Y"
"goodkey(A_A, S_Kab, B_B)"))
(("2" (SPLIT -1)
(("1" (PROPAX) NIL NIL) ("2" (FLATTEN) NIL NIL))
NIL))
NIL)
("3" (SPLIT -1)
(("1"
(LEMMA "msg_m1"
("P" "B_B" "Q" "A_A" "KPQ" "S_Kab" "X" "B_Nib"))
(("1" (SPLIT -1)
(("1" (PROPAX) NIL NIL)
("2"
(LEMMA "belief_sym"
("P" "B_B" "Q" "A_A" "k" "S_Kab"))
(("2" (SPLIT -1)
(("1" (PROPAX) NIL NIL)
("2"
(LEMMA "juris"
("P" "B_B" "Q" "B_S" "X"
"goodkey(A_A, S_Kab, B_B)"))
(("2" (SPLIT -1)
(("1" (PROPAX) NIL NIL)
("2" (PROPAX) NIL NIL)
("3"
(LEMMA "belief2"
("P"
"B_B"
"Q"
"B_S"
"X"
"goodkey(A_A, S_Kab, B_B)"
"Y"
"fresh(goodkey(A_A, S_Kab, B_B))"))
(("3"
(SPLIT -1)
(("1" (FLATTEN) NIL NIL)
("2"
(LEMMA
"belief2"
("P"
"B_B"
"Q"
"B_S"
"X"
"B_Nb"
"Y"
"cat(goodkey(A_A, S_Kab, B_B), fresh(goodkey(A_A, S_Kab, B_B)))"))
(("2"
(SPLIT -1)
(("1" (FLATTEN) NIL NIL)
("2"
(LEMMA
"N_verif"
("P"
"B_B"
"Q"
"B_S"
"X"
"cat(B_Nb, cat(goodkey(A_A, S_Kab, B_B),fresh(goodkey(A_A, S_Kab, B_B))))"))
(("2"
(SPLIT -1)
(("1" (PROPAX) NIL NIL)
("2"
(LEMMA
"fresh1b"
("P"
"B_B"
"X"
"B_Nb"
"Y"
"cat(goodkey(A_A, S_Kab, B_B), fresh(goodkey(A_A, S_Kab, B_B)))"))
(("2"
(SPLIT -1)
(("1" (PROPAX) NIL NIL)
("2" (FLATTEN) NIL NIL))
NIL))
NIL)
("3"
(SPLIT -13)
(("1"
(LEMMA
"msg_m1"
("P"
"B_B"
"Q"
"B_S"
"KPQ"
"S_Kbs"
"X"
"cat(S_Kab, cat(B_Nb, A_A))"))
(("1"
(SPLIT -1)
(("1" (PROPAX) NIL NIL)
("2" (PROPAX) NIL NIL)
("3"
(LEMMA
"sees1"
("P"
"B_B"
"X"
"e(cat(S_Kab, cat(B_Nb, A_A)), S_Kbs)"
"Y"
"e(cat(A_Na, cat(B_B, S_Kab)), S_Kas)"))
(("3"
(SPLIT -1)
(("1"
(FLATTEN)
NIL
NIL)
("2"
(PROPAX)
NIL
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (PROPAX) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("3" (PROPAX) NIL NIL))
NIL))
NIL)
("2" (PROPAX) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2"
(LEMMA "belief2"
("P" "A_A" "Q" "B_B" "X" "A_Na" "Y" "goodkey(A_A, S_Kab, B_B)"))
(("2" (SPLIT -1)
(("1" (FLATTEN) NIL NIL)
("2"
(LEMMA "N_verif"
("P" "A_A" "Q" "B_B" "X"
"cat(A_Na, goodkey(A_A, S_Kab, B_B))"))
(("2" (SPLIT -1)
(("1" (PROPAX) NIL NIL)
("2"
(LEMMA "fresh1b"
("P" "A_A" "X" "A_Na" "Y" "goodkey(A_A, S_Kab, B_B)"))
(("2" (SPLIT -1)
(("1" (PROPAX) NIL NIL) ("2" (FLATTEN) NIL NIL)) NIL))
NIL)
("3" (SPLIT -1)
(("1"
(LEMMA "msg_m1"
("P" "A_A" "Q" "B_B" "KPQ" "S_Kab" "X" "A_Na"))
(("1" (SPLIT -1)
(("1" (PROPAX) NIL NIL)
("2"
(LEMMA "juris"
("P" "A_A" "Q" "A_S" "X"
"goodkey(A_A, S_Kab, B_B)"))
(("2" (SPLIT -1)
(("1" (PROPAX) NIL NIL) ("2" (PROPAX) NIL NIL)
("3"
(LEMMA "belief2"
("P" "A_A" "Q" "A_S" "X"
"goodkey(A_A, S_Kab, B_B)" "Y"
"fresh(goodkey(A_A, S_Kab, B_B))"))
(("3" (SPLIT -1)
(("1" (FLATTEN) NIL NIL)
("2"
(LEMMA "belief2"
("P" "A_A" "Q" "A_S" "X" "A_Na" "Y"
"cat(goodkey(A_A, S_Kab, B_B), fresh(goodkey(A_A, S_Kab, B_B)))"))
(("2" (SPLIT -1)
(("1" (FLATTEN) NIL NIL)
("2"
(LEMMA
"N_verif"
("P"
"A_A"
"Q"
"A_S"
"X"
"cat(A_Na,cat(goodkey(A_A, S_Kab, B_B),fresh(goodkey(A_A, S_Kab, B_B))))"))
(("2"
(SPLIT -1)
(("1" (PROPAX) NIL NIL)
("2"
(LEMMA
"fresh1b"
("P"
"A_A"
"X"
"A_Na"
"Y"
"cat(goodkey(A_A, S_Kab, B_B),fresh(goodkey(A_A, S_Kab, B_B)))"))
(("2"
(SPLIT -1)
(("1" (PROPAX) NIL NIL)
("2" (FLATTEN) NIL NIL))
NIL))
NIL)
("3"
(SPLIT -2)
(("1"
(LEMMA
"msg_m1"
("P"
"A_A"
"Q"
"A_S"
"KPQ"
"S_Kas"
"X"
"cat(A_Na, cat(B_B, S_Kab))"))
(("1"
(SPLIT -1)
(("1" (PROPAX) NIL NIL)
("2" (PROPAX) NIL NIL)
("3"
(LEMMA
"sees1"
("P"
"A_A"
"X"
"e(cat(A_Na, cat(B_B, S_Kab)), S_Kas)"
"Y"
"cat(e(A_Na, S_Kab), B_Nib)"))
(("3"
(SPLIT -1)
(("1" (FLATTEN) NIL NIL)
("2" (PROPAX) NIL NIL))
NIL))
NIL))
NIL))
NIL)
("2" (PROPAX) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("3"
(LEMMA "sees1"
("P" "A_A" "X" "e(A_Na, S_Kab)" "Y" "B_Nib"))
(("3" (SPLIT -1)
(("1" (FLATTEN) NIL NIL)
("2"
(LEMMA "sees1"
("P" "A_A" "X"
"e(cat(A_Na, cat(B_B, S_Kab)), S_Kas)" "Y"
"cat(e(A_Na, S_Kab), B_Nib)"))
(("2" (SPLIT -1)
(("1" (FLATTEN) NIL NIL)
("2" (PROPAX) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (PROPAX) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))