in ../occ/lib/prelude.occ
in ../occ/lib/logic.occ
in ../occ/lib/nat.occ

(act : Type)
(FRESH : {T : Type}nat -> T)
(@princ : Type)
(@msg : Type)
(@nonce : Type)
(@state : Type)
(@empty : @state)
(union : @state -> @state -> @state)
(@& : @msg -> @msg -> @msg)
(@nonce-msg : @nonce -> @msg)
(@princ-msg : @princ -> @msg)
(@N : @msg -> @state)
(@pubK : @princ -> Type)
(@encrypt : {@A | @princ}(@pubK @A)-> @msg -> @msg)
(@START-1 : @princ -> @state)
(@START-2 : @princ -> @state)
(@TERMINATED-1 : @princ -> @princ -> @nonce -> @state)
(@TERMINATED-2 : @princ -> @princ -> @nonce -> @state)
(@A : @princ)
(@B : @princ)
(@pkA : @pubK @A)
(@pkB : @pubK @B)
(@knowledge : Type)
(@msg-knowledge : @msg -> @knowledge)
(@I : @knowledge -> @state)
(@privK : @princ -> Type)
(@privK-knowledge : {@P | @princ}(@privK @P)-> @knowledge)
(@i : @princ)
(@privK-i : @privK @i)
(@pubK-i : @pubK @i)
(F : nat -> @state)
(EL : {T : Type}T -> @state)
(union_comm : ||{i,j : @state}((union i j)=(union j i)))
(union_assoc : ||{i,j,k : @state}((union i(union j k))=(union(union i j)k)))
(append_assoc : ||{i,j,k : @msg}((@& i(@& j k))=(@&(@& i j)k)))
(history : Type)
(HISTORY : history -> @state)
(history_nil : history)
(history_conc : act -> history -> history)
(L_initiator_Init1_1 : act)
(L_initiator_Init1_2 : act)
(L_initiator_Init2_1 : act)
(L_initiator_Init2_2 : act)
(T_initiator_Init1 : @princ ->(@princ -> @nonce -> @state)-> @state)
(T_initiator_Init2 : @princ ->(@princ -> @nonce -> @state)-> @state)
(R_initiator_Init1_1 : !!
 {@A : @princ}
 {@L : @princ -> @nonce -> @state}
 {@B : @princ}
 {@PKB : @pubK @B}
 {@nA : @nonce}
 {fresh,fresh' : nat}
 (@L :=(FRESH(@princ -> @nonce -> @state)fresh))->
 (@nA :=(FRESH @nonce(suc fresh)))->
 (fresh' :=(suc(suc fresh)))->
 [L_initiator_Init1_1]:
 (union(union(F fresh)(union(EL @princ @B)(EL(@pubK @B)@PKB)))(@START-1 @A))
  =>
 (union(union(union(F fresh')(T_initiator_Init2 @A @L))(union(EL @princ @B)(EL(@pubK @B)@PKB)))(union(@N(@&(@princ-msg @A)(
    @&(@princ-msg @B)(@encrypt @PKB(@&(@nonce-msg @nA)(@princ-msg @A))))))(@L @B @nA))))
(R_initiator_Init1_2 : !!
 {@A : @princ}
 {@L : @princ -> @nonce -> @state}
 {@B : @princ}
 {@PKB : @pubK @B}
 {@nA : @nonce}
 {fresh,fresh' : nat}
 (@nA :=(FRESH @nonce fresh))->
 (fresh' :=(suc fresh))->
 [L_initiator_Init1_2]:
 (union(union(union(F fresh)(T_initiator_Init1 @A @L))(union(EL @princ @B)(EL(@pubK @B)@PKB)))(@START-1 @A))
  =>
 (union(union(F fresh')(union(EL @princ @B)(EL(@pubK @B)@PKB)))(union(@N(@&(@princ-msg @A)(@&(@princ-msg @B)(@encrypt @PKB(
    @&(@nonce-msg @nA)(@princ-msg @A))))))(@L @B @nA))))
(R_initiator_Init2_1 : !!
 {@A : @princ}
 {@L : @princ -> @nonce -> @state}
 {@B : @princ}
 {@PKA : @pubK @A}
 {@PKB : @pubK @B}
 {@nA : @nonce}
 {@nB : @nonce}
 {fresh,fresh' : nat}
 (@L :=(FRESH(@princ -> @nonce -> @state)fresh))->
 (fresh' :=(suc fresh))->
 [L_initiator_Init2_1]:
 (union(union(F fresh)(EL(@pubK @B)@PKB))(union(@N(@&(@princ-msg @B)(@&(@princ-msg @A)(@encrypt @PKA(@&(@nonce-msg @nA)(
    @nonce-msg @nB))))))(@L @B @nA)))
  =>
 (union(union(union(F fresh')(T_initiator_Init1 @A @L))(EL(@pubK @B)@PKB))(union(@N(@&(@princ-msg @A)(@&(@princ-msg @B)(
    @encrypt @PKB(@nonce-msg @nB)))))(@TERMINATED-1 @A @B @nB))))
