theory Yubikey begin

// Function signature and definition of the equational theory E

builtins: multiset
functions: fst/1, pair/2, sdec/2, senc/2, snd/1
equations:
    fst(<x.1, x.2>) = x.1,
    sdec(senc(x.1, x.2), x.2) = x.1,
    snd(<x.1, x.2>) = x.2

section{* The Yubikey-Protocol *}

rule (modulo E) 0:
   [ ] --[ Init( ) ]-> [ State_0( ) ]

  /* has exactly the trivial AC variant */

rule (modulo E) Par0:
   [ State_0( ) ] --> [ !State_01( ), !State_02( ) ]

  /* has exactly the trivial AC variant */

rule (modulo E) Rep01:
   [ !State_01( ) ] --> [ State_011( ) ]

  /* has exactly the trivial AC variant */

rule (modulo E) in__L_pid__nonce__senc__secretid__tc__npr___k__011:
   [ State_011( ), In( <L_pid, nonce, senc(<secretid, tc, npr>, k)> )
   ]
  -->
   [ State_0111( L_pid, k, nonce, npr, secretid, tc ) ]

  /* has exactly the trivial AC variant */

rule (modulo E) lock___Server___L_pid_0111:
   [ State_0111( L_pid, k, nonce, npr, secretid, tc ), Fr( ~lock11 ) ]
  --[ Lock( ~lock11, <'Server', L_pid> ) ]->
   [ State_01111( ~lock11, L_pid, k, nonce, npr, secretid, tc ) ]

  /* has exactly the trivial AC variant */

rule (modulo E) lookup___Server___L_pid__as_tuple01111:
   [ State_01111( ~lock11, L_pid, k, nonce, npr, secretid, tc ) ]
  --[ IsIn( <'Server', L_pid>, tuple ) ]->
   [
   State_011111( ~lock11, L_pid, k, nonce, npr, secretid, tc, tuple )
   ]

  /* has exactly the trivial AC variant */

rule (modulo E) else__lookup___Server___L_pid__as_tuple01111:
   [ State_01111( ~lock11, L_pid, k, nonce, npr, secretid, tc ) ]
  --[ IsNotSet( <'Server', L_pid> ) ]->
   [ State_011112( ~lock11, L_pid, k, nonce, npr, secretid, tc ) ]

  /* has exactly the trivial AC variant */

rule (modulo E) if_eq_fst_tuple___secretid_011111:
   [
   State_011111( ~lock11, L_pid, k, nonce, npr, secretid, tc, tuple )
   ]
  --[ Pred_eq( fst(tuple), secretid ) ]->
   [
   State_0111111( ~lock11, L_pid, k, nonce, npr, secretid, tc, tuple )
   ]

  /*
  rule (modulo AC) if_eq_fst_tuple___secretid_011111:
     [
     State_011111( ~lock11, L_pid, k, nonce, npr, secretid, tc, tuple )
     ]
    --[ Pred_eq( z, secretid ) ]->
     [
     State_0111111( ~lock11, L_pid, k, nonce, npr, secretid, tc, tuple )
     ]
    variants (modulo AC)
    1. tuple = tuple.10
       z     = fst(tuple.10)
    
    2. tuple = <x.10, x.11>
       z     = x.10
  */

rule (modulo E) else__if_eq_fst_tuple___secretid_011111:
   [
   State_011111( ~lock11, L_pid, k, nonce, npr, secretid, tc, tuple )
   ]
  --[ Pred_not_eq( fst(tuple), secretid ) ]->
   [
   State_0111112( ~lock11, L_pid, k, nonce, npr, secretid, tc, tuple )
   ]

  /*
  rule (modulo AC) else__if_eq_fst_tuple___secretid_011111:
     [
     State_011111( ~lock11, L_pid, k, nonce, npr, secretid, tc, tuple )
     ]
    --[ Pred_not_eq( z, secretid ) ]->
     [
     State_0111112( ~lock11, L_pid, k, nonce, npr, secretid, tc, tuple )
     ]
    variants (modulo AC)
    1. tuple = tuple.10
       z     = fst(tuple.10)
    
    2. tuple = <x.10, x.11>
       z     = x.10
  */

rule (modulo E) if_eq_fst_snd_tuple____k_0111111:
   [
   State_0111111( ~lock11, L_pid, k, nonce, npr, secretid, tc, tuple )
   ]
  --[ Pred_eq( fst(snd(tuple)), k ) ]->
   [
   State_01111111( ~lock11, L_pid, k, nonce, npr, secretid, tc, tuple
   )
   ]

  /*
  rule (modulo AC) if_eq_fst_snd_tuple____k_0111111:
     [
     State_0111111( ~lock11, L_pid, k, nonce, npr, secretid, tc, tuple )
     ]
    --[ Pred_eq( z, k ) ]->
     [
     State_01111111( ~lock11, L_pid, k, nonce, npr, secretid, tc, tuple
     )
     ]
    variants (modulo AC)
    1. tuple = tuple.10
       z     = fst(snd(tuple.10))
    
    2. tuple = <x.10, x.11>
       z     = fst(x.11)
    
    3. tuple = <x.10, x.11, x.12>
       z     = x.11
  */

rule (modulo E) else__if_eq_fst_snd_tuple____k_0111111:
   [
   State_0111111( ~lock11, L_pid, k, nonce, npr, secretid, tc, tuple )
   ]
  --[ Pred_not_eq( fst(snd(tuple)), k ) ]->
   [
   State_01111112( ~lock11, L_pid, k, nonce, npr, secretid, tc, tuple
   )
   ]

  /*
  rule (modulo AC) else__if_eq_fst_snd_tuple____k_0111111:
     [
     State_0111111( ~lock11, L_pid, k, nonce, npr, secretid, tc, tuple )
     ]
    --[ Pred_not_eq( z, k ) ]->
     [
     State_01111112( ~lock11, L_pid, k, nonce, npr, secretid, tc, tuple
     )
     ]
    variants (modulo AC)
    1. tuple = tuple.10
       z     = fst(snd(tuple.10))
    
    2. tuple = <x.10, x.11>
       z     = fst(x.11)
    
    3. tuple = <x.10, x.11, x.12>
       z     = x.11
  */

