1 theory Engin

     2 imports Main

     3 begin

     4 

     5 typedecl principal

     6 

     7 consts E :: principal

     8 consts T :: principal

     9 consts M :: principal

    10 

    11 consts Says :: "principal \<Rightarrow> bool \<Rightarrow> bool" ("_ says _" [101, 101] 100)

    12 consts Sends :: "principal \<Rightarrow> principal \<Rightarrow> bool \<Rightarrow> bool" ("_ sends _ : _" [100, 100, 100] 100)

    13 consts Enc :: "bool \<Rightarrow> bool \<Rightarrow> bool"

    14 consts Id  :: "principal \<Rightarrow> bool"

    15 

    16 consts N :: "bool"

    17 consts K :: "bool"

    18 consts start_engine :: "principal \<Rightarrow> bool"

    19 

    20 

    21 axiomatization where

    22   saysI[intro]: "F \<Longrightarrow> P says F" and

    23   saysE[elim]:  "\<lbrakk>P says (F1 \<longrightarrow> F2); P says F1\<rbrakk> \<Longrightarrow> P says F2" and

    24   says_encI[intro]: "\<lbrakk>P says F1; P says F2\<rbrakk> \<Longrightarrow> P says (Enc F1 F2)" and

    25   says_encE[elim]: "\<lbrakk>P says (Enc F1 F2); P says F2\<rbrakk> \<Longrightarrow> P says F1" and

    26   sendsE[elim]: "\<lbrakk>P sends Q : F; P says F\<rbrakk> \<Longrightarrow> Q says F"

    27    

    28 

    29 lemma

    30   assumes start: "E says N"

    31   and challenge: "E sends T : N"

    32   and  response: "T says N \<longrightarrow> (T sends E : (Enc N K) \<and> T sends E : Id(T))"

    33   and      keyT: "T says K"

    34   and       idT: "T says Id T"

    35   and    engine: "(E says (Enc N K) \<and> E says Id(T)) \<longrightarrow> start_engine T"

    36   shows "start_engine T"

    37 using assms

    38 by (metis says_encI sendsE)

    39 

    40 lemma

    41   assumes start: "E says N"

    42   and challenge: "\<forall>T. E sends T : N"

    43   and  response: "\<forall>N E. T says N \<longrightarrow> (T sends E : (Enc N K) \<and> T sends E : Id(T))"

    44   and      keyT: "T says K"

    45   and       idT: "T says Id T"

    46   and    engine: "\<forall>T. (E says (Enc N K) \<and> E says Id(T)) \<longrightarrow> start_engine T"

    47   shows "start_engine M"

    48 using assms

    49 sorry

    50 (*by (metis saysE says_encE says_encI sendsE)*)

    51 

    52 lemma

    53   assumes start: "E says N"

    54   and challenge: "\<forall>T. E sends T : N"

    55   and  response: "\<forall>N E. T says N \<longrightarrow> (T sends E : (Enc N K) \<and> T sends E : Id T)"

    56   and      keyT: "T says K"

    57   and       idT: "T says Id T"

    58   and    engine: "\<forall>T. (E says (Enc N K) \<and> E says Id T) \<longrightarrow> start_engine T"

    59   and   middle1: "\<forall>N. M sends T : N" 

    60   and   middle2: "\<forall>N'. M sends E : N'"

    61   and   middle3: "M says Id M"

    62   shows "start_engine M"

    63 using assms

    64 

    65 by (metis saysE says_encE says_encI sendsE)

    66 

    67 end