(R_initiator_Init2_2 : !!
 {@A : @princ}
 {@L : @princ -> @nonce -> @state}
 {@B : @princ}
 {@PKA : @pubK @A}
 {@PKB : @pubK @B}
 {@nA : @nonce}
 {@nB : @nonce}
 {fresh,fresh' : nat}
 (fresh' := fresh)->
 [L_initiator_Init2_2]:
 (union(union(union(F fresh)(T_initiator_Init2 @A @L))(EL(@pubK @B)@PKB))(union(@N(@&(@princ-msg @B)(@&(@princ-msg @A)(
    @encrypt @PKA(@&(@nonce-msg @nA)(@nonce-msg @nB))))))(@L @B @nA)))
  =>
 (union(union(F fresh')(EL(@pubK @B)@PKB))(union(@N(@&(@princ-msg @A)(@&(@princ-msg @B)(@encrypt @PKB(@nonce-msg @nB)))))(
    @TERMINATED-1 @A @B @nB))))

(L_responder_Resp1_1 : act)
(L_responder_Resp1_2 : act)
(L_responder_Resp2_1 : act)
(L_responder_Resp2_2 : act)
(T_responder_Resp1 : @princ ->(@princ -> @nonce -> @nonce -> @state)-> @state)
(T_responder_Resp2 : @princ ->(@princ -> @nonce -> @nonce -> @state)-> @state)
(R_responder_Resp1_1 : !!
 {@B : @princ}
 {@L : @princ -> @nonce -> @nonce -> @state}
 {@A : @princ}
 {@PKA : @pubK @A}
 {@PKB : @pubK @B}
 {@nA : @nonce}
 {@nB : @nonce}
 {fresh,fresh' : nat}
 (@L :=(FRESH(@princ -> @nonce -> @nonce -> @state)fresh))->
 (@nB :=(FRESH @nonce(suc fresh)))->
 (fresh' :=(suc(suc fresh)))->
 [L_responder_Resp1_1]:
 (union(union(F fresh)(EL(@pubK @A)@PKA))(union(@START-2 @B)(@N(@&(@princ-msg @A)(@&(@princ-msg @B)(@encrypt @PKB(@&(
    @nonce-msg @nA)(@princ-msg @A))))))))
  =>
 (union(union(union(F fresh')(T_responder_Resp2 @B @L))(EL(@pubK @A)@PKA))(union(@N(@&(@princ-msg @B)(@&(@princ-msg @A)(
    @encrypt @PKA(@&(@nonce-msg @nA)(@nonce-msg @nB))))))(@L @A @nA @nB))))
(R_responder_Resp1_2 : !!
 {@B : @princ}
 {@L : @princ -> @nonce -> @nonce -> @state}
 {@A : @princ}
 {@PKA : @pubK @A}
 {@PKB : @pubK @B}
 {@nA : @nonce}
 {@nB : @nonce}
 {fresh,fresh' : nat}
 (@nB :=(FRESH @nonce fresh))->
 (fresh' :=(suc fresh))->
 [L_responder_Resp1_2]:
 (union(union(union(F fresh)(T_responder_Resp1 @B @L))(EL(@pubK @A)@PKA))(union(@START-2 @B)(@N(@&(@princ-msg @A)(@&(
    @princ-msg @B)(@encrypt @PKB(@&(@nonce-msg @nA)(@princ-msg @A))))))))
  =>
 (union(union(F fresh')(EL(@pubK @A)@PKA))(union(@N(@&(@princ-msg @B)(@&(@princ-msg @A)(@encrypt @PKA(@&(@nonce-msg @nA)(
    @nonce-msg @nB))))))(@L @A @nA @nB))))