rule (modulo E) in_otc01111111:
   [
   State_01111111( ~lock11, L_pid, k, nonce, npr, secretid, tc, tuple
   ),
   In( otc )
   ]
  -->
   [
   State_011111111( ~lock11, L_pid, k, nonce, npr, otc, secretid, tc,
                    tuple
   )
   ]

  /* has exactly the trivial AC variant */

rule (modulo E) if_eq_snd_snd_tuple____otc_011111111:
   [
   State_011111111( ~lock11, L_pid, k, nonce, npr, otc, secretid, tc,
                    tuple
   )
   ]
  --[ Pred_eq( snd(snd(tuple)), otc ) ]->
   [
   State_0111111111( ~lock11, L_pid, k, nonce, npr, otc, secretid, tc,
                     tuple
   )
   ]

  /*
  rule (modulo AC) if_eq_snd_snd_tuple____otc_011111111:
     [
     State_011111111( ~lock11, L_pid, k, nonce, npr, otc, secretid, tc,
                      tuple
     )
     ]
    --[ Pred_eq( z, otc ) ]->
     [
     State_0111111111( ~lock11, L_pid, k, nonce, npr, otc, secretid, tc,
                       tuple
     )
     ]
    variants (modulo AC)
    1. tuple = tuple.11
       z     = snd(snd(tuple.11))
    
    2. tuple = <x.11, x.12>
       z     = snd(x.12)
    
    3. tuple = <x.11, x.12, x.13>
       z     = x.13
  */

rule (modulo E) else__if_eq_snd_snd_tuple____otc_011111111:
   [
   State_011111111( ~lock11, L_pid, k, nonce, npr, otc, secretid, tc,
                    tuple
   )
   ]
  --[ Pred_not_eq( snd(snd(tuple)), otc ) ]->
   [
   State_0111111112( ~lock11, L_pid, k, nonce, npr, otc, secretid, tc,
                     tuple
   )
   ]

  /*
  rule (modulo AC) else__if_eq_snd_snd_tuple____otc_011111111:
     [
     State_011111111( ~lock11, L_pid, k, nonce, npr, otc, secretid, tc,
                      tuple
     )
     ]
    --[ Pred_not_eq( z, otc ) ]->
     [
     State_0111111112( ~lock11, L_pid, k, nonce, npr, otc, secretid, tc,
                       tuple
     )
     ]
    variants (modulo AC)
    1. tuple = tuple.11
       z     = snd(snd(tuple.11))
    
    2. tuple = <x.11, x.12>
       z     = snd(x.12)
    
    3. tuple = <x.11, x.12, x.13>
       z     = x.13
  */

rule (modulo E) if_smaller_otc__tc_0111111111:
   [
   State_0111111111( ~lock11, L_pid, k, nonce, npr, otc, secretid, tc,
                     tuple
   )
   ]
  --[ Pred_smaller( otc, tc ) ]->
   [
   State_01111111111( ~lock11, L_pid, k, nonce, npr, otc, secretid,
                      tc, tuple
   )
   ]

  /* has exactly the trivial AC variant */

rule (modulo E) else__if_smaller_otc__tc_0111111111:
   [
   State_0111111111( ~lock11, L_pid, k, nonce, npr, otc, secretid, tc,
                     tuple
   )
   ]
  --[ Pred_not_smaller( otc, tc ) ]->
   [
   State_01111111112( ~lock11, L_pid, k, nonce, npr, otc, secretid,
                      tc, tuple
   )
   ]

  /* has exactly the trivial AC variant */

rule (modulo E) event_InitStuff_L_pid__secretid__k__tuple__otc__tc_01111111111:
   [
   State_01111111111( ~lock11, L_pid, k, nonce, npr, otc, secretid,
                      tc, tuple
   )
   ]
  --[ Event( ), InitStuff( L_pid, secretid, k, tuple, otc, tc ) ]->
   [
   State_011111111111( ~lock11, L_pid, k, nonce, npr, otc, secretid,
                       tc, tuple
   )
   ]

  /* has exactly the trivial AC variant */

rule (modulo E) event_Login_L_pid__k__tc_011111111111:
   [
   State_011111111111( ~lock11, L_pid, k, nonce, npr, otc, secretid,
                       tc, tuple
   )
   ]
  --[ Event( ), Login( L_pid, k, tc ) ]->
   [
   State_0111111111111( ~lock11, L_pid, k, nonce, npr, otc, secretid,
                        tc, tuple
   )
   ]

  /* has exactly the trivial AC variant */

rule (modulo E) insert___Server___L_pid___secretid__k__tc_0111111111111:
   [
   State_0111111111111( ~lock11, L_pid, k, nonce, npr, otc, secretid,
                        tc, tuple
   )
   ]
  --[ Insert( <'Server', L_pid>, <secretid, k, tc> ) ]->
   [
   State_01111111111111( ~lock11, L_pid, k, nonce, npr, otc, secretid,
                         tc, tuple
   )
   ]

  /* has exactly the trivial AC variant */

rule (modulo E) unlock___Server___L_pid_01111111111111:
   [
   State_01111111111111( ~lock11, L_pid, k, nonce, npr, otc, secretid,
                         tc, tuple
   )
   ]
  --[ Unlock( ~lock11, <'Server', L_pid> ) ]->
   [
   State_011111111111111( ~lock11, L_pid, k, nonce, npr, otc,
                          secretid, tc, tuple
   )
   ]

  /* has exactly the trivial AC variant */

rule (modulo E) Zero01111111112:
   [
   State_01111111112( ~lock11, L_pid, k, nonce, npr, otc, secretid,
                      tc, tuple
   )
   ]
  -->
   [ ]

  /* has exactly the trivial AC variant */

