Secure Contract Signing Protocol

Contract Signing is the act of two parties agreeing to a contract. A good contract signing protocol is hard to design. It must at least have the following properties:

• Fairness This is a very basic property for a contract signing protocol. This states that an honest participant can never be "cheated" by a dishonest participant. This means that at the end of the protocol run, if the honest party doesn't have a contract then his partner can't have one either.
• Abuse Freeness Describe this...
• Non repudiation Describe this...
• Trusted Third Party Accountability The trusted third party (TTP) should be accountable. That is if he behaves in a dishonest fashion, then the cheated party should be able to show messages which prove this.

With our tool we showed that the particular algorithm with PCS signatures is indeed fair for multiple concurrent contract signings. On the way we discovered a problem, where fairness is violated if an initiator tries to agree with multiple responders on the same contract. We avoided that problem by assuming that every contract is unique.

;;;
;;;   PCS Signature based Secure Contract Signing Protocol
;;;

(murphi-program

 (constant-decls (EMPTY 0)
		 (A->B1 1)
		 (B->A1 2)
		 (A->B2 3)
		 (B->A2 4)

		 (READY 5)
		 (WAITING_B->A1 6)
		 (WAITING_B->A2 7)
		 (WAITING_A->B2 8)
		 (ABORTING 9)
		 (SUCCESS 10)

		 (WAITING_T->A_ABORT 11)
		 (WAITING_T->A_RESOLVE 111)
		 (A->T_ABORT 12)
		 (T->A_ABORT 13)
		 (T->A_SUCCESS 14)
		 (A->T_RESOLVE 141)
		 (T->A_SUCCESS_RESOLVE 142)
		 (T->A_ABORT_RESOLVE 143)

		 (ABORTED 15))

 (global-state (N rat)                   ;; The number of intiators/responders
                                         ;; Assume that processes 1..N are
					 ;; initiators and processes N+1..2N
                                         ;; are responders.

	       (pc (array rat))          ;; State of the processes
	       (responders (array rat))
	       (originator (array rat))
	       (dishonest (array bool))

	       ;; The network...
	       (msg-index rat)
	       (msg-type (array rat))
	       (msg-read (array bool))
	       (msg-sender (array rat))
	       (msg-receiver (array rat))
	       (msg-body (array rat))
	       (msg-signer (array rat))
	       (msg-verifier1 (array rat))
	       (msg-verifier2 (array rat))

	       (resolved (array bool))
	       (transaction-result (array bool))

	       (a rat)                   ;; Arbitrary initiator a
	       (b rat)                   ;; Arbitrary responder b
	       (s1 rat)
	       (s2 rat)
	       (s3 rat)
	       (s4 rat)
	       (s5 rat)
	       (s6 rat)
	       (s7 rat)
	       (s8 rat)
	       (s9 rat)
	       (s10 rat))

 (axiom (and (>= a 0) (< a N)
	     (>= b N) (< b (* 2 N))
	     (= (aref responders a) b)))


 (initialize
  (progn
    (setq dishonest (mwrite dishonest i true false))
    (setq resolved (mwrite resolved i true false))
    (setq originator (mwrite originator i true -1))
    (setq msg-type (mwrite msg-type i true EMPTY))
    (setq msg-sender (mwrite msg-type i true -3))
    (setq msg-signer (mwrite msg-type i true -3))
    (setq msg-receiver (mwrite msg-type i true -3))
    (setq msg-index 0)
    (setq s1 -1)
    (setq s2 -1)
    (setq s3 -1)
    (setq s4 -1)
    (setq s5 -1)
    (setq s6 -1)
    (setq s7 -1)
    (setq s8 -1)
    (setq s9 -1)
    (Setq s10 -1)
    (setq pc (mwrite pc i true READY))))


 ;; The actions of the intruder
 (ruleset (index)
  ;; Lose an arbitrary message...
  (==> true
       (setq (aref msg-read index) true))

  ;; Replay attack...
  (==> true
       (setq (aref msg-read index) false))

  ;; Insert a message on behalf of a dishonest participant...
  (==> (aref dishonest index)
       (progn
	 ;; Note we don't specify receiver/verifiers. That means those
	 ;; values can be assumed to cause maximum havoc.
	 (setq (aref msg-signer msg-index) index)
	 (setq (aref msg-read msg-index) false)
	 (setq msg-index (+ msg-index 1))))

  ;; A participant goes over to the dark side.
  (==> true
       (setq (aref dishonest index) true)))

 (ruleset (initiator responder message)
   ;; Initiate a signing...
   (==> (and (>= initiator 0) (< initiator N)
	     (= responder (aref responders initiator))
	     (>= responder (+ N 1)) (< responder (* 2 N))
	     (= (aref pc initiator) READY)
             (forall (x) (=> (< x msg-index)
                             (/= (aref msg-body msg-index) message)))
	(progn
	  (setq (aref msg-type msg-index) A->B1)
	  (setq (aref msg-read msg-index) false)
	  (setq (aref msg-sender msg-index) initiator)
	  (setq (aref msg-receiver msg-index) responder)
	  (setq (aref msg-body msg-index) message)
	  (setq (aref msg-signer msg-index) initiator)
	  (setq (aref msg-verifier1 msg-index) responder)
	  (setq (aref msg-verifier2 msg-index) -1) ; -1 == Trusted Third Party!

	  (setq (aref pc initiator) WAITING_B->A1)

	  ;; Monitor code
	  (ite (and (= (aref msg-sender msg-index) a)
		    (= (aref msg-receiver msg-index) b))
	       (setq s1 msg-index)
	       (skip))

	  (setq msg-index (+ msg-index 1))))	    

   ;; Initiator times out...
   (==> (and (>= initiator 0) (< initiator N)
	     (= (aref pc initiator) WAITING_B->A1))
	(progn
	  (setq (aref pc initiator) ABORTING)))

   ;; Initiator asks for resolution...
   (==> (and (>= initiator 0) (< initiator N)
   	     (= (aref pc initiator) WAITING_B->A2))
   	(progn
   	  (setq (aref msg-type msg-index) A->T_RESOLVE)
	  (setq (aref msg-sender msg-index) initiator)
	  (setq (aref msg-signer msg-index) -1)
	  (setq (aref msg-receiver msg-index) -1)
	  ;; These are actually the signers...
	  (setq (aref msg-verifier1 msg-index) initiator)
	  (setq (aref msg-verifier2 msg-index) (aref responders initiator))

	  (setq msg-index (+ msg-index 1))
	  (setq (aref pc initiator) WAITING_T->A_RESOLVE)

	  ;; monitor code
	  (ite (and (= initiator a) (= (aref responders initiator) b))
	       (setq s5 (- msg-index 1))
	       (skip))))

   ;; Responder asks for resolution...
   (==> (and (>= responder N) (< responder (* 2 N))
	     (= (aref pc responder) WAITING_A->B2))
	(progn
	  (setq (aref msg-type msg-index) A->T_RESOLVE)
	  (setq (aref msg-signer msg-index) -1)
	  (setq (aref msg-receiver msg-index) -1)
	  (setq (aref msg-sender msg-index) responder)
	  (setq (aref msg-verifier1 msg-index) (aref originator responder))
	  (setq (aref msg-verifier2 msg-index) responder)

	  (setq msg-index (+ msg-index 1))
	  (setq (aref pc responder) WAITING_T->A_RESOLVE)
	  (ite (and (= responder b) (= (aref originator responder) a))
	       (setq s6 (- msg-index 1))
	       (skip)))))

 (ruleset (index)
  (==> (and (= (aref pc index) ABORTING)
	    (>= index 0) (< index N))
       (progn
	 (setq (aref msg-type msg-index) A->T_ABORT)
	 (setq (aref msg-sender msg-index) index)
	 (setq (aref msg-receiver msg-index) -1)
	 (setq (aref msg-verifier1 msg-index) -1)
	 (setq (aref msg-verifier2 msg-index) -1)
	 (setq (aref msg-signer msg-index) -1)
	 (setq (aref msg-signer msg-index) index)
	 (setq (aref msg-read msg-index) false)

	 ;; monitor code
	 (ite (= index a)
	      (setq s9 msg-index)
	      (skip))

	 (setq msg-index (+ msg-index 1))
	 (setq (aref pc index) WAITING_T->A_ABORT))))

 ;; Trusted Third Party actions...
 (ruleset (index)

  (==> (and (not (aref msg-read index))
	    (>= index 0) (< index msg-index)
	    (= (aref msg-receiver index) -1)
	    (= (aref msg-signer index) -1)
	    (or (= (aref msg-sender index) (aref msg-verifier1 index))
		(= (aref msg-sender index) (aref msg-verifier2 index)))
	    (= (aref responders (aref msg-verifier1 index))
	       (aref msg-verifier2 index))
	    (= (aref originator (aref msg-verifier2 index))
	       (aref msg-verifier1 index))
	    (>= (aref msg-verifier1 index) 0)
	    (< (aref msg-verifier1 index) N)
	    (>= (aref msg-verifier2 index) N)
	    (< (aref msg-verifier2 index) (* 2 N))
	    (= (aref msg-type index) A->T_RESOLVE))
       (progn
	 (setq (aref msg-read index) true)
	 (setq (aref msg-sender msg-index) -1)
	 (setq (aref msg-signer msg-index) -1)
	 (setq (aref msg-verifier1 msg-index) -1)
	 (setq (aref msg-verifier2 msg-index) -1)
	 (ite (aref resolved (aref msg-verifier1 index))
	      (ite (aref transaction-result (aref msg-verifier1 index))
		   (setq (aref msg-type msg-index) T->A_SUCCESS_RESOLVE)
		   (setq (aref msg-type msg-index) T->A_ABORT_RESOLVE))
	      (progn
		(setq (aref resolved (aref msg-verifier1 index)) true)
		(setq (aref transaction-result (aref msg-verifier1 index))
		      true)
		(setq (aref msg-type msg-index) T->A_SUCCESS_RESOLVE)))
	 (setq (aref msg-read msg-index) false)
	 (setq (aref msg-receiver msg-index) (aref msg-sender index))

	 (progn
	   ;; Monitor actions...
	   (ite (and (= (aref msg-receiver msg-index) a)
		     (= (aref msg-verifier1 index) a)
		     (= (aref msg-verifier2 index) b))
		(setq s7 msg-index)
		(skip))
	   (ite (and (= (aref msg-receiver msg-index) b)
		     (= (aref originator b) a)
		     (= (aref msg-verifier1 index) a)
		     (= (aref msg-verifier2 index) b))
		(setq s8 msg-index)
		(skip))
	    
	   (setq msg-index (+ msg-index 1)))))

  (==> (and (not (aref msg-read index))
	    (>= index 0) (< index msg-index)
	    (>= (aref msg-sender index) 0)
	    (< (aref msg-sender index) N)
	    (= (aref msg-receiver index) -1)
	    (= (aref msg-verifier1 index) -1)
	    (= (aref msg-verifier2 index) -1)
	    (= (aref msg-signer index) (aref msg-sender index))
	    (= (aref msg-type index) A->T_ABORT))
       (progn
	 (setq (aref msg-read index) true)

	 (setq (aref msg-sender msg-index) -1)
	 (setq (aref msg-signer msg-index) -1)
	 (setq (aref msg-verifier1 msg-index) -1)
	 (setq (aref msg-verifier2 msg-index) -1)
	 (ite (aref resolved (aref msg-sender index))
	      (ite (aref transaction-result (aref msg-sender index))
		   (setq (aref msg-type msg-index) T->A_SUCCESS)
		   (setq (aref msg-type msg-index) T->A_ABORT))
	      (progn
		(setq (aref resolved (aref msg-sender index)) true)
		(setq (aref transaction-result (aref msg-sender index)) false)
		(setq (aref msg-type msg-index) T->A_ABORT)))
	 (setq (aref msg-read msg-index) false)
	 (setq (aref msg-receiver msg-index) (aref msg-sender index))

	 (progn
	   ;; monitor action
	   (ite (= (aref msg-sender index) a)
		(setq s10 msg-index)
		(skip))

	   (setq msg-index (+ 1 msg-index))))))

 ;; Receiving results from abort request...
 (ruleset (index)
  (==> (and (not (aref msg-read index))
	    (>= index 0) (< index msg-index)
	    (= (aref msg-type index) T->A_SUCCESS)
	    (= (aref pc (aref msg-receiver index)) WAITING_T->A_ABORT))
       (setq (aref pc (aref msg-receiver index)) SUCCESS))
  (==> (and (not (aref msg-read index))
	    (>= index 0) (< index msg-index)
	    (= (aref msg-type index) T->A_ABORT)
	    (= (aref pc (aref msg-receiver index)) WAITING_T->A_ABORT))
       (setq (aref pc (aref msg-receiver index)) ABORTED)))

 ;; Rules for receiving results from the resolve request...
 (ruleset (index)
  (==> (and (not (aref msg-read index))
	    (>= index 0) (< index msg-index)
	    (= (aref msg-type index) T->A_SUCCESS_RESOLVE)
	    (= (aref pc (aref msg-receiver index)) WAITING_T->A_RESOLVE))
       (setq (aref pc (aref msg-receiver index)) SUCCESS))

  (==> (and (not (aref msg-read index))
	    (>= index 0) (< index msg-index)
	    (= (aref msg-type index) T->A_ABORT_RESOLVE)
	    (= (aref pc (aref msg-receiver index)) WAITING_T->A_RESOLVE))
       (setq (aref pc (aref msg-receiver index)) ABORTED)))

 ;; Rules of the original protocol...
 (ruleset (index)
  (==> (and (= (aref msg-type index) A->B1)
	    (>= index 0) (< index msg-index)
	    (= (aref pc (aref msg-receiver index)) READY)
	    (= (aref originator (aref msg-receiver index)) -1) ;Filtering
	    (>= (aref msg-sender index) 0)
	    (< (aref msg-sender index) N)
	    (>= (aref msg-receiver index) N)
	    (< (aref msg-receiver index) (* 2 N))
	    (= (aref msg-sender index) (aref msg-signer index))
	    (= (aref msg-verifier1 index) (aref msg-receiver index))
	    (= (aref msg-verifier2 index) -1)
	    (not (aref msg-read index)))
       (progn
	 (setq (aref msg-read index) TRUE)

	 ;; Send message to A
	 (setq (aref msg-type msg-index) B->A1)
	 (setq (aref msg-read msg-index) FALSE)
	 (setq (aref msg-sender msg-index) (aref msg-receiver index))
	 (setq (aref msg-receiver msg-index) (aref msg-sender index))
	 (setq (aref msg-body msg-index) (aref msg-body index))
	 (setq (aref msg-signer msg-index) (aref msg-receiver index))
	 (setq (aref msg-verifier1 msg-index) (aref msg-sender index))
	 (setq (aref msg-verifier2 msg-index) -1) ;; -1 == Trusted Third Party!

	 (setq (aref originator (aref msg-receiver index))
	       (aref msg-sender index))

	  ;; Monitor code
	  (ite (and (= (aref msg-sender index) a)
		    (= (aref msg-receiver index) b))
	       (setq s2 msg-index)
	       (skip))

	 (setq msg-index (+ msg-index 1))
	 (setq (aref pc (aref msg-receiver index)) WAITING_A->B2)))

  (==> (and (= (aref msg-type index) B->A1)
	    (>= index 0) (< index msg-index)
	    (= (aref pc (aref msg-receiver index)) WAITING_B->A1)
	    (>= (aref msg-receiver index) 0)
	    (< (aref msg-receiver index) N)
	    (= (aref msg-sender index) (aref msg-signer index))
	    (= (aref msg-sender index)
	       (aref responders (aref msg-receiver index)))
	    (= (aref msg-verifier1 index) (aref msg-receiver index))
	    (= (aref msg-verifier2 index) 0)
	    ;(or true (= (aref msg-verifier2 a) -1)) ;Instatiation hint
	    (not (aref msg-read index)))
       (progn
	 (setq (aref msg-read index) true)

	 ;; Send signed message to B
	 (setq (aref msg-type msg-index) A->B2)
	 (setq (aref msg-read msg-index) FALSE)
	 (setq (aref msg-sender msg-index) (aref msg-receiver index))
	 (setq (aref msg-receiver msg-index) (aref msg-sender index))
	 (setq (aref msg-body msg-index) (aref msg-body index))
	 (setq (aref msg-signer msg-index) (aref msg-receiver index))
	 (setq (aref msg-verifier1 msg-index) -2)
	 (setq (aref msg-verifier2 msg-index) -2)

	  ;; Monitor code
	  (ite (and (= (aref msg-sender index) b)
		    (= (aref msg-receiver index) a))
	       (setq s3 msg-index)
	       (skip))

	 (setq msg-index (+ msg-index 1))
	 (setq (aref pc (aref msg-receiver index)) WAITING_B->A2)))

  (==> (and (= (aref msg-type index) A->B2)
	    (>= index 0) (< index msg-index)
	    (>= (aref msg-receiver index) N)
	    (< (aref msg-receiver index) (* 2 N))
	    (= (aref pc (aref msg-receiver index)) WAITING_A->B2)
	    (= (aref msg-sender index) (aref msg-signer index))
	    (= (aref msg-sender index)
	       (aref originator (aref msg-receiver index)))
	    (= (aref msg-verifier1 index) -2)
	    (= (aref msg-verifier2 index) -2)
	    (not (aref msg-read index)))
       (progn
	 (setq (aref msg-read index) TRUE)

	 ;; Send signed message to A
	 (setq (aref msg-type msg-index) B->A2)
	 (setq (aref msg-read msg-index) FALSE)
	 (setq (aref msg-sender msg-index) (aref msg-receiver index))
	 (setq (aref msg-receiver msg-index) (aref msg-sender index))
	 (setq (aref msg-body msg-index) (aref msg-body index))
	 (setq (aref msg-signer msg-index) (aref msg-receiver index))
	 (setq (aref msg-verifier1 msg-index) -2)
	 (setq (aref msg-verifier2 msg-index) -2)

	 ;; Monitor code
	 (ite (and (= (aref msg-sender index) a)
		   (= (aref msg-receiver index) b))
	      (setq s4 msg-index)
	      (skip))

	 (setq msg-index (+ msg-index 1))
	 (setq (aref pc (aref msg-receiver index)) SUCCESS)))

  (==> (and (= (aref msg-type index) B->A2)
	    (>= index 0) (< index msg-index)
	    (>= (aref msg-receiver index) 0)
	    (< (aref msg-receiver index) N)
	    (= (aref pc (aref msg-receiver index)) WAITING_B->A2)
	    (= (aref msg-sender index) (aref msg-signer index))
	    (= (aref msg-sender index)
	       (aref responders (aref msg-receiver index)))
	    (= (aref msg-verifier1 index) -2)
	    (= (aref msg-verifier2 index) -2)
	    (not (aref msg-read index)))
       (progn
	 (setq (aref msg-read index) TRUE)
	 (setq (aref pc (aref msg-receiver index)) SUCCESS))))

 (invariant (and ;; Honest initiator can't be cheated...
                 (=> (and (not (aref dishonest a))
			  (or (= (aref originator b) a)
			      (= (aref originator b) -1)))
		     (not (and (= (aref pc a) ABORTED)
			       (= (aref pc b) SUCCESS))))
                 ;; Honest respondent can't be cheated...
		 (=> (and (not (aref dishonest b))
			  (or (= (aref originator b) a)
			      (= (aref originator b) -1)))
		     (not (and (= (aref pc a) SUCCESS)
			       (= (aref pc b) ABORTED))))))

 (abstraction

  (INV-EMPTY (forall (x) (=> (>= x msg-index) (= (aref msg-type x) EMPTY))))
  (INV (and (or (= s1 -1)
		(and (>= s1 0)
		     (= (aref msg-sender s1) a)
		     (= (aref msg-receiver s1) b)
		     (= (aref msg-type s1) A->B1)))
	    (or (= s2 -1)
		(and (> s2 s1)
		     (>= s1 0)
		     (= (aref msg-sender s2) b)
		     (= (aref msg-receiver s2) a)
		     (= (aref msg-type s2) B->A1)))
	    (or (= s3 -1)
		(and (> s3 s2)
		     (> s2 s1)
		     (>= s1 0)
		     (= (aref msg-sender s3) a)
		     (= (aref msg-receiver s3) b)
		     (= (aref msg-type s3) A->B2)))
	    (or (= s4 -1)
		(and (> s4 s3)
		     (> s3 s2)
		     (> s2 s1)
		     (>= s1 0)
		     (= (aref msg-sender s4) b)
		     (= (aref msg-signer s4) b)
		     (= (aref msg-receiver s4) a)
		     (= (aref msg-type s4) B->A2)))
	    (and (>= msg-index 0)
		 (> msg-index s1)
		 (> msg-index s2)
		 (> msg-index s3)
		 (> msg-index s4))))

  (INV-RES1 (and (or (= s5 -1)
		     (and (>= s5 0) (< s5 msg-index)
			  (= (aref msg-sender s5) a)
			  (= (aref msg-signer s5) -1)
			  (= (aref msg-receiver s5) -1)
			  (= (aref msg-verifier1 s5) a)
			  (= (aref msg-verifier2 s5) b)
			  (= (aref msg-type s5) A->T_RESOLVE)))
		 (or (= s7 -1)
		     (and
		      (>= s7 0) (< s7 msg-index)
		      (= (aref msg-receiver s7) a)
		      (= (aref msg-sender s7) -1)
		      (= (aref msg-signer s7) -1)
		      (= (aref msg-verifier1 s7) -1)
		      (= (aref msg-verifier2 s7) -1)
		      (=> (aref transaction-result a)
			  (= (aref msg-type s7) T->A_SUCCESS_RESOLVE))
		      (=> (not (aref transaction-result a))
			  (= (aref msg-type s7) T->A_ABORT_RESOLVE))))))
  (INV-RES2 (and (or (= s6 -1)
		     (and (>= s6 0) (< s6 msg-index)
			  (= (aref msg-signer s6) -1)
			  (= (aref msg-receiver s6) -1)
			  (= (aref msg-sender s6) b)
			  (= (aref msg-verifier1 s6) a)
			  (= (aref msg-verifier2 s6) b)
			  (= (aref msg-type s6) A->T_RESOLVE)))
		 (or (= s8 -1)
		     (and
		      (>= s8 0) (< s8 msg-index)
		      (= (aref msg-sender s8) -1)
		      (= (aref msg-signer s8) -1)
		      (= (aref msg-verifier1 s8) -1)
		      (= (aref msg-verifier2 s8) -1)
		      (= (aref msg-receiver s8) b)
		      (=> (aref transaction-result a)
			  (= (aref msg-type s8) T->A_SUCCESS_RESOLVE))
		      (=> (not (aref transaction-result a))
			  (= (aref msg-type s8) T->A_ABORT_RESOLVE))))))
  (INV-AB (and (or (= s9 -1)
		   (and (>= s9 0) (< s9 msg-index)
			(= (aref msg-sender s9) a)
			(= (aref msg-receiver s9) -1)
			(= (aref msg-verifier1 s9) -1)
			(= (aref msg-verifier2 s9) -1)
			(= (aref msg-signer s9) a)
			(= (aref msg-type s9) A->T_ABORT)))
	       (or (= s10 -1)
		   (and (>= s10 0) (< s10 msg-index)
			(= (aref msg-sender s10) -1)
			(= (aref msg-signer s10) -1)
			(= (aref msg-verifier1 s10) -1)
			(= (aref msg-verifier2 s10) -1)
			(= (aref msg-receiver s10) a)
			(=> (aref transaction-result a)
			    (= (aref msg-type s10) T->A_SUCCESS))
			(=> (not (aref transaction-result a))
			    (= (aref msg-type s10) T->A_ABORT))))))

  ;; States A can be in...
  (A@READY (= (aref pc a) READY))
  (A@ABORTING (= (aref pc a) ABORTING))
  (A@WAITING_B->A1 (= (aref pc a) WAITING_B->A1))
  (A@WAITING_B->A2 (= (aref pc a) WAITING_B->A2))
  (A@WAITING_T->A_ABORT (= (aref pc a) WAITING_T->A_ABORT))
  (A@WAITING_T->A_RESOLVE (= (aref pc a) WAITING_T->A_RESOLVE))
  (A@ABORTED (= (aref pc a) ABORTED))
  (A@SUCCESS (= (aref pc a) SUCCESS))

  (s11 (= s1 -1))
  (s12 (= s2 -1))
  (s13 (= s3 -1))
  (s14 (= s4 -1))
  (s15 (= s5 -1))
  (s16 (= s6 -1))
  (s17 (= s7 -1))
  (s18 (= s8 -1))
  (s19 (= s9 -1))
  (s110 (= s10 -1))


  ;; States B can be in...
  (B@READY (= (aref pc b) READY))
  (B@WAITING_A->B2 (= (aref pc b) WAITING_A->B2))
  (B@WAITING_T->B_RESOLVE (= (aref pc b) WAITING_T->A_RESOLVE))
  (B@ABORTED (= (aref pc b) ABORTED))
  (B@SUCCESS (= (aref pc b) SUCCESS))
  (ORIGINATOR[B]=A (= (aref originator b) a))
  (ORIGINATOR[B]=-1 (= (aref originator b) -1))
  (ORIGINATOR[B]>=0 (>= (aref originator b) 0))

  ;; Messages in transit...
  (M1 (forall (x)
  	 (=> (and (>= x 0) (< x msg-index) (/= x s1) (not (aref dishonest a)))
  	     (not (and (= (aref msg-sender x) a)
  		       (= (aref msg-signer x) a)
  		       (= (aref msg-receiver x) b)
  		       (= (aref msg-type x) A->B1))))))
  (M2 (forall (x)
  	 (=> (and (>= x 0) (< x msg-index) (/= x s2) (not (aref dishonest b)))
  	     (not (and (= (aref msg-sender x) b)
  		       (= (aref msg-signer x) b)
  		       (= (aref msg-receiver x) a)
  		       (= (aref msg-type x) B->A1))))))
  (M3 (forall (x)
  	 (=> (and (>= x 0) (< x msg-index) (/= x s3) (not (aref dishonest a)))
  	     (not (and (= (aref msg-sender x) a)
  		       (= (aref msg-signer x) a)
  		       (= (aref msg-receiver x) b)
  		       (= (aref msg-type x) A->B2))))))
  (M4 (forall (x)
  	 (=> (and (>= x 0) (< x msg-index) (/= x s4) (not (aref dishonest b)))
  	     (not (and (= (aref msg-sender x) b)
  		       (= (aref msg-signer x) b)
  		       (= (aref msg-receiver x) a)
  		       (= (aref msg-type x) B->A2))))))
  (M5 (forall (x)
         (=> (and (>= x 0) (< x msg-index) (/= x s5) (not (aref dishonest a))
		  (or (= (aref originator b) -1)
		      (= (aref originator b) a)))
	     (not (and ;(not (aref msg-read x))
		       (= (aref msg-sender x) a)
		       (= (aref msg-signer x) -1)
		       (= (aref msg-receiver x) -1)
		       (= (aref msg-verifier1 x) a)
		       (= (aref msg-verifier2 x) b)
		       (= (aref msg-type x) A->T_RESOLVE))))))
  ;(M51 (forall (x)
  ;	    (=> (and (>= x 0) (not (aref dishonest a)))
  ;		(not (and (= (aref msg-sender x) a)
  ;			  ;(= (aref msg-verifier1 x) a)
  ;			  ;(= (aref msg-verifier2 x) b)
  ;			  (= (aref msg-type x) A->T_RESOLVE))))))
  (M6 (forall (x)
  	  (=> (and (>= x 0) (< x msg-index) (/= x s6) (not (aref dishonest b))
  		   (or (= (aref originator b) -1)
  		       (= (aref originator b) a)))
  	      (not (and ;(not (aref msg-read x))
			(= (aref msg-sender x) b)
  			(= (aref msg-signer x) -1)
  			(= (aref msg-receiver x) -1)
  			(= (aref msg-verifier1 x) a)
  			(= (aref msg-verifier2 x) b)
  			(= (aref msg-type x) A->T_RESOLVE))))))
  ;(M61 (forall (x)
  ;	    (=> (and (>= x 0) (not (aref dishonest b)))
  ;		(not (and (= (aref msg-sender x) b)
  ;			  ;(= (aref msg-verifier1 x) a)
  ;			  ;(= (aref msg-verifier2 x) b)
  ;			  (= (aref msg-type x) A->T_RESOLVE))))))
  (M7 (forall (x)
        (=> (and (>= x 0) (< x msg-index)
		 (or (= (aref msg-type x) T->A_SUCCESS_RESOLVE)
		     (= (aref msg-type x) T->A_ABORT_RESOLVE)))
	    (and (=> (= (aref msg-receiver x) a)
		     (and (aref resolved a)
			  (=> (aref transaction-result a)
			      (= (aref msg-type x) T->A_SUCCESS_RESOLVE))
			  (=> (not (aref transaction-result a))
			      (= (aref msg-type x) T->A_ABORT_RESOLVE))))
		 (=> (and (= (aref msg-receiver x) b)
			  (= (aref originator b) a))
		     (and (aref resolved a)
			  (=> (aref transaction-result a)
			      (= (aref msg-type x) T->A_SUCCESS_RESOLVE))
			  (=> (not (aref transaction-result a))
			      (= (aref msg-type x) T->A_ABORT_RESOLVE))))))))
  (M8 (forall (x)
        (=> (and (>= x 0) (< x msg-index) (= (aref originator b) -1))
	    (and (not (and (= (aref msg-type x) T->A_SUCCESS_RESOLVE)
			   (= (aref msg-receiver x) b)))
		 (not (and (= (aref msg-type x) T->A_ABORT_RESOLVE)
			   (= (aref msg-receiver x) b)))
		 (not (and (= (aref msg-type x) A->T_RESOLVE)
			   (= (aref msg-verifier1 x) a)
			   (= (aref msg-verifier2 x) b)
			   (= (aref msg-sender x) b)))))))
  (M81 (forall (x)
	 (=> (and (>= x 0) (< x msg-index)
		  (or (= (aref pc a) READY)
		      (= (aref pc a) WAITING_B->A1)
		      (= (aref pc a) ABORTING)
		      (= (aref pc a) WAITING_B->A2)
		      (= (aref pc a) WAITING_T->A_ABORT)))
	     (and (not (and (= (aref msg-type x) T->A_SUCCESS_RESOLVE)
			    (= (aref msg-receiver x) a)))
		  (not (and (= (aref msg-type x) T->A_ABORT_RESOLVE)
			    (= (aref msg-receiver x) a)))
		  (not (and (= (aref msg-type x) A->T_RESOLVE)
			    (= (aref msg-verifier1 x) a)
			    (= (aref msg-verifier2 x) b)
			    (= (aref msg-sender x) a)))))))
  (M9 (forall (x)
         (=> (and (>= x 0) (< x msg-index) (/= x s9) (not (aref dishonest a)))
	     (not (and (not (aref msg-read x))
		       (= (aref msg-sender x) a)
		       ;(= (aref msg-receiver x) -1)
		       ;(= (aref msg-verifier1 x) -1)
		       ;(= (aref msg-verifier2 x) -1)
		       (= (aref msg-signer x) a)
		       (= (aref msg-type x) A->T_ABORT))))))
  (M10 (forall (x)
	  (=> (and (>= x 0) (< x msg-index) (/= x s10) (not (aref dishonest a)))
	      (not (and (or (= (aref msg-type x) T->A_ABORT)
			    (= (aref msg-type x) T->A_SUCCESS))
			;(= (aref msg-sender x) -1)
			;(= (aref msg-signer x) -1)
			;(= (aref msg-verifier1 x) -1)
			;(= (aref msg-verifier2 x) -1)
			(= (aref msg-receiver x) a))))))

  ;; What the TTP thinks...
  (A->B_RESOLVED (aref resolved a))
  (A->B_RESULT (aref transaction-result a))

  ;; A/B is honest
  (HONEST_A (not (aref dishonest a)))
  (HONEST_B (not (aref dishonest b)))))