theory nsl
imports
  "../ESPLogic"
begin

role I
where "I =
  [ Send ''1'' ( Enc {| sLN ''ni'', sLAV ''I'' |} ( sPK ''R'' ) )
  , Recv ''2'' ( Enc {| sLN ''ni'', sLNV ''nr'', sLAV ''R'' |}
                     ( sPK ''I'' )
               )
  , Send ''3'' ( Enc ( sLNV ''nr'' ) ( sPK ''R'' ) )
  ]"

role R
where "R =
  [ Recv ''1'' ( Enc {| sLNV ''ni'', sLAV ''I'' |} ( sPK ''R'' ) )
  , Send ''2'' ( Enc {| sLNV ''ni'', sLN ''nr'', sLAV ''R'' |}
                     ( sPK ''I'' )
               )
  , Recv ''3'' ( Enc ( sLN ''nr'' ) ( sPK ''R'' ) )
  ]"

protocol nsl3
where "nsl3 = { I, R }"

locale atomic_nsl3_state = atomic_state nsl3
locale nsl3_state = reachable_state nsl3

lemma (in atomic_nsl3_state) I_sk_I_secrecy:
  assumes asms:
    "roleMap r tid0 = Some I"
    "s(|AV ''I'' tid0|) ~: Compromised"
    "SK ( s(|AV ''I'' tid0|) ) : knows t"
  shows "False"
using asms prefix_close
proof(sources " SK ( s(|AV ''I'' tid0|) ) ")
qed ((clarsimp, order?)+)?

lemma (in atomic_nsl3_state) I_sk_R_secrecy:
  assumes asms:
    "roleMap r tid0 = Some I"
    "s(|AV ''R'' tid0|) ~: Compromised"
    "SK ( s(|AV ''R'' tid0|) ) : knows t"
  shows "False"
using asms prefix_close
proof(sources " SK ( s(|AV ''R'' tid0|) ) ")
qed ((clarsimp, order?)+)?

lemma (in atomic_nsl3_state) I_ni_secrecy:
  assumes asms:
    "roleMap r tid0 = Some I"
    "s(|AV ''I'' tid0|) ~: Compromised"
    "s(|AV ''R'' tid0|) ~: Compromised"
    "LN ''ni'' tid0 : knows t"
  shows "False"
using asms prefix_close
proof(sources " LN ''ni'' tid0 ")
  case (I_1_ni tid2) thus ?thesis
  by (fastsimp dest: I_sk_R_secrecy intro: event_predOrdI)
next
  case (I_3_nr tid2) thus ?thesis
  proof(sources "
      Enc {| LN ''ni'' tid2, LN ''ni'' tid0, s(|AV ''R'' tid2|) |}
          ( PK ( s(|AV ''I'' tid2|) ) ) ")
  qed ((clarsimp, order?)+)?
next
  case (R_2_ni tid2) thus ?thesis
  proof(sources "
      Enc {| LN ''ni'' tid0, s(|AV ''I'' tid2|) |}
          ( PK ( s(|AV ''R'' tid2|) ) ) ")
    case (I_1_enc tid4) thus ?thesis
    by (fastsimp dest: I_sk_I_secrecy intro: event_predOrdI)
  qed ((clarsimp, order?)+)?
qed

lemma (in atomic_nsl3_state) I_nr_secrecy:
  assumes asms:
    "roleMap r tid0 = Some I"
    "s(|AV ''I'' tid0|) ~: Compromised"
    "s(|AV ''R'' tid0|) ~: Compromised"
    "(tid0, I_2) : steps t"
    "s(|NV ''nr'' tid0|) : knows t"
  shows "False"
using asms prefix_close
proof(sources "
    Enc {| LN ''ni'' tid0, s(|NV ''nr'' tid0|), s(|AV ''R'' tid0|) |}
        ( PK ( s(|AV ''I'' tid0|) ) ) ")
  case fake thus ?thesis
  by (fastsimp dest: I_ni_secrecy intro: event_predOrdI)
next
  case (I_3_enc tid2) thus ?thesis
  by (fastsimp dest: I_ni_secrecy intro: event_predOrdI)
next
  case (R_2_enc tid2) thus ?thesis
  proof(sources " LN ''nr'' tid2 ")
    case (I_3_nr tid4) thus ?thesis
    proof(sources "
        Enc {| LN ''ni'' tid4, LN ''nr'' tid2, s(|AV ''R'' tid4|) |}
            ( PK ( s(|AV ''I'' tid4|) ) ) ")
      case (R_2_enc tid6) thus ?thesis
      by (fastsimp dest: I_sk_R_secrecy intro: event_predOrdI)
    qed ((clarsimp, order?)+)?
  next
    case (R_2_ni tid4) thus ?thesis
    proof(sources "
        Enc {| LN ''nr'' tid2, s(|AV ''I'' tid4|) |}
            ( PK ( s(|AV ''R'' tid4|) ) ) ")
    qed ((clarsimp, order?)+)?
  next
    case (R_2_nr tid4) thus ?thesis
    by (fastsimp dest: I_sk_I_secrecy intro: event_predOrdI)
  qed
qed ((clarsimp, order?)+)?

lemma (in atomic_nsl3_state) I_ni_synch:
  assumes asms:
    "roleMap r tid1 = Some I"
    "s(|AV ''I'' tid1|) ~: Compromised"
    "s(|AV ''R'' tid1|) ~: Compromised"
    "(tid1, I_3) : steps t"
  shows
    "? tid2 . roleMap r tid2 = Some R &
         s(|AV ''I'' tid2|) = s(|AV ''I'' tid1|) &
         s(|AV ''R'' tid2|) = s(|AV ''R'' tid1|) &
         s(|NV ''ni'' tid2|) = LN ''ni'' tid1 &
         s(|NV ''nr'' tid1|) = LN ''nr'' tid2 &
         predOrd t (St(tid1, I_1)) (St(tid2, R_1)) &
         predOrd t (St(tid1, I_2)) (St(tid1, I_3)) &
         predOrd t (St(tid2, R_2)) (St(tid1, I_2)) &
         predOrd t (St(tid2, R_1)) (St(tid2, R_2))"
using asms prefix_close
proof(sources "
    Enc {| LN ''ni'' tid1, s(|NV ''nr'' tid1|), s(|AV ''R'' tid1|) |}
        ( PK ( s(|AV ''I'' tid1|) ) ) ")
  case fake thus ?thesis
  by (fastsimp dest: I_nr_secrecy intro: event_predOrdI)
next
  case (I_3_enc tid3) thus ?thesis
  by (fastsimp dest: I_nr_secrecy intro: event_predOrdI)
next
  case (R_2_enc tid3) thus ?thesis
  proof(sources "
      Enc {| LN ''ni'' tid1, s(|AV ''I'' tid1|) |}
          ( PK ( s(|AV ''R'' tid1|) ) ) ")
    case fake thus ?thesis
    by (fastsimp dest: I_ni_secrecy intro: event_predOrdI)
  next
    case (I_1_enc tid5) thus ?thesis
    by auto
  next
    case (I_3_enc tid5) thus ?thesis
    by (fastsimp dest: I_ni_secrecy intro: event_predOrdI)
  qed ((clarsimp, order?)+)?
qed ((clarsimp, order?)+)?

end