rule (modulo E) Zero0111111112:
   [
   State_0111111112( ~lock11, L_pid, k, nonce, npr, otc, secretid, tc,
                     tuple
   )
   ]
  -->
   [ ]

  /* has exactly the trivial AC variant */

rule (modulo E) Zero01111112:
   [
   State_01111112( ~lock11, L_pid, k, nonce, npr, secretid, tc, tuple
   )
   ]
  -->
   [ ]

  /* has exactly the trivial AC variant */

rule (modulo E) Zero0111112:
   [
   State_0111112( ~lock11, L_pid, k, nonce, npr, secretid, tc, tuple )
   ]
  -->
   [ ]

  /* has exactly the trivial AC variant */

rule (modulo E) Rep02:
   [ !State_02( ) ] --> [ State_021( ) ]

  /* has exactly the trivial AC variant */

rule (modulo E) new_k021:
   [ State_021( ), Fr( k ) ] --> [ State_0211( k ) ]

  /* has exactly the trivial AC variant */

rule (modulo E) new_L_pid0211:
   [ State_0211( k ), Fr( L_pid ) ] --> [ State_02111( L_pid, k ) ]

  /* has exactly the trivial AC variant */

rule (modulo E) new_secretid02111:
   [ State_02111( L_pid, k ), Fr( secretid ) ]
  -->
   [ State_021111( L_pid, k, secretid ) ]

  /* has exactly the trivial AC variant */

rule (modulo E) insert___Server___L_pid___secretid__k___zero__021111:
   [ State_021111( L_pid, k, secretid ) ]
  --[ Insert( <'Server', L_pid>, <secretid, k, 'zero'> ) ]->
   [ State_0211111( L_pid, k, secretid ) ]

  /* has exactly the trivial AC variant */

rule (modulo E) insert___L_Yubikey___L_pid____zero_______one__0211111:
   [ State_0211111( L_pid, k, secretid ) ]
  --[ Insert( <'L_Yubikey', L_pid>, ('one'+'zero') ) ]->
   [ State_02111111( L_pid, k, secretid ) ]

  /* has exactly the trivial AC variant */

rule (modulo E) event_YubiInit_L_pid__secretid__k_02111111:
   [ State_02111111( L_pid, k, secretid ) ]
  --[ Event( ), YubiInit( L_pid, secretid, k ) ]->
   [ State_021111111( L_pid, k, secretid ) ]

  /* has exactly the trivial AC variant */

rule (modulo E) out_L_pid021111111:
   [ State_021111111( L_pid, k, secretid ) ]
  -->
   [ Out( L_pid ), !State_0211111111( L_pid, k, secretid ) ]

  /* has exactly the trivial AC variant */

rule (modulo E) Rep0211111111:
   [ !State_0211111111( L_pid, k, secretid ) ]
  -->
   [ State_02111111111( L_pid, k, secretid ) ]

  /* has exactly the trivial AC variant */

rule (modulo E) Par02111111111:
   [ State_02111111111( L_pid, k, secretid ) ]
  -->
   [
   State_021111111111( L_pid, k, secretid ),
   State_021111111112( L_pid, k, secretid )
   ]

  /* has exactly the trivial AC variant */

rule (modulo E) lock___Yubikey___L_pid_021111111111:
   [ State_021111111111( L_pid, k, secretid ), Fr( ~lock5 ) ]
  --[ Lock( ~lock5, <'Yubikey', L_pid> ) ]->
   [ State_0211111111111( ~lock5, L_pid, k, secretid ) ]

  /* has exactly the trivial AC variant */

rule (modulo E) lookup___L_Yubikey___L_pid__as_sc0211111111111:
   [ State_0211111111111( ~lock5, L_pid, k, secretid ) ]
  --[ IsIn( <'L_Yubikey', L_pid>, sc ) ]->
   [ State_02111111111111( ~lock5, L_pid, k, sc, secretid ) ]

  /* has exactly the trivial AC variant */

rule (modulo E) else__lookup___L_Yubikey___L_pid__as_sc0211111111111:
   [ State_0211111111111( ~lock5, L_pid, k, secretid ) ]
  --[ IsNotSet( <'L_Yubikey', L_pid> ) ]->
   [ State_02111111111112( ~lock5, L_pid, k, secretid ) ]

  /* has exactly the trivial AC variant */

rule (modulo E) in_sc02111111111111:
   [ State_02111111111111( ~lock5, L_pid, k, sc, secretid ), In( sc )
   ]
  -->
   [ State_021111111111111( ~lock5, L_pid, k, sc, secretid ) ]

  /* has exactly the trivial AC variant */

rule (modulo E) insert___L_Yubikey___L_pid___sc______one__021111111111111:
   [ State_021111111111111( ~lock5, L_pid, k, sc, secretid ) ]
  --[ Insert( <'L_Yubikey', L_pid>, ('one'+sc) ) ]->
   [ State_0211111111111111( ~lock5, L_pid, k, sc, secretid ) ]

  /* has exactly the trivial AC variant */

rule (modulo E) unlock___Yubikey___L_pid_0211111111111111:
   [ State_0211111111111111( ~lock5, L_pid, k, sc, secretid ) ]
  --[ Unlock( ~lock5, <'Yubikey', L_pid> ) ]->
   [ State_02111111111111111( ~lock5, L_pid, k, sc, secretid ) ]

  /* has exactly the trivial AC variant */

rule (modulo E) lock___Yubikey___L_pid_021111111112:
   [ State_021111111112( L_pid, k, secretid ), Fr( ~lock9 ) ]
  --[ Lock( ~lock9, <'Yubikey', L_pid> ) ]->
   [ State_0211111111121( ~lock9, L_pid, k, secretid ) ]

  /* has exactly the trivial AC variant */

