(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)
(@KAS : Type)
(@server : Type)
(@tcs : Type)
(@ts : Type)
(@TGS : Type)
(@client : Type)
(@KAS-princ : @KAS -> @princ)
(@tcs-princ : @tcs -> @princ)
(@ts-tcs : @ts -> @tcs)
(@TGS-ts : @TGS -> @ts)
(@server-ts : @server -> @ts)
(@client-tcs : @client -> @tcs)
(@key : Type)
(@dbK : @tcs -> Type)
(@shK : @client -> @ts -> Type)
(@dbK-key : {@A | @tcs}(@dbK @A)-> @key)
(@shK-key : {@C | @client}{@A | @ts}(@shK @C @A)-> @key)
(@shK-msg : {@C | @client}{@A | @ts}(@shK @C @A)-> @msg)
(@time : Type)
(@time-msg : @time -> @msg)
(@encrypt : @key -> @msg -> @msg)
(@Auth : {@C : @client}@msg ->{@T : @TGS}(@shK @C(@TGS-ts @T))-> @state)
(@Service : {@C : @client}@msg ->{@S : @server}(@shK @C(@server-ts @S))-> @state)
(@Mem : {@S : @server}{@C : @client}(@shK @C(@server-ts @S))-> @time -> @state)
(@DoneMut : {@C : @client}{@S : @server}(@shK @C(@server-ts @S))-> @state)
(@START-ASE : @client -> @TGS -> @state)
(@START-TGE : @client -> @state)
(@START-CSE : @client -> @state)
(@C : @client)
(@AS : @KAS)
(@TS : @TGS)
(@S : @server)
(@kC : @dbK(@client-tcs @C))
(@kTS : @dbK(@ts-tcs(@TGS-ts @TS)))
(@kS : @dbK(@ts-tcs(@server-ts @S)))
(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)))
(L_clientASE_req_1 : act)
(L_clientASE_req_2 : act)
(L_clientASE_resp_1 : act)
(L_clientASE_resp_2 : act)
(T_clientASE_req : @client ->(@client -> @TGS -> @nonce -> @state)-> @state)
(T_clientASE_resp : @client ->(@client -> @TGS -> @nonce -> @state)-> @state)
(R_clientASE_req_1 : !!
 {@C : @client}
 {@L : @client -> @TGS -> @nonce -> @state}
 {@T : @TGS}
 {@n1 : @nonce}
 {fresh,fresh' : nat}
 (@L :=(FRESH(@client -> @TGS -> @nonce -> @state)fresh))->
 (@n1 :=(FRESH @nonce(suc fresh)))->
 (fresh' :=(suc(suc fresh)))->
 [L_clientASE_req_1]:
 (union(F fresh)(@START-ASE @C @T))
  =>
 (union(union(F fresh')(T_clientASE_resp @C @L))(union(@N(@&(@princ-msg(@tcs-princ(@client-tcs @C)))(@&(@princ-msg(
    @tcs-princ(@ts-tcs(@TGS-ts @T))))(@nonce-msg @n1))))(@L @C @T @n1))))
(R_clientASE_req_2 : !!
 {@C : @client}
 {@L : @client -> @TGS -> @nonce -> @state}
 {@T : @TGS}
 {@n1 : @nonce}
 {fresh,fresh' : nat}
 (@n1 :=(FRESH @nonce fresh))->
 (fresh' :=(suc fresh))->
 [L_clientASE_req_2]:
 (union(union(F fresh)(T_clientASE_req @C @L))(@START-ASE @C @T))
  =>
 (union(F fresh')(union(@N(@&(@princ-msg(@tcs-princ(@client-tcs @C)))(@&(@princ-msg(@tcs-princ(@ts-tcs(@TGS-ts @T))))(
    @nonce-msg @n1))))(@L @C @T @n1))))
