SendReceive = spec type Action type Agent type Term (* Action is a sending by Agent of Term *) op send : Action * Agent * Term -> Boolean (* Action is a receiving by Agent of Term *) op receive : Action * Agent * Term -> Boolean axiom SendIsOneToOne is fa(sending,sender1,sender2,term1,term2) send(sending,sender1,term1) & send(sending,sender2,term2) => sender1 = sender2 & term1 = term2 axiom ReceiveIsOneToOne is fa(receiving,receiver1,receiver2,term1,term2) receive(receiving,receiver1,term1) & receive(receiving,receiver2,term2) => receiver1 = receiver2 & term1 = term2 axiom SendAndReceiveAreDistinct is fa(action,agent1,agent2,term1,term2) ~(send(action,agent1,term1) & receive(action,agent2,term2)) (* precedes is the ordering relation on actions. *) op precedes infixl 20 : Action * Action -> Boolean (* precedes is irreflexive, asymmetric, and transitive *) axiom IrrefexivityOfPrecedes is fa(action) ~(action precedes action) axiom AsymmetryOfPrecedes is fa(action1, action2) action1 precedes action2 => ~(action2 precedes action1) axiom TransitivityOfPrecedes is fa(action1,action2,action3) (action1 precedes action2 & action2 precedes action3) => action1 precedes action3 (* Every receive is preceded by an earlier send *) op earlierSending : Action * Agent * Term -> Action op earlierSender : Action * Agent * Term -> Agent axiom Rcv is fa(receiving,receiver,term) receive(receiving,receiver,term) => (send(earlierSending(receiving,receiver,term), earlierSender(receiving,receiver,term), term) & earlierSending(receiving,receiver,term) precedes receiving) (* We could have used an existential quantifier instead of explicit functions earlierSending and earlierSender here. This way we avoid the appearance of Skolem functions in the proof, but the two representation are equivalent. *) (* inside is the (reflexive) subterm relation *) op inside infixl 20 : Term * Term -> Boolean axiom InsideIsReflexive is fa(t) t inside t axiom TransitivityOfInside is fa(t1,t2,t3) (t1 inside t2 & t2 inside t3) => t1 inside t3 (* Action is a sending by Agent of a message that contains Term. *) op sendIn : Action * Agent * Term -> Boolean axiom DefinitionOfSendIn is fa(sending,sender,t0) sendIn(sending,sender,t0) <=> (ex(t1) send(sending,sender,t1) & t0 inside t1) conjecture ThmSendInIsMonotonic is fa(sending,sender,t0,t1) sendIn(sending,sender,t1) & t0 inside t1 => sendIn(sending,sender,t0) (* Action is a receiving by Agent of a message that contains Term.*) op receiveIn : Action * Agent * Term -> Boolean axiom DefinitionOfReceiveIn is fa(receiving, receiver,t0) receiveIn(receiving,receiver,t0) <=> (ex (t1) receive(receiving,receiver,t1) & t0 inside t1) conjecture ThmReceiveInIsMonotonic is fa(receiving,receiver,t0,t1) receiveIn(receiving,receiver,t1) & t0 inside t1 => receiveIn(receiving,receiver,t0) (* Receipt of a message containing a term is preceded by the sending of a message containing that term. *) conjecture ThmRcvIn is fa(receiving,receiver,term) receiveIn(receiving,receiver,term) => (ex(sending,sender) sendIn(sending,sender,term) & sending precedes receiving) (* A minimal sending of a message containing a term is not preceded by any other such sending *) op minSendIn: Action * Agent * Term -> Boolean axiom DefinitionOfMinSendIn is fa(sending,sender,term) minSendIn(sending,sender,term) <=> (sendIn(sending,sender,term) & (fa(sending1,sender1) sendIn(sending1,sender1,term) => ~(sending1 precedes sending))) (* Any sending of a message containing a term is preceded by a minimal such sending. *) op minSending : Action * Agent * Term -> Action op minSender : Action * Agent * Term -> Agent axiom SendingPrecededByMinimalSending is fa(sending,sender,t) sendIn(sending,sender,t) => (minSendIn(minSending(sending,sender,t), minSender(sending,sender,t), t) & (minSending(sending,sender,t) precedes sending || minSending(sending,sender,t) = sending)) conjecture ThmReceivingPrecededByMinimalSending is fa(receiving,receiver,t) receiveIn(receiving,receiver,t) => (ex(sending,sender) minSendIn(sending,sender,t) & sending precedes receiving) (*A first sending of a message containing a term precedes all others. *) op firstSendIn: Action * Agent * Term -> Boolean axiom DefinitionOfFirstSendIn is fa(sending,sender,term) firstSendIn(sending,sender,term) <=> sendIn(sending,sender,term) & (fa(sending1,sender1) sendIn(sending1,sender1,term) => (sending precedes sending1 || sending = sending1)) conjecture ThmFirstImpliesMinSendIn is fa(sending,sender,term) firstSendIn(sending,sender,term) => minSendIn(sending,sender,term) op pair : Term * Term -> Term axiom PairIsOneToOne is fa(s1,s2,t1,t2) pair(s1,s2) = pair(t1,t2) => s1 = t1 & s2 = t2 axiom ComponentsInsidePair is fa(t1,t2) inside(t1, pair(t1,t2)) & inside(t2, pair(t1,t2)) (* The first sending of a message containing a term precedes any receiving of such a message *) conjecture ThmFirstSendInPrecedesReceiveIn is fa(sending,sender,receiving,receiver,t) firstSendIn(sending,sender,t) & receiveIn(receiving,receiver,t) => sending precedes receiving def proverOptions = "(use-resolution nil) (use-hyperresolution t) (use-negative-hyperresolution t) (use-paramodulation) (use-factoring) (use-literal-ordering-with-hyperresolution 'literal-ordering-p) (use-literal-ordering-with-negative-hyperresolution 'literal-ordering-n) (use-literal-ordering-with-resolution 'literal-ordering-a) (use-literal-ordering-with-paramodulation 'literal-ordering-a) (declare-ordering-greaterp 'snark::|firstSendIn| 'snark::|precedes| 'snark::|sendIn| 'snark::|inside| 'snark::|send| 'snark::|minSendIn|) (variable-weight 6) (use-ac-connectives) (run-time-limit 90) (assert-supported nil) (use-code-for-numbers nil) (print-symbol-ordering) (print-rows-when-processed nil) (print-final-rows)" endspec Nonce = spec import SendReceive (* Nonces are special terms with the property that they have a unique origin. *) op nonce? : Term -> Boolean type Nonce = {t : Term | nonce? t} (* The creator is the originator of the nonce. *) op creator : Nonce -> Agent (* The firstSending is the earliest sending of the term *) op firstSending : Action * Agent * Nonce -> Action axiom NonceFirstSending is fa(sending,sender,nonce:Nonce) sendIn(sending,sender,nonce) => firstSendIn(firstSending(sending,sender,nonce), creator(nonce), nonce) (* If a nonce has been sent by someone other than its creator, that agent has previously received the nonce after the creator has sent it. *) axiom NonceOtherSending is fa(nonce:Nonce,sending,agent) agent ~= creator(nonce) & sendIn(sending,agent,nonce) => (ex(receiving) receiveIn(receiving,agent,nonce) & firstSending(sending,agent,nonce) precedes receiving & receiving precedes sending) conjecture ThmNonceFirstSendPrecedesSending is fa(sending,sender,nonce:Nonce) sendIn(sending,sender,nonce) => (firstSending(sending,sender,nonce) precedes sending || firstSending(sending,sender,nonce) = sending) conjecture ThmNonceFirstSendPrecedesReceiving is fa(receiving,receiver,nonce:Nonce) receiveIn(receiving,receiver,nonce) => (ex(sending) firstSendIn(sending,creator(nonce),nonce) & sending precedes receiving) (* out---increased proof times conjecture ThmNonceMinImpliesFirstSendIn is fa(sending,sender,nonce:Nonce) minSendIn(sending,sender,nonce) => firstSendIn(sending,sender,nonce) *) def proverNonceOptions = "(use-resolution nil) (use-hyperresolution t) (use-negative-hyperresolution t) (use-paramodulation) (use-factoring) (use-literal-ordering-with-hyperresolution 'literal-ordering-p) (use-literal-ordering-with-negative-hyperresolution 'literal-ordering-n) (use-literal-ordering-with-resolution 'literal-ordering-a) (use-literal-ordering-with-paramodulation 'literal-ordering-a) (declare-ordering-greaterp 'snark::|nonce?| 'snark::|firstSendIn| 'snark::|precedes| 'snark::|sendIn| 'snark::|inside| 'snark::|send| 'snark::|minSendIn|) (variable-weight 6) (use-ac-connectives) (run-time-limit 60) (assert-supported nil) (use-code-for-numbers nil) (print-symbol-ordering) (print-rows-when-processed nil) (print-final-rows)" endspec Hash = spec import Nonce (* hash is a keyed hash function *) op hash : Agent * Agent * Term -> Term axiom HashIsOneToOne is fa(agentA1,agentB1,t1,agentA2,agentB2,t2) hash(agentA1,agentB1,t1) = hash(agentA2,agentB2,t2) => agentA1 = agentA2 & agentB1 = agentB2 & t1 = t2 (* A minimal sending of a message containing a keyed hash must be by one of the principals of the hash. *) axiom SenderOfHash is fa(sending,sender,agentA,agentB,t) minSendIn(sending,sender,hash(agentA,agentB,t)) => (sender = agentA || sender = agentB) axiom HashContainsTerm is fa(agentA,agentB,t) t inside hash(agentA,agentB,t) conjecture HashedPairContainsComponents is fa(agentA,agentB,t1,t2) t1 inside hash(agentA,agentB,pair(t1,t2)) & t2 inside hash(agentA,agentB,pair(t1,t2)) endspec A_AuthenticationSpec = spec import HashPlus conjecture A_Authentication is fa(agentB,m:Nonce,n:Term,sendingM,receivingPair) (* Alice doesn't forge Bob's hash: *) ~(ex(sillySending,t) (sendIn(sillySending,creator(m),hash(agentB,creator(m),pair(m,n))) )) (* Bob only sends the hash in the context of a pair. The second component of the pair is a nonce he creates: *) & (fa(honestSending) minSendIn(honestSending,agentB, hash(agentB,creator(m),pair(m,n))) => firstSendIn(honestSending,agentB, pair(n,hash(agentB,creator(m),pair(m,n)))) & nonce?(n) & agentB = creator(n) ) (* Alice is the first sender of nonce m: *) & firstSendIn(sendingM,creator(m),m) (* Alice receives the hashed pair of nonces: *) & receiveIn(receivingPair,creator(m), hash(agentB,creator(m),pair(m,n))) => (ex(receivingM,sendingPair) (* Bob has received the nonce m: *) receiveIn(receivingM,agentB,m) (* Bob creates the nonce n: *) & nonce?(n) & agentB = creator(n) (* Bob is the first sender of the pair. *) & firstSendIn(sendingPair,agentB,pair(n,hash(agentB,creator(m),pair(m,n)))) (* These events occur in order: *) & sendingM precedes receivingM & receivingM precedes sendingPair & sendingPair precedes receivingPair ) op agentA : Agent op agentB : Agent op m : Nonce op n : Term op sendingM : Action op receivingPair : Action axiom A_Authentication_Supported is (* Alice is the creator of nonce m: *) agentA = creator(m) (* Alice receives the hashed pair of nonces: *) & receiveIn(receivingPair,agentA, hash(agentB,agentA,pair(m,n))) axiom A_Authentication_Hyp is (* Alice doesn't forge Bob's hash: *) ~(ex(sillySending) (sendIn(sillySending,agentA,hash(agentB,agentA,pair(m,n))) )) (* Bob only sends the hash in the context of a pair. The second component of the pair is a nonce he creates: *) & (fa(honestSending) minSendIn(honestSending,agentB, hash(agentB,agentA,pair(m,n))) => firstSendIn(honestSending,agentB, pair(n,hash(agentB,agentA,pair(m,n)))) & nonce?(n) & agentB = creator(n) ) (* Alice is the first sender of nonce m: *) & firstSendIn(sendingM,agentA,m) conjecture A_Authentication1 is (ex(receivingM,sendingPair) (* Bob has received the nonce m: *) receiveIn(receivingM,agentB,m) (* Bob creates the nonce n: *) & nonce?(n) & agentB = creator(n) (* Bob is the first sender of the pair. *) & firstSendIn(sendingPair,agentB,pair(n,hash(agentB,agentA,pair(m,n)))) (* These events occur in order: *) & sendingM precedes receivingM & receivingM precedes sendingPair & sendingPair precedes receivingPair ) def proverAuthOptions = "(use-resolution nil) (use-hyperresolution t) (use-negative-hyperresolution t) (use-paramodulation) (use-factoring) (use-literal-ordering-with-hyperresolution 'literal-ordering-p) (use-literal-ordering-with-negative-hyperresolution 'literal-ordering-n) (use-literal-ordering-with-resolution 'literal-ordering-a) (use-literal-ordering-with-paramodulation 'literal-ordering-a) (declare-ordering-greaterp 'snark::|nonce?| 'snark::|firstSendIn| 'snark::|precedes| 'snark::|sendIn| 'snark::|inside| 'snark::|send| 'snark::|minSendIn|) (declare-ordering-greaterp 'snark::|agentA| 'snark::|creator|) (declare-ordering-greaterp 'snark::|agentA| 'snark::|m|) (variable-weight 6) (use-ac-connectives) (run-time-limit 60) (assert-supported nil) (use-code-for-numbers nil) (print-symbol-ordering) (print-rows-when-processed nil) (print-final-rows)" endspec B_AuthenticationSpec = spec import HashPlus conjecture B_Authentication is fa(agentA,n:Nonce,m:Term,receivingM,sendingPair,receivingN) (* Bob does not forge Alice's hash: *) ~(ex(sillySending,t) sendIn(sillySending,creator(n),hash(agentA,creator(n),n))) (* If Alice has sent the hashed nonce n, she has previously sent the nonce m and then received the pair: *) & (fa(honestSending) sendIn(honestSending,agentA,hash(agentA,creator(n),n)) => (ex(sendingM,receivingPair) firstSendIn(sendingM,agentA,m) & receiveIn(receivingPair,agentA, pair(n,hash(creator(n),agentA,pair(m,n)))) & nonce?(m) & agentA = creator(m) & sendingM precedes receivingPair & receivingPair precedes honestSending)) (* Bob has received the nonce m: *) & receiveIn(receivingM,creator(n),m) (* Bob has originated n and sent it with the hashed pair of nonces: *) & firstSendIn(sendingPair,creator(n), pair(n,hash(creator(n),agentA,pair(m,n)))) (* Bob has received the hashed nonce n: *) & receiveIn(receivingN,creator(n),hash(agentA,creator(n),n)) (* These events have occurred in order: *) & receivingM precedes sendingPair & sendingPair precedes receivingN => (ex(sendingM,sendingN,receivingPair,senderN) (* Alice is the originator and sender of nonce m: *) firstSendIn(sendingM,agentA,m) (* Alice has received the pair: *) & receiveIn(receivingPair,agentA, pair(n,hash(creator(n),agentA,pair(m,n)))) (* m is a nonce and Alice is its creator *) & nonce?(m) & agentA = creator(m) (* Alice is a minimal sender of the hashed nonce n: *) & minSendIn(sendingN,agentA,hash(agentA,creator(n),n)) (* Alice has received the nonce n: *) & receiveIn(receivingPair,agentA,n) (* These events have occurred in order: *) & sendingM precedes receivingM & sendingPair precedes receivingPair & receivingPair precedes sendingN & sendingN precedes receivingN) endspec HashPlus = spec import Hash (* We introduce two functions, identityChallenge and hashResponse, to serve as images for challenge and response, respectively, in the CRH morphism. *) op identityChallenge : Agent * Agent * Term -> Term op hashResponse : Agent * Agent * Term -> Term axiom DefinitionOfIdentityChallenge is fa(agentA,agentB,s) identityChallenge(agentA,agentB,s) = s axiom DefinitionOfHashResponse is fa(agentA,agentB,s) hashResponse(agentA,agentB,s) = hash(agentB,agentA,s) op pairChallenge : Agent * Agent * Term -> Term op pairResponse : Agent * Agent * Term -> Term axiom DefinitionOfPairChallenge is fa(agent1,agent2,n) pairChallenge(agent1,agent2,n) = n axiom DefinitionOfPairResponse is fa(agent1,agent2,n,m) pairResponse(agent1,agent2,n) = hash(agent2,agent1,n) def proverHashOptions = "(use-resolution nil) (use-hyperresolution t) (use-negative-hyperresolution t) (use-paramodulation) (use-factoring) (use-literal-ordering-with-hyperresolution 'literal-ordering-p) (use-literal-ordering-with-negative-hyperresolution 'literal-ordering-n) (use-literal-ordering-with-resolution 'literal-ordering-a) (use-literal-ordering-with-paramodulation 'literal-ordering-a) (declare-ordering-greaterp 'snark::|nonce?| 'snark::|firstSendIn| 'snark::|precedes| 'snark::|sendIn| 'snark::|inside| 'snark::|send| 'snark::|minSendIn|) (declare-ordering-greaterp 'snark::|hashResponse| 'snark::|hash|) (variable-weight 6) (use-ac-connectives) (run-time-limit 60) (assert-supported nil) (use-code-for-numbers nil) (print-symbol-ordering) (print-final-rows)" endspec ChallengeResponse = spec import Nonce op challenge : Agent * Agent * Term -> Term op response : Agent * Agent * Term -> Term (* If a response was received, there was a first sending of that response. *) axiom MinSendingOfResponse is fa(receiving,m:Nonce,agentA,agentB) receiveIn(receiving,agentA,response(agentA,agentB,m)) => (ex(sending,sender) minSendIn(sending,sender,response(agentA,agentB,m))) axiom ChallengeResponse is fa(receivingR,sendingC,m:Nonce,agentB,n:Nonce) (~(ex(sillysending) sendIn(sillysending,creator(m), response(creator(m),agentB,m)))) & minSendIn(sendingC,creator(m),challenge(creator(m),agentB,m)) & receiveIn(receivingR,creator(m),response(creator(m),agentB,m)) & sendingC precedes receivingR & agentB ~= creator(m) % optional slight improvement in time => (ex(receivingC,sendingR) receiveIn(receivingC,agentB,challenge(creator(m),agentB,m)) & minSendIn(sendingR,agentB,response(creator(m),agentB,m)) & sendingC precedes receivingC & receivingC precedes sendingR & sendingR precedes receivingR) endspec CRHOblig = obligations morphism ChallengeResponse -> HashPlus {challenge +-> identityChallenge, response +-> hashResponse} CRPairOblig = obligations morphism ChallengeResponse -> HashPlus {challenge +->pairChallenge, response +->pairResponse} CRHH = spec import CRHOblig import CRPairOblig conjecture A_Authentication is fa(agentB,m:Nonce,n:Term,sendingM,receivingPair) (* Alice doesn't forge Bob's hash: *) ~(ex(sillySending,t) (sendIn(sillySending,creator(m),hash(agentB,creator(m),pair(m,n))) )) (* Bob only sends the hash in the context of a pair. The second component of the pair is a nonce he creates: *) & (fa(honestSending) minSendIn(honestSending,agentB, hash(agentB,creator(m),pair(m,n))) => firstSendIn(honestSending,agentB, pair(n,hash(agentB,creator(m),pair(m,n)))) & nonce?(n) & agentB = creator(n) ) (* Alice is the first sender of nonce m: *) & firstSendIn(sendingM,creator(m),m) (* Alice receives the hashed pair of nonces: *) & receiveIn(receivingPair,creator(m), hash(agentB,creator(m),pair(m,n))) => (ex(receivingM,sendingPair) (* Bob has received the nonce m: *) receiveIn(receivingM,agentB,m) (* Bob creates the nonce n: *) & nonce?(n) & agentB = creator(n) (* Bob is the first sender of the pair. *) & firstSendIn(sendingPair,agentB,pair(n,hash(agentB,creator(m),pair(m,n)))) (* These events occur in order: *) & sendingM precedes receivingM & receivingM precedes sendingPair & sendingPair precedes receivingPair ) endspec (* for searches for inconsistencies: *) ConsistencySpec = spec import Hash conjecture Inconsistency is false endspec ThmSendInIsMonotonic = prove ThmSendInIsMonotonic in SendReceive options proverOptions ThmReceiveInIsMonotonic = prove ThmReceiveInIsMonotonic in SendReceive options proverOptions ThmRcvIn = prove ThmRcvIn in SendReceive options proverOptions ThmReceivingPrecededByMinimalSending = prove ThmReceivingPrecededByMinimalSending in SendReceive options proverOptions ThmFirstImpliesMinSendIn = prove ThmFirstImpliesMinSendIn in SendReceive options proverOptions ThmFirstSendInPrecedesReceiveIn = prove ThmFirstSendInPrecedesReceiveIn in SendReceive options proverOptions ThmNonceFirstSendPrecedesSending = prove ThmNonceFirstSendPrecedesSending in Nonce options proverNonceOptions ThmNonceFirstSendPrecedesReceiving = prove ThmNonceFirstSendPrecedesReceiving in Nonce options proverNonceOptions (* out--increased proof times ThmNonceMinImpliesFirstSendIn = prove ThmNonceMinImpliesFirstSendIn in Nonce options proverNonceOptions *) HashedPairContainsComponents = prove HashedPairContainsComponents in Hash options proverNonceOptions ThmCRHMinSendingOfResponse = prove MinSendingOfResponse in CRHOblig options proverHashOptions ThmCRHChallengeResponse = prove ChallengeResponse in CRHOblig options proverHashOptions TmhCRPairMinSendingOfResponse = prove MinSendingOfResponse in CRPairOblig options proverHashOptions ThmCRPairChallengeResponse = prove ChallengeResponse in CRPairOblig options proverOptions A_Authentication = prove A_Authentication in A_AuthenticationSpec options proverNonceOptions A_AuthenticationCRHH = prove A_Authentication in CRHH options proverNonceOptions (* omitted---requires one axiom to be supported A_Authentication1 = prove A_Authentication1 in A_AuthenticationSpec options proverAuthOptions *) B_Authentication = prove B_Authentication in B_AuthenticationSpec options proverNonceOptions (* (* uncomment for inconsistency search only: *) Inconsistency = prove Inconsistency in ConsistencySpec options "(use-resolution t) (use-hyperresolution nil) (use-negative-hyperresolution nil) (use-paramodulation) (use-factoring) (use-literal-ordering-with-resolution 'literal-ordering-a) (use-literal-ordering-with-paramodulation 'literal-ordering-a) (variable-weight 3) (use-ac-connectives) (run-time-limit 200) (assert-supported t) (use-code-for-numbers nil) (print-symbol-ordering) (print-final-rows)" *)