rule (modulo E) lookup___L_Yubikey___L_pid__as_tc0211111111121:
   [ State_0211111111121( ~lock9, L_pid, k, secretid ) ]
  --[ IsIn( <'L_Yubikey', L_pid>, tc ) ]->
   [ State_02111111111211( ~lock9, L_pid, k, secretid, tc ) ]

  /* has exactly the trivial AC variant */

rule (modulo E) else__lookup___L_Yubikey___L_pid__as_tc0211111111121:
   [ State_0211111111121( ~lock9, L_pid, k, secretid ) ]
  --[ IsNotSet( <'L_Yubikey', L_pid> ) ]->
   [ State_02111111111212( ~lock9, L_pid, k, secretid ) ]

  /* has exactly the trivial AC variant */

rule (modulo E) in_tc02111111111211:
   [ State_02111111111211( ~lock9, L_pid, k, secretid, tc ), In( tc )
   ]
  -->
   [ State_021111111112111( ~lock9, L_pid, k, secretid, tc ) ]

  /* has exactly the trivial AC variant */

rule (modulo E) insert___L_Yubikey___L_pid___tc______one__021111111112111:
   [ State_021111111112111( ~lock9, L_pid, k, secretid, tc ) ]
  --[ Insert( <'L_Yubikey', L_pid>, ('one'+tc) ) ]->
   [ State_0211111111121111( ~lock9, L_pid, k, secretid, tc ) ]

  /* has exactly the trivial AC variant */

rule (modulo E) new_nonce0211111111121111:
   [
   State_0211111111121111( ~lock9, L_pid, k, secretid, tc ),
   Fr( nonce )
   ]
  -->
   [ State_02111111111211111( ~lock9, L_pid, k, nonce, secretid, tc )
   ]

  /* has exactly the trivial AC variant */

rule (modulo E) new_npr02111111111211111:
   [
   State_02111111111211111( ~lock9, L_pid, k, nonce, secretid, tc ),
   Fr( npr )
   ]
  -->
   [
   State_021111111112111111( ~lock9, L_pid, k, nonce, npr, secretid,
                             tc
   )
   ]

  /* has exactly the trivial AC variant */

rule (modulo E) event_YubiPress_L_pid__secretid__k__tc_021111111112111111:
   [
   State_021111111112111111( ~lock9, L_pid, k, nonce, npr, secretid,
                             tc
   )
   ]
  --[ Event( ), YubiPress( L_pid, secretid, k, tc ) ]->
   [
   State_0211111111121111111( ~lock9, L_pid, k, nonce, npr, secretid,
                              tc
   )
   ]

  /* has exactly the trivial AC variant */

rule (modulo E) out__L_pid__nonce__senc__secretid__tc__npr___k__0211111111121111111:
   [
   State_0211111111121111111( ~lock9, L_pid, k, nonce, npr, secretid,
                              tc
   )
   ]
  -->
   [
   Out( <L_pid, nonce, senc(<secretid, tc, npr>, k)> ),
   State_02111111111211111111( ~lock9, L_pid, k, nonce, npr, secretid,
                               tc
   )
   ]

  /* has exactly the trivial AC variant */

rule (modulo E) unlock___Yubikey___L_pid_02111111111211111111:
   [
   State_02111111111211111111( ~lock9, L_pid, k, nonce, npr, secretid,
                               tc
   )
   ]
  --[ Unlock( ~lock9, <'Yubikey', L_pid> ) ]->
   [
   State_021111111112111111111( ~lock9, L_pid, k, nonce, npr,
                                secretid, tc
   )
   ]

  /* has exactly the trivial AC variant */

restriction single_session:
  "∀ #i #j. ((Init( ) @ #i) ∧ (Init( ) @ #j)) ⇒ (#i = #j)"
  // safety formula