(R_clientASE_resp_1 : !!
 {@C : @client}
 {@L : @client -> @TGS -> @nonce -> @state}
 {@X : @msg}
 {@T : @TGS}
 {@kC : @dbK(@client-tcs @C)}
 {@AKey : @shK @C(@TGS-ts @T)}
 {@n1 : @nonce}
 {fresh,fresh' : nat}
 (@L :=(FRESH(@client -> @TGS -> @nonce -> @state)fresh))->
 (fresh' :=(suc fresh))->
 [L_clientASE_resp_1]:
 (union(F fresh)(union(@N(@&(@princ-msg(@tcs-princ(@client-tcs @C)))(@& @X(@encrypt(@dbK-key @kC)(@&(@shK-msg @AKey)(@&(
    @nonce-msg @n1)(@princ-msg(@tcs-princ(@ts-tcs(@TGS-ts @T))))))))))(@L @C @T @n1)))
  =>
 (union(union(F fresh')(T_clientASE_req @C @L))(@Auth @C @X @T @AKey)))
(R_clientASE_resp_2 : !!
 {@C : @client}
 {@L : @client -> @TGS -> @nonce -> @state}
 {@X : @msg}
 {@T : @TGS}
 {@kC : @dbK(@client-tcs @C)}
 {@AKey : @shK @C(@TGS-ts @T)}
 {@n1 : @nonce}
 {fresh,fresh' : nat}
 (fresh' := fresh)->
 [L_clientASE_resp_2]:
 (union(union(F fresh)(T_clientASE_resp @C @L))(union(@N(@&(@princ-msg(@tcs-princ(@client-tcs @C)))(@& @X(@encrypt(@dbK-key
    @kC)(@&(@shK-msg @AKey)(@&(@nonce-msg @n1)(@princ-msg(@tcs-princ(@ts-tcs(@TGS-ts @T))))))))))(@L @C @T @n1)))
  =>
 (union(F fresh')(@Auth @C @X @T @AKey)))

(L_serverASE_answer_1 : act)
(L_serverASE_answer_2 : act)
(T_serverASE_answer : @KAS -> @state)
(R_serverASE_answer_1 : !!
 {@K : @KAS}
 {@C : @client}
 {@T : @TGS}
 {@n1 : @nonce}
 {@kC : @dbK(@client-tcs @C)}
 {@kT : @dbK(@ts-tcs(@TGS-ts @T))}
 {@AKey : @shK @C(@TGS-ts @T)}
 {fresh,fresh' : nat}
 (@AKey :=(FRESH(@shK @C(@TGS-ts @T))fresh))->
 (fresh' :=(suc fresh))->
 [L_serverASE_answer_1]:
 (union(union(F fresh)(union(EL(@dbK(@ts-tcs(@TGS-ts @T)))@kT)(EL(@dbK(@client-tcs @C))@kC)))(@N(@&(@princ-msg(@tcs-princ(
    @client-tcs @C)))(@&(@princ-msg(@tcs-princ(@ts-tcs(@TGS-ts @T))))(@nonce-msg @n1)))))
  =>
 (union(union(F fresh')(union(EL(@dbK(@ts-tcs(@TGS-ts @T)))@kT)(EL(@dbK(@client-tcs @C))@kC)))(@N(@&(@princ-msg(@tcs-princ(
    @client-tcs @C)))(@&(@encrypt(@dbK-key @kT)(@&(@shK-msg @AKey)(@princ-msg(@tcs-princ(@client-tcs @C)))))(@encrypt(
    @dbK-key @kC)(@&(@shK-msg @AKey)(@&(@nonce-msg @n1)(@princ-msg(@tcs-princ(@ts-tcs(@TGS-ts @T))))))))))))
(R_serverASE_answer_2 : !!
 {@K : @KAS}
 {@C : @client}
 {@T : @TGS}
 {@n1 : @nonce}
 {@kC : @dbK(@client-tcs @C)}
 {@kT : @dbK(@ts-tcs(@TGS-ts @T))}
 {@AKey : @shK @C(@TGS-ts @T)}
 {fresh,fresh' : nat}
 (@AKey :=(FRESH(@shK @C(@TGS-ts @T))fresh))->
 (fresh' :=(suc fresh))->
 [L_serverASE_answer_2]:
 (union(union(union(F fresh)(T_serverASE_answer @K))(union(EL(@dbK(@ts-tcs(@TGS-ts @T)))@kT)(EL(@dbK(@client-tcs
    @C))@kC)))(@N(@&(@princ-msg(@tcs-princ(@client-tcs @C)))(@&(@princ-msg(@tcs-princ(@ts-tcs(@TGS-ts @T))))(@nonce-msg
    @n1)))))
  =>
 (union(union(F fresh')(union(EL(@dbK(@ts-tcs(@TGS-ts @T)))@kT)(EL(@dbK(@client-tcs @C))@kC)))(@N(@&(@princ-msg(@tcs-princ(
    @client-tcs @C)))(@&(@encrypt(@dbK-key @kT)(@&(@shK-msg @AKey)(@princ-msg(@tcs-princ(@client-tcs @C)))))(@encrypt(
    @dbK-key @kC)(@&(@shK-msg @AKey)(@&(@nonce-msg @n1)(@princ-msg(@tcs-princ(@ts-tcs(@TGS-ts @T))))))))))))

(L_clientTGE_req_1 : act)
(L_clientTGE_req_2 : act)
(L_clientTGE_resp_1 : act)
(L_clientTGE_resp_2 : act)
(T_clientTGE_req : @client ->(@client -> @server -> @TGS -> @nonce -> @state)-> @state)
(T_clientTGE_resp : @client ->(@client -> @server -> @TGS -> @nonce -> @state)-> @state)
(R_clientTGE_req_1 : !!
 {@C : @client}
 {@L : @client -> @server -> @TGS -> @nonce -> @state}
 {@T : @TGS}
 {@S : @server}
 {@AKey : @shK @C(@TGS-ts @T)}
 {@X : @msg}
 {@n2 : @nonce}
 {fresh,fresh' : nat}
 (@L :=(FRESH(@client -> @server -> @TGS -> @nonce -> @state)fresh))->
 (@n2 :=(FRESH @nonce(suc fresh)))->
 (fresh' :=(suc(suc fresh)))->
 [L_clientTGE_req_1]:
 (union(union(F fresh)(EL @server @S))(union(@START-TGE @C)(@Auth @C @X @T @AKey)))
  =>
 (union(union(union(F fresh')(T_clientTGE_resp @C @L))(EL @server @S))(union(union(@N(@& @X(@&(@encrypt(@shK-key @AKey)(
    @princ-msg(@tcs-princ(@client-tcs @C))))(@&(@princ-msg(@tcs-princ(@client-tcs @C)))(@&(@princ-msg(@tcs-princ(@ts-tcs(
    @server-ts @S))))(@nonce-msg @n2))))))(@L @C @S @T @n2))(@Auth @C @X @T @AKey))))
(R_clientTGE_req_2 : !!
 {@C : @client}
 {@L : @client -> @server -> @TGS -> @nonce -> @state}
 {@T : @TGS}
 {@S : @server}
 {@AKey : @shK @C(@TGS-ts @T)}
 {@X : @msg}
 {@n2 : @nonce}
 {fresh,fresh' : nat}
 (@n2 :=(FRESH @nonce fresh))->
 (fresh' :=(suc fresh))->
 [L_clientTGE_req_2]:
 (union(union(union(F fresh)(T_clientTGE_req @C @L))(EL @server @S))(union(@START-TGE @C)(@Auth @C @X @T @AKey)))
  =>
 (union(union(F fresh')(EL @server @S))(union(union(@N(@& @X(@&(@encrypt(@shK-key @AKey)(@princ-msg(@tcs-princ(@client-tcs
    @C))))(@&(@princ-msg(@tcs-princ(@client-tcs @C)))(@&(@princ-msg(@tcs-princ(@ts-tcs(@server-ts @S))))(@nonce-msg
    @n2))))))(@L @C @S @T @n2))(@Auth @C @X @T @AKey))))
(R_clientTGE_resp_1 : !!
 {@C : @client}
 {@L : @client -> @server -> @TGS -> @nonce -> @state}
 {@T : @TGS}
 {@S : @server}
 {@SKey : @shK @C(@server-ts @S)}
 {@AKey : @shK @C(@TGS-ts @T)}
 {@Y : @msg}
 {@n2 : @nonce}
 {fresh,fresh' : nat}
 (@L :=(FRESH(@client -> @server -> @TGS -> @nonce -> @state)fresh))->
 (fresh' :=(suc fresh))->
 [L_clientTGE_resp_1]:
 (union(F fresh)(union(@N(@&(@princ-msg(@tcs-princ(@client-tcs @C)))(@& @Y(@encrypt(@shK-key @AKey)(@&(@shK-msg @SKey)(@&(
    @nonce-msg @n2)(@princ-msg(@tcs-princ(@ts-tcs(@server-ts @S))))))))))(@L @C @S @T @n2)))
  =>
 (union(union(F fresh')(T_clientTGE_req @C @L))(@Service @C @Y @S @SKey)))
(R_clientTGE_resp_2 : !!
 {@C : @client}
 {@L : @client -> @server -> @TGS -> @nonce -> @state}
 {@T : @TGS}
 {@S : @server}
 {@SKey : @shK @C(@server-ts @S)}
 {@AKey : @shK @C(@TGS-ts @T)}
 {@Y : @msg}
 {@n2 : @nonce}
 {fresh,fresh' : nat}
 (fresh' := fresh)->
 [L_clientTGE_resp_2]:
 (union(union(F fresh)(T_clientTGE_resp @C @L))(union(@N(@&(@princ-msg(@tcs-princ(@client-tcs @C)))(@& @Y(@encrypt(@shK-key
    @AKey)(@&(@shK-msg @SKey)(@&(@nonce-msg @n2)(@princ-msg(@tcs-princ(@ts-tcs(@server-ts @S))))))))))(@L @C @S @T @n2)))
  =>
 (union(F fresh')(@Service @C @Y @S @SKey)))

(L_serverTGE_answer_1 : act)
(L_serverTGE_answer_2 : act)
(T_serverTGE_answer : @TGS -> @state)
(R_serverTGE_answer_1 : !!
 {@T : @TGS}
 {@C : @client}
 {@S : @server}
 {@AKey : @shK @C(@TGS-ts @T)}
 {@kT : @dbK(@ts-tcs(@TGS-ts @T))}
 {@kS : @dbK(@ts-tcs(@server-ts @S))}
 {@n2 : @nonce}
 {@SKey : @shK @C(@server-ts @S)}
 {fresh,fresh' : nat}
 (@SKey :=(FRESH(@shK @C(@server-ts @S))fresh))->
 (fresh' :=(suc fresh))->
 [L_serverTGE_answer_1]:
 (union(union(F fresh)(EL(@dbK(@ts-tcs(@server-ts @S)))@kS))(@N(@&(@encrypt(@dbK-key @kT)(@&(@shK-msg @AKey)(@princ-msg(
    @tcs-princ(@client-tcs @C)))))(@&(@encrypt(@shK-key @AKey)(@princ-msg(@tcs-princ(@client-tcs @C))))(@&(@princ-msg(
    @tcs-princ(@client-tcs @C)))(@&(@princ-msg(@tcs-princ(@ts-tcs(@server-ts @S))))(@nonce-msg @n2)))))))
  =>
 (union(union(F fresh')(EL(@dbK(@ts-tcs(@server-ts @S)))@kS))(@N(@&(@princ-msg(@tcs-princ(@client-tcs @C)))(@&(@encrypt(
    @dbK-key @kS)(@&(@shK-msg @SKey)(@princ-msg(@tcs-princ(@client-tcs @C)))))(@encrypt(@shK-key @AKey)(@&(@shK-msg @SKey)(
    @&(@nonce-msg @n2)(@princ-msg(@tcs-princ(@ts-tcs(@server-ts @S))))))))))))
(R_serverTGE_answer_2 : !!
 {@T : @TGS}
 {@C : @client}
 {@S : @server}
 {@AKey : @shK @C(@TGS-ts @T)}
 {@kT : @dbK(@ts-tcs(@TGS-ts @T))}
 {@kS : @dbK(@ts-tcs(@server-ts @S))}
 {@n2 : @nonce}
 {@SKey : @shK @C(@server-ts @S)}
 {fresh,fresh' : nat}
 (@SKey :=(FRESH(@shK @C(@server-ts @S))fresh))->
 (fresh' :=(suc fresh))->
 [L_serverTGE_answer_2]:
 (union(union(union(F fresh)(T_serverTGE_answer @T))(EL(@dbK(@ts-tcs(@server-ts @S)))@kS))(@N(@&(@encrypt(@dbK-key @kT)(@&(
    @shK-msg @AKey)(@princ-msg(@tcs-princ(@client-tcs @C)))))(@&(@encrypt(@shK-key @AKey)(@princ-msg(@tcs-princ(@client-tcs
    @C))))(@&(@princ-msg(@tcs-princ(@client-tcs @C)))(@&(@princ-msg(@tcs-princ(@ts-tcs(@server-ts @S))))(@nonce-msg
    @n2)))))))
  =>
 (union(union(F fresh')(EL(@dbK(@ts-tcs(@server-ts @S)))@kS))(@N(@&(@princ-msg(@tcs-princ(@client-tcs @C)))(@&(@encrypt(
    @dbK-key @kS)(@&(@shK-msg @SKey)(@princ-msg(@tcs-princ(@client-tcs @C)))))(@encrypt(@shK-key @AKey)(@&(@shK-msg @SKey)(
    @&(@nonce-msg @n2)(@princ-msg(@tcs-princ(@ts-tcs(@server-ts @S))))))))))))

(L_clientCSE_req_1 : act)
(L_clientCSE_req_2 : act)
(L_clientCSE_resp_1 : act)
(L_clientCSE_resp_2 : act)
(T_clientCSE_req : @client ->({@C : @client}{@S : @server}(@shK @C(@server-ts @S))-> @time -> @msg -> @state)-> @state)
(T_clientCSE_resp : @client ->({@C : @client}{@S : @server}(@shK @C(@server-ts @S))-> @time -> @msg -> @state)-> @state)
(R_clientCSE_req_1 : !!
 {@C : @client}
 {@L : {@C : @client}{@S : @server}(@shK @C(@server-ts @S))-> @time -> @msg -> @state}
 {@S : @server}
 {@SKey : @shK @C(@server-ts @S)}
 {@Y : @msg}
 {@t : @time}
 {fresh,fresh' : nat}
 (@L :=(FRESH({@C : @client}{@S : @server}(@shK @C(@server-ts @S))-> @time -> @msg -> @state)fresh))->
 (@t :=(FRESH @time(suc fresh)))->
 (fresh' :=(suc(suc fresh)))->
 [L_clientCSE_req_1]:
 (union(F fresh)(union(@START-CSE @C)(@Service @C @Y @S @SKey)))
  =>
 (union(union(F fresh')(T_clientCSE_resp @C @L))(union(@Service @C @Y @S @SKey)(union(@N(@& @Y(@encrypt(@shK-key @SKey)(@&(
    @princ-msg(@tcs-princ(@client-tcs @C)))(@time-msg @t)))))(@L @C @S @SKey @t @Y)))))
(R_clientCSE_req_2 : !!
 {@C : @client}
 {@L : {@C : @client}{@S : @server}(@shK @C(@server-ts @S))-> @time -> @msg -> @state}
 {@S : @server}
 {@SKey : @shK @C(@server-ts @S)}
 {@Y : @msg}
 {@t : @time}
 {fresh,fresh' : nat}
 (@t :=(FRESH @time fresh))->
 (fresh' :=(suc fresh))->
 [L_clientCSE_req_2]:
 (union(union(F fresh)(T_clientCSE_req @C @L))(union(@START-CSE @C)(@Service @C @Y @S @SKey)))
  =>
 (union(F fresh')(union(@Service @C @Y @S @SKey)(union(@N(@& @Y(@encrypt(@shK-key @SKey)(@&(@princ-msg(@tcs-princ(
    @client-tcs @C)))(@time-msg @t)))))(@L @C @S @SKey @t @Y)))))
(R_clientCSE_resp_1 : !!
 {@C : @client}
 {@L : {@C : @client}{@S : @server}(@shK @C(@server-ts @S))-> @time -> @msg -> @state}
 {@S : @server}
 {@SKey : @shK @C(@server-ts @S)}
 {@t : @time}
 {@Y : @msg}
 {fresh,fresh' : nat}
 (@L :=(FRESH({@C : @client}{@S : @server}(@shK @C(@server-ts @S))-> @time -> @msg -> @state)fresh))->
 (fresh' :=(suc fresh))->
 [L_clientCSE_resp_1]:
 (union(F fresh)(union(@N(@encrypt(@shK-key @SKey)(@time-msg @t)))(@L @C @S @SKey @t @Y)))
  =>
 (union(union(F fresh')(T_clientCSE_req @C @L))(@DoneMut @C @S @SKey)))
(R_clientCSE_resp_2 : !!
 {@C : @client}
 {@L : {@C : @client}{@S : @server}(@shK @C(@server-ts @S))-> @time -> @msg -> @state}
 {@S : @server}
 {@SKey : @shK @C(@server-ts @S)}
 {@t : @time}
 {@Y : @msg}
 {fresh,fresh' : nat}
 (fresh' := fresh)->
 [L_clientCSE_resp_2]:
 (union(union(F fresh)(T_clientCSE_resp @C @L))(union(@N(@encrypt(@shK-key @SKey)(@time-msg @t)))(@L @C @S @SKey @t @Y)))
  =>
 (union(F fresh')(@DoneMut @C @S @SKey)))

(L_serverCSE_answer_1 : act)
(L_serverCSE_answer_2 : act)
(T_serverCSE_answer : @server -> @state)
(R_serverCSE_answer_1 : !!
 {@S : @server}
 {@C : @client}
 {@SKey : @shK @C(@server-ts @S)}
 {@t : @time}
 {@kS : @dbK(@ts-tcs(@server-ts @S))}
 {@X : @msg}
 {fresh,fresh' : nat}
 (fresh' := fresh)->
 [L_serverCSE_answer_1]:
 (union(union(F fresh)(EL @server @S))(@N(@&(@encrypt(@dbK-key @kS)@X)(@encrypt(@shK-key @SKey)(@&(@princ-msg(@tcs-princ(
    @client-tcs @C)))(@time-msg @t))))))
  =>
 (union(union(F fresh')(EL @server @S))(union(@N(@encrypt(@shK-key @SKey)(@time-msg @t)))(@Mem @S @C @SKey @t))))
(R_serverCSE_answer_2 : !!
 {@S : @server}
 {@C : @client}
 {@SKey : @shK @C(@server-ts @S)}
 {@t : @time}
 {@kS : @dbK(@ts-tcs(@server-ts @S))}
 {@X : @msg}
 {fresh,fresh' : nat}
 (fresh' := fresh)->
 [L_serverCSE_answer_2]:
 (union(union(union(F fresh)(T_serverCSE_answer @S))(EL @server @S))(@N(@&(@encrypt(@dbK-key @kS)@X)(@encrypt(@shK-key
    @SKey)(@&(@princ-msg(@tcs-princ(@client-tcs @C)))(@time-msg @t))))))
  =>
 (union(union(F fresh')(EL @server @S))(union(@N(@encrypt(@shK-key @SKey)(@time-msg @t)))(@Mem @S @C @SKey @t))))

(config :=(union(F 0)(union(union(union(union(union(EL @KAS @AS)(EL @server @S))(EL(@dbK(@client-tcs @C))@kC))(EL(@dbK(
    @ts-tcs(@TGS-ts @TS)))@kTS))(EL(@dbK(@ts-tcs(@server-ts @S)))@kS))(union(@START-ASE @C @TS)(union(@START-TGE @C)(
    @START-CSE @C))))))
(red config)