theory OTYT06_UK1_proof begin

// Function signature and definition of the equational theory E

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



rule (modulo E) SetupLearning:
   [ Fr( ~k1 ), Fr( ~k2 ) ]
  --[ Setup( ~k1 ), Setup( ~k2 ), OnlyOnce( 'setupLearning' ) ]->
   [ Tag( ~k1, ~k1 ), Tag( ~k2, ~k2 ), SetupKeys( ~k1, ~k2 ) ]

rule (modulo E) SetupGuessing:
   [ SetupKeys( ~k1, ~k2 ), Tag( ~k1, x1 ), Tag( ~k2, x2 ) ]
  --[ OnlyOnce( 'setupGuessing' ) ]->
   [ Tag( diff(~k1, ~k2), diff(x1, x2) ) ]

rule (modulo E) tag1:
   [ In( r1 ), Tag( ~k, x ) ]
  --[
  Response( ~k, 'Tag' ), Challenge( x, 'Tag' ), Tag( ~k, x ),
  Running( ~k, 'Tag', x ), OnlyTwice( 'tag1' )
  ]->
   [ Out( h((r1⊕x)) ), Tag( ~k, x ), TagRunning( ~k, x ) ]

rule (modulo E) tag2:
   [ Fr( ~k2 ), In( newkey ), TagRunning( ~k, x ) ]
  --[
  Update( x, (newkey⊕x), 'Tag' ), Alive( ~k, 'Reader' ),
  OnlyTwice( 'tag2' )
  ]->
   [ Tag( ~k, (newkey⊕x) ) ]

restriction unique [right]:
  "∀ x #i #j.
    ((OnlyOnce( x ) @ #i) ∧ (OnlyOnce( x ) @ #j)) ⇒ (#i = #j)"
  // safety formula

restriction unique [left]:
  "∀ x #i #j.
    ((OnlyOnce( x ) @ #i) ∧ (OnlyOnce( x ) @ #j)) ⇒ (#i = #j)"
  // safety formula

restriction uniqueTwice [right]:
  "∀ x #i #j #k.
    (((OnlyTwice( x ) @ #i) ∧ (OnlyTwice( x ) @ #j)) ∧
     (OnlyTwice( x ) @ #k)) ⇒
    (((#i = #j) ∨ (#i = #k)) ∨ (#j = #k))"
  // safety formula

restriction uniqueTwice [left]:
  "∀ x #i #j #k.
    (((OnlyTwice( x ) @ #i) ∧ (OnlyTwice( x ) @ #j)) ∧
     (OnlyTwice( x ) @ #k)) ⇒
    (((#i = #j) ∨ (#i = #k)) ∨ (#j = #k))"
  // safety formula

lemma tag_start [right, reuse, use_induction]:
  all-traces
  "∀ x y #k.
    (Tag( x, y ) @ #k) ⇒ (∃ #i. (Setup( x ) @ #i) ∧ (#i < #k))"
/*
guarded formula characterizing all counter-examples:
"∃ x y #k.
  (Tag( x, y ) @ #k) ∧ ∀ #i. (Setup( x ) @ #i) ⇒ ¬(#i < #k)"
*/
induction
  case empty_trace
  by contradiction /* from formulas */
next
  case non_empty_trace
  simplify
  solve( (last(#k))  ∥
         (∃ #i. (Setup( ~k.1 ) @ #i) ∧ (¬(last(#i))) ∧ (#i < #k)) )
    case case_1
    solve( Tag( ~k.1, y ) ▶₁ #k )
      case SetupGuessing
      by contradiction /* from formulas */
    next
      case SetupLearning_case_1
      by contradiction /* from formulas */
    next
      case SetupLearning_case_2
      by contradiction /* from formulas */
    next
      case tag1
      by contradiction /* from formulas */
    next
      case tag2
      by contradiction /* from formulas */
    qed
  next
    case case_2
    by contradiction /* from formulas */
  qed
qed

lemma tag_start [left, reuse, use_induction]:
  all-traces
  "∀ x y #k.
    (Tag( x, y ) @ #k) ⇒ (∃ #i. (Setup( x ) @ #i) ∧ (#i < #k))"
/*
guarded formula characterizing all counter-examples:
"∃ x y #k.
  (Tag( x, y ) @ #k) ∧ ∀ #i. (Setup( x ) @ #i) ⇒ ¬(#i < #k)"
*/
induction
  case empty_trace
  by contradiction /* from formulas */
next
  case non_empty_trace
  simplify
  solve( (last(#k))  ∥
         (∃ #i. (Setup( ~k.1 ) @ #i) ∧ (¬(last(#i))) ∧ (#i < #k)) )
    case case_1
    solve( Tag( ~k.1, y ) ▶₁ #k )
      case SetupGuessing
      by contradiction /* from formulas */
    next
      case SetupLearning_case_1
      by contradiction /* from formulas */
    next
      case SetupLearning_case_2
      by contradiction /* from formulas */
    next
      case tag1
      by contradiction /* from formulas */
    next
      case tag2
      by contradiction /* from formulas */
    qed
  next
    case case_2
    by contradiction /* from formulas */
  qed
qed

/* All well-formedness checks were successful. */

diffLemma Observational_equivalence:
rule-equivalence
  case Rule_Destrd_0_fst
  by sorry
next
  case Rule_Destrd_0_snd
  by sorry
next
  case Rule_Destrd_union
  by sorry
next
  case Rule_Destrd_xor
  by sorry
next
  case Rule_Equality
  backward-search
    case LHS
    step( simplify )
    step( solve( !KD( x ) ▶₁ #i ) )
      case tag1
      step( solve( (#vl, 0) ~~> (#i, 1) ) )
        case h
        step( solve( Tag( ~k, x ) ▶₁ #vr ) )
          case SetupGuessing
          step( solve( Tag( ~k, x ) ▶₁ #vr.1 ) )
            case tag1
            step( solve( Tag( ~k2, x2 ) ▶₂ #vr.1 ) )
              case SetupLearning
              step( solve( Tag( ~k, x ) ▶₁ #vr.3 ) )
                case SetupLearning
                step( solve( !KU( h(z) ) @ #vk ) )
                  case tag1
                  step( solve( (#vr = #vr.4)  ∥ (#vr.3 = #vr.4) ) )
                    case case_2
                    step( solve( splitEqs(0) ) )
                      case split_case_2
                      by ATTACK // trace found
                    qed
                  qed
                qed
              qed
            qed
          qed
        qed
      qed
    qed
  next
    case RHS
    step( simplify )
    by sorry
  qed
next
  case Rule_Send
  by sorry
next
  case Rule_SetupGuessing
  by sorry
next
  case Rule_SetupLearning
  by sorry
next
  case Rule_tag1
  by sorry
next
  case Rule_tag2
  by sorry
qed

end