restriction set_in:
  "∀ x y #t3.
    (IsIn( x, y ) @ #t3) ⇒
    (∃ #t2.
      (((Insert( x, y ) @ #t2) ∧ (#t2 < #t3)) ∧
       (∀ #t1. (Delete( x ) @ #t1) ⇒ ((#t1 < #t2) ∨ (#t3 < #t1)))) ∧
      (∀ #t1 yp.
        (Insert( x, yp ) @ #t1) ⇒
        (((#t1 < #t2) ∨ (#t1 = #t2)) ∨ (#t3 < #t1))))"

restriction set_notin:
  "∀ x #t3.
    (IsNotSet( x ) @ #t3) ⇒
    ((∀ #t1 y. (Insert( x, y ) @ #t1) ⇒ (#t3 < #t1)) ∨
     (∃ #t1.
       ((Delete( x ) @ #t1) ∧ (#t1 < #t3)) ∧
       (∀ #t2 y. ((Insert( x, y ) @ #t2) ∧ (#t2 < #t3)) ⇒ (#t2 < #t1))))"

restriction predicate_not_eq:
  "∀ #i a b. (Pred_not_eq( a, b ) @ #i) ⇒ (¬(a = b))"
  // safety formula

restriction predicate_eq:
  "∀ #i a b. (Pred_eq( a, b ) @ #i) ⇒ (a = b)"
  // safety formula

restriction immeadiate_in:
  "∀ x #t3.
    (ChannelInEvent( x ) @ #t3) ⇒
    (∃ #t2.
      (((K( x ) @ #t2) ∧ (#t2 < #t3)) ∧
       (∀ #t0. (Event( ) @ #t0) ⇒ ((#t0 < #t2) ∨ (#t3 < #t0)))) ∧
      (∀ #t0 xp.
        (K( xp ) @ #t0) ⇒ (((#t0 < #t2) ∨ (#t0 = #t2)) ∨ (#t3 < #t0))))"

restriction locking:
  "∀ l x lp #t1 #t3.
    ((Lock( l, x ) @ #t1) ∧ (Lock( lp, x ) @ #t3)) ⇒
    ((((#t1 < #t3) ∧
       (∃ #t2.
         (((((Unlock( l, x ) @ #t2) ∧ (#t1 < #t2)) ∧ (#t2 < #t3)) ∧
           (∀ #t0. (Unlock( l, x ) @ #t0) ⇒ (#t0 = #t2))) ∧
          (∀ lp.1 #t0.
            (Lock( lp.1, x ) @ #t0) ⇒
            (((#t0 < #t1) ∨ (#t0 = #t1)) ∨ (#t2 < #t0)))) ∧
         (∀ lp.1 #t0.
           (Unlock( lp.1, x ) @ #t0) ⇒
           (((#t0 < #t1) ∨ (#t2 < #t0)) ∨ (#t2 = #t0))))) ∨
      (#t3 < #t1)) ∨
     (#t1 = #t3))"

restriction predicate1:
  "∀ #i a b. (Pred_not_smaller( a, b ) @ #i) ⇒ (¬(∃ z. (a+z) = b))"
  // safety formula

restriction predicate0:
  "∀ #i a b. (Pred_smaller( a, b ) @ #i) ⇒ (∃ z. (a+z) = b)"

lemma init_server [sources]:
  all-traces
  "∀ pid sid k tuple otc tc #i.
    (InitStuff( pid, sid, k, tuple, otc, tc ) @ #i) ⇒
    ((tuple = <sid, k, otc>) ∧
     (∃ #j. (YubiInit( pid, sid, k ) @ #j) ∧ (#j < #i)))"
/*
guarded formula characterizing all counter-examples:
"∃ pid sid k tuple otc tc #i.
  (InitStuff( pid, sid, k, tuple, otc, tc ) @ #i)
 ∧
  (¬(tuple = <sid, k, otc>)) ∨
  (∀ #j. (YubiInit( pid, sid, k ) @ #j) ⇒ ¬(#j < #i))"
*/
by sorry

lemma init_server_secrecy [use_induction, reuse]:
  all-traces
  "∀ pid sid k tuple otc tc #i.
    (InitStuff( pid, sid, k, tuple, otc, tc ) @ #i) ⇒
    (¬(∃ #j. !KU( k ) @ #j))"
/*
guarded formula characterizing all counter-examples:
"∃ pid sid k tuple otc tc #i.
  (InitStuff( pid, sid, k, tuple, otc, tc ) @ #i)
 ∧
  ∃ #j. (!KU( k ) @ #j)"
*/
by sorry

lemma init_yubikey [sources]:
  all-traces
  "∀ pid sid k tc #i.
    (YubiPress( pid, sid, k, tc ) @ #i) ⇒
    (∃ #j. (YubiInit( pid, sid, k ) @ #j) ∧ (#j < #i))"
/*
guarded formula characterizing all counter-examples:
"∃ pid sid k tc #i.
  (YubiPress( pid, sid, k, tc ) @ #i)
 ∧
  ∀ #j. (YubiInit( pid, sid, k ) @ #j) ⇒ ¬(#j < #i)"
*/
by sorry

lemma slightly_weaker_invariant [reuse, use_induction]:
  all-traces
  "∀ pid k tc1 tc2 #t1 #t2.
    ((Login( pid, k, tc1 ) @ #t1) ∧ (Login( pid, k, tc2 ) @ #t2)) ⇒
    ((((#t1 < #t2) ∧ (∃ z. (tc1+z) = tc2)) ∨ (#t2 < #t1)) ∨
     (#t1 = #t2))"
/*
guarded formula characterizing all counter-examples:
"∃ pid k tc1 tc2 #t1 #t2.
  (Login( pid, k, tc1 ) @ #t1) ∧ (Login( pid, k, tc2 ) @ #t2)
 ∧
  ((¬(#t1 < #t2)) ∨ (∀ z. ((tc1+z) = tc2) ⇒ ⊥)) ∧
  (¬(#t2 < #t1)) ∧
  (¬(#t1 = #t2))"
*/
induction
  case empty_trace
  by contradiction // from formulas
next
  case non_empty_trace
  simplify
  solve( (¬(#t1 < #t2))  ∥ (∀ z. ((tc1+z) = tc2) ⇒ ⊥) )
    case case_1
    solve( (#t2 = #t1)  ∥ (#t1 < #t2) )
      case case_1
      by contradiction // from formulas
    next
      case case_2
      by contradiction // from formulas
    qed
  next
    case case_2
    solve( (#t2 = #t1)  ∥ (#t1 < #t2) )
      case case_1
      by contradiction // from formulas
    next
      case case_2
      solve( (∀ pid k tc1 tc2 #t1 #t2.
               (Login( pid, k, tc1 ) @ #t1) ∧ (Login( pid, k, tc2 ) @ #t2)
              ⇒
               (last(#t2)) ∨
               (last(#t1)) ∨
               ((#t1 < #t2) ∧ (∃ z. ((tc1+z) = tc2))) ∨
               (#t2 < #t1) ∨
               (#t1 = #t2))  ∥
             (∃ x y #t3.
               (IsIn( x, y ) @ #t3)
              ∧
               (¬(last(#t3))) ∧
               (∀ #t2.
                 (Insert( x, y ) @ #t2)
                ⇒
                 (last(#t2)) ∨
                 (#t2 = #t3) ∨
                 (#t3 < #t2) ∨
                 (∃ #t1.
                   (Delete( x ) @ #t1)
                  ∧
                   (¬(last(#t1))) ∧
                   ((#t1 = #t2) ∨ (#t2 < #t1)) ∧
                   ((#t3 = #t1) ∨ (#t1 < #t3))) ∨
                 (∃ #t1 yp.
                   (Insert( x, yp ) @ #t1)
                  ∧
                   (¬(last(#t1))) ∧
                   ((#t1 = #t2) ∨ (#t2 < #t1)) ∧
                   (¬(#t1 = #t2)) ∧
                   ((#t3 = #t1) ∨ (#t1 < #t3)))))  ∥
             (∃ x #t3.
               (IsNotSet( x ) @ #t3)
              ∧
               (¬(last(#t3))) ∧
               (∃ #t1 y.
                 (Insert( x, y ) @ #t1)
                ∧
                 (¬(last(#t1))) ∧ ((#t3 = #t1) ∨ (#t1 < #t3))) ∧
               (∀ #t1.
                 (Delete( x ) @ #t1)
                ⇒
                 (last(#t1)) ∨
                 (#t1 = #t3) ∨
                 (#t3 < #t1) ∨
                 (∃ #t2 y.
                   (Insert( x, y ) @ #t2)
                  ∧
                   (¬(last(#t2))) ∧ (#t2 < #t3) ∧ ((#t2 = #t1) ∨ (#t1 < #t2)))))  ∥
             (∃ x #t3.
               (ChannelInEvent( x ) @ #t3)
              ∧
               (¬(last(#t3))) ∧
               (∀ #t2.
                 (K( x ) @ #t2)
                ⇒
                 (last(#t2)) ∨
                 (#t2 = #t3) ∨
                 (#t3 < #t2) ∨
                 (∃ #t0.
                   (Event( ) @ #t0)
                  ∧
                   (¬(last(#t0))) ∧
                   ((#t0 = #t2) ∨ (#t2 < #t0)) ∧
                   ((#t3 = #t0) ∨ (#t0 < #t3))) ∨
                 (∃ #t0 xp.
                   (K( xp ) @ #t0)
                  ∧
                   (¬(last(#t0))) ∧
                   ((#t0 = #t2) ∨ (#t2 < #t0)) ∧
                   (¬(#t0 = #t2)) ∧
                   ((#t3 = #t0) ∨ (#t0 < #t3)))))  ∥
             (∃ l x lp #t1 #t3.
               (Lock( l, x ) @ #t1) ∧ (Lock( lp, x ) @ #t3)
              ∧
               (¬(last(#t3))) ∧
               (¬(last(#t1))) ∧
               ((#t1 = #t3) ∨
                (#t3 < #t1) ∨
                (∀ #t2.
                  (Unlock( l, x ) @ #t2)
                 ⇒
                  (last(#t2)) ∨
                  (#t1 = #t2) ∨
                  (#t2 < #t1) ∨
                  (#t2 = #t3) ∨
                  (#t3 < #t2) ∨
                  (∃ #t0. (Unlock( l, x ) @ #t0) ∧ (¬(last(#t0))) ∧ (¬(#t0 = #t2))) ∨
                  (∃ lp.1 #t0.
                    (Lock( lp.1, x ) @ #t0)
                   ∧
                    (¬(last(#t0))) ∧
                    ((#t0 = #t1) ∨ (#t1 < #t0)) ∧
                    (¬(#t0 = #t1)) ∧
                    ((#t2 = #t0) ∨ (#t0 < #t2))) ∨
                  (∃ lp.1 #t0.
                    (Unlock( lp.1, x ) @ #t0)
                   ∧
                    (¬(last(#t0))) ∧
                    ((#t0 = #t1) ∨ (#t1 < #t0)) ∧
                    ((#t2 = #t0) ∨ (#t0 < #t2)) ∧
                    (¬(#t2 = #t0))))) ∧
               ((#t3 = #t1) ∨ (#t1 < #t3)) ∧
               (¬(#t1 = #t3)))  ∥
             (∃ #i a b.
               (Pred_smaller( a, b ) @ #i)
              ∧
               (¬(last(#i))) ∧ (∀ z. ((a+z) = b) ⇒ ⊥)) )
        case case_1
        solve( (last(#t2))  ∥ (∃ z. ((tc1+z) = tc2)) )
          case case_1
          solve( State_011111111111( ~lock11, pid, k, nonce, npr, otc,
                                     secretid, tc1, tuple
                 ) ▶₀ #t1 )
            case event_InitStuff_L_pid__secretid__k__tuple__otc__tc_01111111111
            solve( State_011111111111( ~lock11.1, ~n, ~n.1, nonce.1, npr.1,
                                       otc.1, secretid, tc2, tuple
                   ) ▶₀ #t2 )
              case event_InitStuff_L_pid__secretid__k__tuple__otc__tc_01111111111
              solve( ((#vr.7 < #vr.25) ∧
                      (∃ #t2.
                        (Unlock( ~lock11, <'Server', ~n> ) @ #t2)
                       ∧
                        (#vr.7 < #t2) ∧
                        (#t2 < #vr.25) ∧
                        (∀ #t0. (Unlock( ~lock11, <'Server', ~n> ) @ #t0) ⇒ #t0 = #t2) ∧
                        (∀ lp #t0.
                          (Lock( lp, <'Server', ~n> ) @ #t0)
                         ⇒
                          (#t0 < #vr.7) ∨ (#t0 = #vr.7) ∨ (#t2 < #t0)) ∧
                        (∀ lp #t0.
                          (Unlock( lp, <'Server', ~n> ) @ #t0)
                         ⇒
                          (#t0 < #vr.7) ∨ (#t2 < #t0) ∨ (#t2 = #t0))))  ∥
                     (#vr.25 < #vr.7)  ∥ (#vr.7 = #vr.25) )
                case case_1
                solve( Insert( <'Server', ~n>, <~n.2, ~n.1, otc.1> ) @ #t2.2 )
                  case insert___Server___L_pid___secretid__k___zero__021111
                  by sorry
                next
                  case insert___Server___L_pid___secretid__k__tc_0111111111111
                  solve( State_0111111111111( ~lock11.2, ~n, ~n.1, nonce.2, npr.2,
                                              otc.2, ~n.2, otc.1, tuple
                         ) ▶₀ #t2.1 )
                    case event_Login_L_pid__k__tc_011111111111
                    solve( ((#vr.7 < #vr.36) ∧
                            (∃ #t2.
                              (Unlock( ~lock11, <'Server', ~n> ) @ #t2)
                             ∧
                              (#vr.7 < #t2) ∧
                              (#t2 < #vr.36) ∧
                              (∀ #t0. (Unlock( ~lock11, <'Server', ~n> ) @ #t0) ⇒ #t0 = #t2) ∧
                              (∀ lp #t0.
                                (Lock( lp, <'Server', ~n> ) @ #t0)
                               ⇒
                                (#t0 < #vr.7) ∨ (#t0 = #vr.7) ∨ (#t2 < #t0)) ∧
                              (∀ lp #t0.
                                (Unlock( lp, <'Server', ~n> ) @ #t0)
                               ⇒
                                (#t0 < #vr.7) ∨ (#t2 < #t0) ∨ (#t2 = #t0))))  ∥
                           (#vr.36 < #vr.7)  ∥ (#vr.7 = #vr.36) )
                      case case_1
                      solve( Unlock( ~lock11, <'Server', ~n> ) @ #t2.3 )
                        case unlock___Server___L_pid_01111111111111
                        solve( State_01111111111111( ~lock11, ~n, k, nonce.3, npr.3, otc.2,
                                                     secretid, tc, tuple
                               ) ▶₀ #t2.2 )
                          case insert___Server___L_pid___secretid__k__tc_0111111111111_case_01
                          by contradiction // from formulas
                        next
                          case insert___Server___L_pid___secretid__k__tc_0111111111111_case_02
                          by contradiction // from formulas
                        next
                          case insert___Server___L_pid___secretid__k__tc_0111111111111_case_03
                          by contradiction // from formulas
                        next
                          case insert___Server___L_pid___secretid__k__tc_0111111111111_case_04
                          by contradiction // from formulas
                        next
                          case insert___Server___L_pid___secretid__k__tc_0111111111111_case_05
                          by contradiction // from formulas
                        next
                          case insert___Server___L_pid___secretid__k__tc_0111111111111_case_06
                          by contradiction // from formulas
                        next
                          case insert___Server___L_pid___secretid__k__tc_0111111111111_case_07
                          by contradiction // from formulas
                        next
                          case insert___Server___L_pid___secretid__k__tc_0111111111111_case_08
                          by contradiction // from formulas
                        next
                          case insert___Server___L_pid___secretid__k__tc_0111111111111_case_09
                          by contradiction // from formulas
                        next
                          case insert___Server___L_pid___secretid__k__tc_0111111111111_case_10
                          by contradiction // from formulas
                        next
                          case insert___Server___L_pid___secretid__k__tc_0111111111111_case_11
                          by contradiction // from formulas
                        next
                          case insert___Server___L_pid___secretid__k__tc_0111111111111_case_12
                          by contradiction // from formulas
                        next
                          case insert___Server___L_pid___secretid__k__tc_0111111111111_case_13
                          by contradiction // from formulas
                        next
                          case insert___Server___L_pid___secretid__k__tc_0111111111111_case_14
                          by contradiction // from formulas
                        next
                          case insert___Server___L_pid___secretid__k__tc_0111111111111_case_15
                          by contradiction // from formulas
                        next
                          case insert___Server___L_pid___secretid__k__tc_0111111111111_case_16
                          by contradiction // from formulas
                        next
                          case insert___Server___L_pid___secretid__k__tc_0111111111111_case_17
                          by contradiction // from formulas
                        next
                          case insert___Server___L_pid___secretid__k__tc_0111111111111_case_18
                          by contradiction // from formulas
                        next
                          case insert___Server___L_pid___secretid__k__tc_0111111111111_case_19
                          by contradiction // from formulas
                        next
                          case insert___Server___L_pid___secretid__k__tc_0111111111111_case_20
                          by contradiction // from formulas
                        next
                          case insert___Server___L_pid___secretid__k__tc_0111111111111_case_21
                          by contradiction // from formulas
                        next
                          case insert___Server___L_pid___secretid__k__tc_0111111111111_case_22
                          by contradiction // from formulas
                        next
                          case insert___Server___L_pid___secretid__k__tc_0111111111111_case_23
                          by contradiction // from formulas
                        next
                          case insert___Server___L_pid___secretid__k__tc_0111111111111_case_24
                          by contradiction // from formulas
                        next
                          case insert___Server___L_pid___secretid__k__tc_0111111111111_case_25
                          by contradiction // from formulas
                        qed
                      qed
                    next
                      case case_2
                      solve( Unlock( ~lock11, <'Server', ~n> ) @ #t2.3 )
                        case unlock___Server___L_pid_01111111111111
                        solve( State_01111111111111( ~lock11, ~n, k, nonce.3, npr.3, otc.2,
                                                     secretid, tc, tuple
                               ) ▶₀ #t2.2 )
                          case insert___Server___L_pid___secretid__k__tc_0111111111111
                          solve( Unlock( ~lock11.2, <'Server', ~n> ) @ #t2.5 )
                            case unlock___Server___L_pid_01111111111111
                            solve( State_01111111111111( ~lock11.2, ~n, k, nonce.3, npr.3,
                                                         otc.2, secretid, tc, tuple
                                   ) ▶₀ #t2.3 )
                              case insert___Server___L_pid___secretid__k__tc_0111111111111_case_01
                              by contradiction // cyclic
                            next
                              case insert___Server___L_pid___secretid__k__tc_0111111111111_case_02
                              by contradiction // cyclic
                            next
                              case insert___Server___L_pid___secretid__k__tc_0111111111111_case_03
                              by contradiction // cyclic
                            next
                              case insert___Server___L_pid___secretid__k__tc_0111111111111_case_04
                              by contradiction // cyclic
                            next
                              case insert___Server___L_pid___secretid__k__tc_0111111111111_case_05
                              by contradiction // cyclic
                            next
                              case insert___Server___L_pid___secretid__k__tc_0111111111111_case_06
                              by contradiction // cyclic
                            next
                              case insert___Server___L_pid___secretid__k__tc_0111111111111_case_07
                              by contradiction // cyclic
                            next
                              case insert___Server___L_pid___secretid__k__tc_0111111111111_case_08
                              by contradiction // cyclic
                            next
                              case insert___Server___L_pid___secretid__k__tc_0111111111111_case_09
                              by contradiction // cyclic
                            next
                              case insert___Server___L_pid___secretid__k__tc_0111111111111_case_10
                              by contradiction // cyclic
                            next
                              case insert___Server___L_pid___secretid__k__tc_0111111111111_case_11
                              by contradiction // cyclic
                            next
                              case insert___Server___L_pid___secretid__k__tc_0111111111111_case_12
                              by contradiction // cyclic
                            next
                              case insert___Server___L_pid___secretid__k__tc_0111111111111_case_13
                              by contradiction // cyclic
                            next
                              case insert___Server___L_pid___secretid__k__tc_0111111111111_case_14
                              by contradiction // cyclic
                            next
                              case insert___Server___L_pid___secretid__k__tc_0111111111111_case_15
                              by contradiction // cyclic
                            next
                              case insert___Server___L_pid___secretid__k__tc_0111111111111_case_16
                              by contradiction // cyclic
                            next
                              case insert___Server___L_pid___secretid__k__tc_0111111111111_case_17
                              by contradiction // cyclic
                            next
                              case insert___Server___L_pid___secretid__k__tc_0111111111111_case_18
                              by contradiction // cyclic
                            next
                              case insert___Server___L_pid___secretid__k__tc_0111111111111_case_19
                              by contradiction // cyclic
                            next
                              case insert___Server___L_pid___secretid__k__tc_0111111111111_case_20
                              by contradiction // cyclic
                            next
                              case insert___Server___L_pid___secretid__k__tc_0111111111111_case_21
                              by contradiction // cyclic
                            next
                              case insert___Server___L_pid___secretid__k__tc_0111111111111_case_22
                              by contradiction // cyclic
                            next
                              case insert___Server___L_pid___secretid__k__tc_0111111111111_case_23
                              by contradiction // cyclic
                            next
                              case insert___Server___L_pid___secretid__k__tc_0111111111111_case_24
                              by contradiction // cyclic
                            next
                              case insert___Server___L_pid___secretid__k__tc_0111111111111_case_25
                              by contradiction // cyclic
                            qed
                          qed
                        qed
                      qed
                    next
                      case case_3
                      by contradiction // from formulas
                    qed
                  qed
                qed
              next
                case case_2
                by sorry
              next
                case case_3
                by contradiction // cyclic
              qed
            qed
          qed
        next
          case case_2
          by contradiction // from formulas
        qed
      next
        case case_2
        by sorry
      next
        case case_3
        by sorry
      next
        case case_4
        by sorry
      next
        case case_5
        by sorry
      next
        case case_6
        by contradiction // from formulas
      qed
    qed
  qed
qed

lemma one_count_foreach_login [reuse, use_induction]:
  all-traces
  "∀ pid k x #t2.
    (Login( pid, k, x ) @ #t2) ⇒
    (∃ #t1 sid. (YubiPress( pid, sid, k, x ) @ #t1) ∧ (#t1 < #t2))"
/*
guarded formula characterizing all counter-examples:
"∃ pid k x #t2.
  (Login( pid, k, x ) @ #t2)
 ∧
  ∀ #t1 sid. (YubiPress( pid, sid, k, x ) @ #t1) ⇒ ¬(#t1 < #t2)"
*/
by sorry

lemma no_replay [reuse]:
  all-traces
  "¬(∃ #i #j pid k x.
      ((Login( pid, k, x ) @ #i) ∧ (Login( pid, k, x ) @ #j)) ∧
      (¬(#i = #j)))"
/*
guarded formula characterizing all counter-examples:
"∃ #i #j pid k x.
  (Login( pid, k, x ) @ #i) ∧ (Login( pid, k, x ) @ #j) ∧ ¬(#i = #j)"
*/
by sorry

lemma injective_correspondance [reuse, use_induction]:
  all-traces
  "∀ pid k x #t2.
    (Login( pid, k, x ) @ #t2) ⇒
    ((∃ #t1 sid. (YubiPress( pid, sid, k, x ) @ #t1) ∧ (#t1 < #t2)) ∧
     (∀ #t3. (Login( pid, k, x ) @ #t3) ⇒ (#t3 = #t2)))"
/*
guarded formula characterizing all counter-examples:
"∃ pid k x #t2.
  (Login( pid, k, x ) @ #t2)
 ∧
  (∀ #t1 sid. (YubiPress( pid, sid, k, x ) @ #t1) ⇒ ¬(#t1 < #t2)) ∨
  (∃ #t3. (Login( pid, k, x ) @ #t3) ∧ ¬(#t3 = #t2))"
*/
by sorry

lemma Login_invalidates_smaller_counters:
  all-traces
  "∀ pid k tc1 tc2 #t1 #t2.
    (((Login( pid, k, tc1 ) @ #t1) ∧ (Login( pid, k, tc2 ) @ #t2)) ∧
     (∃ z. (tc1+z) = tc2)) ⇒
    (#t1 < #t2)"
/*
guarded formula characterizing all counter-examples:
"∃ pid k tc1 tc2 #t1 #t2.
  (Login( pid, k, tc1 ) @ #t1) ∧ (Login( pid, k, tc2 ) @ #t2)
 ∧
  (∃ z. ((tc1+z) = tc2)) ∧ (¬(#t1 < #t2))"
*/
by sorry

/*
WARNING: the following wellformedness checks failed!

unbound:
  rule `lookup___Server___L_pid__as_tuple01111' has unbound variables: 
    tuple
  
  rule `lookup___L_Yubikey___L_pid__as_sc0211111111111' has unbound variables: 
    sc
  
  rule `lookup___L_Yubikey___L_pid__as_tc0211111111121' has unbound variables: 
    tc
*/

end