(R_responder_Resp2_1 : !!
 {@B : @princ}
 {@L : @princ -> @nonce -> @nonce -> @state}
 {@A : @princ}
 {@PKB : @pubK @B}
 {@nA : @nonce}
 {@nB : @nonce}
 {fresh,fresh' : nat}
 (@L :=(FRESH(@princ -> @nonce -> @nonce -> @state)fresh))->
 (fresh' :=(suc fresh))->
 [L_responder_Resp2_1]:
 (union(F fresh)(union(@N(@&(@princ-msg @A)(@&(@princ-msg @B)(@encrypt @PKB(@nonce-msg @nB)))))(@L @A @nA @nB)))
  =>
 (union(union(F fresh')(T_responder_Resp1 @B @L))(@TERMINATED-2 @B @A @nA)))
(R_responder_Resp2_2 : !!
 {@B : @princ}
 {@L : @princ -> @nonce -> @nonce -> @state}
 {@A : @princ}
 {@PKB : @pubK @B}
 {@nA : @nonce}
 {@nB : @nonce}
 {fresh,fresh' : nat}
 (fresh' := fresh)->
 [L_responder_Resp2_2]:
 (union(union(F fresh)(T_responder_Resp2 @B @L))(union(@N(@&(@princ-msg @A)(@&(@princ-msg @B)(@encrypt @PKB(@nonce-msg
    @nB)))))(@L @A @nA @nB)))
  =>
 (union(F fresh')(@TERMINATED-2 @B @A @nA)))

(L_dolevyao_INT_1 : act)
(L_dolevyao_INT_2 : act)
(L_dolevyao_TRN_1 : act)
(L_dolevyao_TRN_2 : act)
(L_dolevyao_DCM_1 : act)
(L_dolevyao_DCM_2 : act)
(L_dolevyao_CMP_1 : act)
(L_dolevyao_CMP_2 : act)
(L_dolevyao_IPR_1 : act)
(L_dolevyao_IPR_2 : act)
(L_dolevyao_GNC_1 : act)
(L_dolevyao_GNC_2 : act)
(L_dolevyao_GMS_1 : act)
(L_dolevyao_GMS_2 : act)
(L_dolevyao_DEL_1 : act)
(L_dolevyao_DEL_2 : act)
(L_dolevyao_DUP_1 : act)
(L_dolevyao_DUP_2 : act)
(T_dolevyao_INT : @state)
(T_dolevyao_TRN : @state)
(T_dolevyao_DCM : @state)
(T_dolevyao_CMP : @state)
(T_dolevyao_IPR : @state)
(T_dolevyao_GNC : @state)
(T_dolevyao_GMS : @state)
(T_dolevyao_DEL : @state)
(T_dolevyao_DUP : @state)
(R_dolevyao_INT_1 : !!
 {@t : @msg}
 {fresh,fresh' : nat}
 (fresh' := fresh)->
 [L_dolevyao_INT_1]:
 (union(F fresh)(@N @t))
  =>
 (union(union(F fresh')(union(T_dolevyao_TRN)(union(T_dolevyao_DCM)(union(T_dolevyao_CMP)(union(T_dolevyao_IPR)(union(
    T_dolevyao_GNC)(union(T_dolevyao_GMS)(union(T_dolevyao_DEL)(T_dolevyao_DUP)))))))))(@I @t)))
(R_dolevyao_INT_2 : !!
 {@t : @msg}
 {fresh,fresh' : nat}
 (fresh' := fresh)->
 [L_dolevyao_INT_2]:
 (union(union(F fresh)(T_dolevyao_INT))(@N @t))
  =>
 (union(F fresh')(@I @t)))
(R_dolevyao_TRN_1 : !!
 {@t : @msg}
 {fresh,fresh' : nat}
 (fresh' := fresh)->
 [L_dolevyao_TRN_1]:
 (union(F fresh)(@I @t))
  =>
 (union(union(F fresh')(union(T_dolevyao_INT)(union(T_dolevyao_DCM)(union(T_dolevyao_CMP)(union(T_dolevyao_IPR)(union(
    T_dolevyao_GNC)(union(T_dolevyao_GMS)(union(T_dolevyao_DEL)(T_dolevyao_DUP)))))))))(@N @t)))
(R_dolevyao_TRN_2 : !!
 {@t : @msg}
 {fresh,fresh' : nat}
 (fresh' := fresh)->
 [L_dolevyao_TRN_2]:
 (union(union(F fresh)(T_dolevyao_TRN))(@I @t))
  =>
 (union(F fresh')(@N @t)))
(R_dolevyao_DCM_1 : !!
 {@t1 : @msg}
 {@t2 : @msg}
 {fresh,fresh' : nat}
 (fresh' := fresh)->
 [L_dolevyao_DCM_1]:
 (union(F fresh)(@I(@& @t1 @t2)))
  =>
 (union(union(F fresh')(union(T_dolevyao_INT)(union(T_dolevyao_TRN)(union(T_dolevyao_CMP)(union(T_dolevyao_IPR)(union(
    T_dolevyao_GNC)(union(T_dolevyao_GMS)(union(T_dolevyao_DEL)(T_dolevyao_DUP)))))))))(union(@I @t1)(@I @t2))))
(R_dolevyao_DCM_2 : !!
 {@t1 : @msg}
 {@t2 : @msg}
 {fresh,fresh' : nat}
 (fresh' := fresh)->
 [L_dolevyao_DCM_2]:
 (union(union(F fresh)(T_dolevyao_DCM))(@I(@& @t1 @t2)))
  =>
 (union(F fresh')(union(@I @t1)(@I @t2))))
(R_dolevyao_CMP_1 : !!
 {@t1 : @msg}
 {@t2 : @msg}
 {fresh,fresh' : nat}
 (fresh' := fresh)->
 [L_dolevyao_CMP_1]:
 (union(F fresh)(union(@I @t1)(@I @t2)))
  =>
 (union(union(F fresh')(union(T_dolevyao_INT)(union(T_dolevyao_TRN)(union(T_dolevyao_DCM)(union(T_dolevyao_IPR)(union(
    T_dolevyao_GNC)(union(T_dolevyao_GMS)(union(T_dolevyao_DEL)(T_dolevyao_DUP)))))))))(@I(@& @t1 @t2))))
(R_dolevyao_CMP_2 : !!
 {@t1 : @msg}
 {@t2 : @msg}
 {fresh,fresh' : nat}
 (fresh' := fresh)->
 [L_dolevyao_CMP_2]:
 (union(union(F fresh)(T_dolevyao_CMP))(union(@I @t1)(@I @t2)))
  =>
 (union(F fresh')(@I(@& @t1 @t2))))
(R_dolevyao_IPR_1 : !!
 {@A : @princ}
 {fresh,fresh' : nat}
 (fresh' := fresh)->
 [L_dolevyao_IPR_1]:
 (union(F fresh)(EL @princ @A))
  =>
 (union(union(union(F fresh')(union(T_dolevyao_INT)(union(T_dolevyao_TRN)(union(T_dolevyao_DCM)(union(T_dolevyao_CMP)(
    union(T_dolevyao_GNC)(union(T_dolevyao_GMS)(union(T_dolevyao_DEL)(T_dolevyao_DUP)))))))))(EL @princ @A))(@I @A)))
(R_dolevyao_IPR_2 : !!
 {@A : @princ}
 {fresh,fresh' : nat}
 (fresh' := fresh)->
 [L_dolevyao_IPR_2]:
 (union(union(F fresh)(T_dolevyao_IPR))(EL @princ @A))
  =>
 (union(union(F fresh')(EL @princ @A))(@I @A)))
(R_dolevyao_GNC_1 : !!
 {@n : @nonce}
 {fresh,fresh' : nat}
 (@n :=(FRESH @nonce fresh))->
 (fresh' :=(suc fresh))->
 [L_dolevyao_GNC_1]:
 (F fresh)
  =>
 (union(union(F fresh')(union(T_dolevyao_INT)(union(T_dolevyao_TRN)(union(T_dolevyao_DCM)(union(T_dolevyao_CMP)(union(
    T_dolevyao_IPR)(union(T_dolevyao_GMS)(union(T_dolevyao_DEL)(T_dolevyao_DUP)))))))))(@I @n)))
(R_dolevyao_GNC_2 : !!
 {@n : @nonce}
 {fresh,fresh' : nat}
 (@n :=(FRESH @nonce fresh))->
 (fresh' :=(suc fresh))->
 [L_dolevyao_GNC_2]:
 (union(F fresh)(T_dolevyao_GNC))
  =>
 (union(F fresh')(@I @n)))
(R_dolevyao_GMS_1 : !!
 {@m : @msg}
 {fresh,fresh' : nat}
 (@m :=(FRESH @msg fresh))->
 (fresh' :=(suc fresh))->
 [L_dolevyao_GMS_1]:
 (F fresh)
  =>
 (union(union(F fresh')(union(T_dolevyao_INT)(union(T_dolevyao_TRN)(union(T_dolevyao_DCM)(union(T_dolevyao_CMP)(union(
    T_dolevyao_IPR)(union(T_dolevyao_GNC)(union(T_dolevyao_DEL)(T_dolevyao_DUP)))))))))(@I @m)))
(R_dolevyao_GMS_2 : !!
 {@m : @msg}
 {fresh,fresh' : nat}
 (@m :=(FRESH @msg fresh))->
 (fresh' :=(suc fresh))->
 [L_dolevyao_GMS_2]:
 (union(F fresh)(T_dolevyao_GMS))
  =>
 (union(F fresh')(@I @m)))
(R_dolevyao_DEL_1 : !!
 {@t : @msg}
 {fresh,fresh' : nat}
 (fresh' := fresh)->
 [L_dolevyao_DEL_1]:
 (union(F fresh)(@I @t))
  =>
 (union(F fresh')(union(T_dolevyao_INT)(union(T_dolevyao_TRN)(union(T_dolevyao_DCM)(union(T_dolevyao_CMP)(union(
    T_dolevyao_IPR)(union(T_dolevyao_GNC)(union(T_dolevyao_GMS)(T_dolevyao_DUP))))))))))
(R_dolevyao_DEL_2 : !!
 {@t : @msg}
 {fresh,fresh' : nat}
 (fresh' := fresh)->
 [L_dolevyao_DEL_2]:
 (union(union(F fresh)(T_dolevyao_DEL))(@I @t))
  =>
 (F fresh'))
(R_dolevyao_DUP_1 : !!
 {@t : @msg}
 {fresh,fresh' : nat}
 (fresh' := fresh)->
 [L_dolevyao_DUP_1]:
 (union(F fresh)(@I @t))
  =>
 (union(union(F fresh')(union(T_dolevyao_INT)(union(T_dolevyao_TRN)(union(T_dolevyao_DCM)(union(T_dolevyao_CMP)(union(
    T_dolevyao_IPR)(union(T_dolevyao_GNC)(union(T_dolevyao_GMS)(T_dolevyao_DEL)))))))))(union(@I @t)(@I @t))))
(R_dolevyao_DUP_2 : !!
 {@t : @msg}
 {fresh,fresh' : nat}
 (fresh' := fresh)->
 [L_dolevyao_DUP_2]:
 (union(union(F fresh)(T_dolevyao_DUP))(@I @t))
  =>
 (union(F fresh')(union(@I @t)(@I @t))))

(L_dolevyao-ns2_PDC_1 : act)
(L_dolevyao-ns2_PDC_2 : act)
(L_dolevyao-ns2_PEC_1 : act)
(L_dolevyao-ns2_PEC_2 : act)
(T_dolevyao-ns2_PDC : @state)
(T_dolevyao-ns2_PEC : @state)
(R_dolevyao-ns2_PDC_1 : !!
 {@A : @princ}
 {@k : @pubK @A}
 {@k' : @privK @A}
 {@t : @msg}
 {fresh,fresh' : nat}
 (fresh' := fresh)->
 [L_dolevyao-ns2_PDC_1]:
 (union(F fresh)(union(@I(@encrypt @k @t))(@I @k')))
  =>
 (union(union(F fresh')(T_dolevyao-ns2_PEC))(@I @t)))
(R_dolevyao-ns2_PDC_2 : !!
 {@A : @princ}
 {@k : @pubK @A}
 {@k' : @privK @A}
 {@t : @msg}
 {fresh,fresh' : nat}
 (fresh' := fresh)->
 [L_dolevyao-ns2_PDC_2]:
 (union(union(F fresh)(T_dolevyao-ns2_PDC))(union(@I(@encrypt @k @t))(@I @k')))
  =>
 (union(F fresh')(@I @t)))
(R_dolevyao-ns2_PEC_1 : !!
 {@A : @princ}
 {@k : @pubK @a}
 {@t : @msg}
 {fresh,fresh' : nat}
 (fresh' := fresh)->
 [L_dolevyao-ns2_PEC_1]:
 (union(F fresh)(union(@I @t)(@I @k)))
  =>
 (union(union(F fresh')(T_dolevyao-ns2_PDC))(@I(@encrypt @k @t))))
(R_dolevyao-ns2_PEC_2 : !!
 {@A : @princ}
 {@k : @pubK @a}
 {@t : @msg}
 {fresh,fresh' : nat}
 (fresh' := fresh)->
 [L_dolevyao-ns2_PEC_2]:
 (union(union(F fresh)(T_dolevyao-ns2_PEC))(union(@I @t)(@I @k)))
  =>
 (union(F fresh')(@I(@encrypt @k @t))))

(config :=(union(F 0)(union(union(union(union(union(union(EL @princ @A)(EL @princ @B))(EL(@pubK @A)@pkA))(EL(@pubK
    @B)@pkB))(EL @princ @i))(EL(@pubK @i)@pubK-i))(union(@START-1 @A)(union(@START-2 @B)(@I(@privK-knowledge
    @privK-i)))))))
(red config)