theory "isoiec-9798-2-bdkey_cert_auto" imports "ESPLogic" begin role isoiec_9798_2_1_bdkey_A where "isoiec_9798_2_1_bdkey_A = [ Send ''leak_A'' ( sN ''TNA'' ) , Recv ''text_1'' <| sMV ''Text1'', sMV ''Text2'' |> , Send ''1'' <| sAV ''A'', sAV ''B'', sMV ''Text2'', PEnc <| sC ''isoiec_9798_2_1_enc_1'', sN ''TNA'', sAV ''B'', sMV ''Text1'' |> ( sKbd (AVar ''A'') (AVar ''B'') ) |> ]" role isoiec_9798_2_1_bdkey_B where "isoiec_9798_2_1_bdkey_B = [ Recv ''1'' <| sMV ''A'', sAV ''B'', sMV ''Text2'', PEnc <| sC ''isoiec_9798_2_1_enc_1'', sMV ''TNA'', sAV ''B'', sMV ''Text1'' |> ( sKbd (MVar ''A'') (AVar ''B'') ) |> ]" role isoiec_9798_2_2_bdkey_A where "isoiec_9798_2_2_bdkey_A = [ Recv ''1'' <| sMV ''B'', sAV ''A'', sMV ''RB'', sMV ''Text1'' |> , Recv ''text_2'' <| sMV ''Text2'', sMV ''Text3'' |> , Send ''2'' <| sAV ''A'', sMV ''B'', sMV ''Text3'', PEnc <| sC ''isoiec_9798_2_2_enc_2'', sMV ''RB'', sMV ''B'', sMV ''Text2'' |> ( sKbd (MVar ''B'') (AVar ''A'') ) |> ]" role isoiec_9798_2_2_bdkey_B where "isoiec_9798_2_2_bdkey_B = [ Recv ''text_1'' ( sMV ''Text1'' ) , Send ''1'' <| sAV ''B'', sAV ''A'', sN ''RB'', sMV ''Text1'' |> , Recv ''2'' <| sAV ''A'', sAV ''B'', sMV ''Text3'', PEnc <| sC ''isoiec_9798_2_2_enc_2'', sN ''RB'', sAV ''B'', sMV ''Text2'' |> ( sKbd (AVar ''B'') (AVar ''A'') ) |> ]" role isoiec_9798_2_3_bdkey_A where "isoiec_9798_2_3_bdkey_A = [ Send ''leak_A'' ( sN ''TNA'' ) , Recv ''text_1'' <| sMV ''Text1'', sMV ''Text2'' |> , Send ''1'' <| sAV ''A'', sAV ''B'', sMV ''Text2'', PEnc <| sC ''isoiec_9798_2_3_enc_1'', sN ''TNA'', sAV ''B'', sMV ''Text1'' |> ( sKbd (AVar ''A'') (AVar ''B'') ) |> , Recv ''2'' <| sAV ''B'', sAV ''A'', sMV ''Text4'', PEnc <| sC ''isoiec_9798_2_3_enc_2'', sMV ''TNB'', sAV ''A'', sMV ''Text3'' |> ( sKbd (AVar ''B'') (AVar ''A'') ) |> ]" role isoiec_9798_2_3_bdkey_B where "isoiec_9798_2_3_bdkey_B = [ Send ''leak_B'' ( sN ''TNB'' ) , Recv ''1'' <| sMV ''A'', sAV ''B'', sMV ''Text2'', PEnc <| sC ''isoiec_9798_2_3_enc_1'', sMV ''TNA'', sAV ''B'', sMV ''Text1'' |> ( sKbd (MVar ''A'') (AVar ''B'') ) |> , Recv ''text_2'' <| sMV ''Text3'', sMV ''Text4'' |> , Send ''2'' <| sAV ''B'', sMV ''A'', sMV ''Text4'', PEnc <| sC ''isoiec_9798_2_3_enc_2'', sN ''TNB'', sMV ''A'', sMV ''Text3'' |> ( sKbd (AVar ''B'') (MVar ''A'') ) |> ]" role isoiec_9798_2_4_bdkey_A where "isoiec_9798_2_4_bdkey_A = [ Recv ''1'' <| sMV ''B'', sAV ''A'', sMV ''RB'', sMV ''Text1'' |> , Recv ''text_2'' <| sMV ''Text2'', sMV ''Text3'' |> , Send ''2'' <| sAV ''A'', sMV ''B'', sMV ''Text3'', PEnc <| sC ''isoiec_9798_2_4_enc_1'', sN ''RA'', sMV ''RB'', sMV ''B'', sMV ''Text2'' |> ( sKbd (AVar ''A'') (MVar ''B'') ) |> , Recv ''3'' <| sMV ''B'', sAV ''A'', sMV ''Text5'', PEnc <| sC ''isoiec_9798_2_4_enc_2'', sMV ''RB'', sN ''RA'', sMV ''Text4'' |> ( sKbd (AVar ''A'') (MVar ''B'') ) |> ]" role isoiec_9798_2_4_bdkey_B where "isoiec_9798_2_4_bdkey_B = [ Recv ''text_1'' ( sMV ''Text1'' ) , Send ''1'' <| sAV ''B'', sAV ''A'', sN ''RB'', sMV ''Text1'' |> , Recv ''2'' <| sAV ''A'', sAV ''B'', sMV ''Text3'', PEnc <| sC ''isoiec_9798_2_4_enc_1'', sMV ''RA'', sN ''RB'', sAV ''B'', sMV ''Text2'' |> ( sKbd (AVar ''A'') (AVar ''B'') ) |> , Recv ''text_3'' <| sMV ''Text4'', sMV ''Text5'' |> , Send ''3'' <| sAV ''B'', sAV ''A'', sMV ''Text5'', PEnc <| sC ''isoiec_9798_2_4_enc_2'', sN ''RB'', sMV ''RA'', sMV ''Text4'' |> ( sKbd (AVar ''A'') (AVar ''B'') ) |> ]" role isoiec_9798_2_5_bdkey_A where "isoiec_9798_2_5_bdkey_A = [ Send ''leak_A'' <| sN ''TVPa'', sN ''TNa'' |> , Recv ''text_1'' ( sMV ''Text1'' ) , Send ''1'' <| sAV ''A'', sAV ''P'', sN ''TVPa'', sAV ''B'', sMV ''Text1'' |> , Recv ''2'' <| sAV ''P'', sAV ''A'', sMV ''Text4'', PEnc <| sC ''isoiec_9798_2_5_enc_2_1'', sN ''TVPa'', sMV ''Kab'', sAV ''A'', sAV ''B'', sMV ''Text3'' |> ( sKbd (AVar ''A'') (AVar ''P'') ), sMV ''TokenPA_for_B'' |> , Recv ''text_3'' <| sMV ''Text5'', sMV ''Text6'' |> , Send ''3'' <| sAV ''A'', sAV ''B'', sMV ''Text6'', sAV ''P'', sMV ''TokenPA_for_B'', PEnc <| sC ''isoiec_9798_2_5_enc_3'', sN ''TNa'', sAV ''B'', sMV ''Text5'' |> ( sMV ''Kab'' ) |> , Recv ''4'' <| sAV ''B'', sAV ''A'', sMV ''Text8'', PEnc <| sC ''isoiec_9798_2_5_enc_4'', sMV ''TNb'', sAV ''A'', sMV ''Text7'' |> ( sMV ''Kab'' ) |> ]" role isoiec_9798_2_5_bdkey_B where "isoiec_9798_2_5_bdkey_B = [ Send ''leak_B'' ( sN ''TNb'' ) , Recv ''3'' <| sMV ''A'', sAV ''B'', sMV ''Text6'', sMV ''P'', PEnc <| sC ''isoiec_9798_2_5_enc_2_2'', sMV ''TNp'', sMV ''Kab'', sMV ''A'', sAV ''B'', sMV ''Text2'' |> ( sKbd (AVar ''B'') (MVar ''P'') ), PEnc <| sC ''isoiec_9798_2_5_enc_3'', sMV ''TNa'', sAV ''B'', sMV ''Text5'' |> ( sMV ''Kab'' ) |> , Recv ''text_4'' <| sMV ''Text7'', sMV ''Text8'' |> , Send ''4'' <| sAV ''B'', sMV ''A'', sMV ''Text8'', PEnc <| sC ''isoiec_9798_2_5_enc_4'', sN ''TNb'', sMV ''A'', sMV ''Text7'' |> ( sMV ''Kab'' ) |> ]" role isoiec_9798_2_5_bdkey_P where "isoiec_9798_2_5_bdkey_P = [ Send ''leak_P'' ( sN ''TNp'' ) , Recv ''1'' <| sMV ''A'', sAV ''P'', sMV ''TVPa'', sMV ''B'', sMV ''Text1'' |> , Recv ''text_2'' <| sMV ''Text2'', sMV ''Text3'', sMV ''Text4'' |> , Send ''2'' <| sAV ''P'', sMV ''A'', sMV ''Text4'', PEnc <| sC ''isoiec_9798_2_5_enc_2_1'', sMV ''TVPa'', sN ''Kab'', sMV ''A'', sMV ''B'', sMV ''Text3'' |> ( sKbd (MVar ''A'') (AVar ''P'') ), PEnc <| sC ''isoiec_9798_2_5_enc_2_2'', sN ''TNp'', sN ''Kab'', sMV ''A'', sMV ''B'', sMV ''Text2'' |> ( sKbd (MVar ''B'') (AVar ''P'') ) |> ]" role isoiec_9798_2_6_bdkey_A where "isoiec_9798_2_6_bdkey_A = [ Recv ''1'' <| sMV ''B'', sAV ''A'', sMV ''Rb'', sMV ''Text1'' |> , Recv ''text_2'' ( sMV ''Text2'' ) , Send ''2'' <| sAV ''A'', sAV ''P'', sN ''Ra'', sMV ''Rb'', sMV ''B'', sMV ''Text2'' |> , Recv ''3'' <| sAV ''P'', sAV ''A'', sMV ''Text5'', PEnc <| sC ''isoiec_9798_2_6_enc_3_1'', sN ''Ra'', sMV ''Kab'', sAV ''A'', sMV ''B'', sMV ''Text4'' |> ( sKbd (AVar ''A'') (AVar ''P'') ), sMV ''TokenPA_for_B'' |> , Recv ''text_4'' <| sMV ''Text6'', sMV ''Text7'' |> , Send ''4'' <| sAV ''A'', sMV ''B'', sMV ''Text7'', sAV ''P'', sMV ''TokenPA_for_B'', PEnc <| sC ''isoiec_9798_2_6_enc_4'', sN ''Rpa'', sMV ''Rb'', sMV ''Text6'' |> ( sMV ''Kab'' ) |> , Recv ''5'' <| sMV ''B'', sAV ''A'', sMV ''Text9'', PEnc <| sC ''isoiec_9798_2_6_enc_5'', sMV ''Rb'', sN ''Rpa'', sMV ''Text8'' |> ( sMV ''Kab'' ) |> ]" role isoiec_9798_2_6_bdkey_B where "isoiec_9798_2_6_bdkey_B = [ Recv ''text_1'' ( sMV ''Text1'' ) , Send ''1'' <| sAV ''B'', sAV ''A'', sN ''Rb'', sMV ''Text1'' |> , Recv ''4'' <| sAV ''A'', sAV ''B'', sMV ''Text7'', sMV ''P'', PEnc <| sC ''isoiec_9798_2_6_enc_3_2'', sN ''Rb'', sMV ''Kab'', sAV ''A'', sAV ''B'', sMV ''Text3'' |> ( sKbd (AVar ''B'') (MVar ''P'') ), PEnc <| sC ''isoiec_9798_2_6_enc_4'', sMV ''Rpa'', sN ''Rb'', sMV ''Text6'' |> ( sMV ''Kab'' ) |> , Recv ''text_5'' <| sMV ''Text8'', sMV ''Text9'' |> , Send ''5'' <| sAV ''B'', sAV ''A'', sMV ''Text9'', PEnc <| sC ''isoiec_9798_2_6_enc_5'', sN ''Rb'', sMV ''Rpa'', sMV ''Text8'' |> ( sMV ''Kab'' ) |> ]" role isoiec_9798_2_6_bdkey_P where "isoiec_9798_2_6_bdkey_P = [ Recv ''2'' <| sMV ''A'', sAV ''P'', sMV ''Ra'', sMV ''Rb'', sMV ''B'', sMV ''Text2'' |> , Recv ''text_3'' <| sMV ''Text3'', sMV ''Text4'', sMV ''Text5'' |> , Send ''3'' <| sAV ''P'', sMV ''A'', sMV ''Text5'', PEnc <| sC ''isoiec_9798_2_6_enc_3_1'', sMV ''Ra'', sN ''Kab'', sMV ''A'', sMV ''B'', sMV ''Text4'' |> ( sKbd (MVar ''A'') (AVar ''P'') ), PEnc <| sC ''isoiec_9798_2_6_enc_3_2'', sMV ''Rb'', sN ''Kab'', sMV ''A'', sMV ''B'', sMV ''Text3'' |> ( sKbd (MVar ''B'') (AVar ''P'') ) |> ]" role isoiec_9798_2_5_special_TTP_bdkey_A where "isoiec_9798_2_5_special_TTP_bdkey_A = [ Send ''leak_A'' <| sN ''TVPa'', sN ''TNa'' |> , Recv ''text_1'' ( sMV ''Text1'' ) , Send ''1'' <| sAV ''A'', sAV ''P'', sN ''TVPa'', sAV ''B'', sMV ''Text1'' |> , Recv ''2'' <| sAV ''P'', sAV ''A'', sMV ''Text4'', PEnc <| sC ''isoiec_9798_2_5_special_TTP_enc_2_1'', sN ''TVPa'', sMV ''Kab'', sAV ''B'', sMV ''Text3'' |> ( sKbd (AVar ''A'') (AVar ''P'') ), sMV ''TokenPA_for_B'' |> , Recv ''text_3'' <| sMV ''Text5'', sMV ''Text6'' |> , Send ''3'' <| sAV ''A'', sAV ''B'', sMV ''Text6'', sAV ''P'', sMV ''TokenPA_for_B'', PEnc <| sC ''isoiec_9798_2_5_special_TTP_enc_3'', sN ''TNa'', sAV ''B'', sMV ''Text5'' |> ( sMV ''Kab'' ) |> , Recv ''4'' <| sAV ''B'', sAV ''A'', sMV ''Text8'', PEnc <| sC ''isoiec_9798_2_5_special_TTP_enc_4'', sMV ''TNb'', sAV ''A'', sMV ''Text7'' |> ( sMV ''Kab'' ) |> ]" role isoiec_9798_2_5_special_TTP_bdkey_B where "isoiec_9798_2_5_special_TTP_bdkey_B = [ Send ''leak_B'' ( sN ''TNb'' ) , Recv ''3'' <| sMV ''A'', sAV ''B'', sMV ''Text6'', sMV ''P'', PEnc <| sC ''isoiec_9798_2_5_special_TTP_enc_2_2'', sMV ''TNp'', sMV ''Kab'', sMV ''A'', sMV ''Text2'' |> ( sKbd (AVar ''B'') (MVar ''P'') ), PEnc <| sC ''isoiec_9798_2_5_special_TTP_enc_3'', sMV ''TNa'', sAV ''B'', sMV ''Text5'' |> ( sMV ''Kab'' ) |> , Recv ''text_4'' <| sMV ''Text7'', sMV ''Text8'' |> , Send ''4'' <| sAV ''B'', sMV ''A'', sMV ''Text8'', PEnc <| sC ''isoiec_9798_2_5_special_TTP_enc_4'', sN ''TNb'', sMV ''A'', sMV ''Text7'' |> ( sMV ''Kab'' ) |> ]" role isoiec_9798_2_5_special_TTP_bdkey_P where "isoiec_9798_2_5_special_TTP_bdkey_P = [ Send ''leak_P'' ( sN ''TNp'' ) , Recv ''1'' <| sMV ''A'', sAV ''P'', sMV ''TVPa'', sMV ''B'', sMV ''Text1'' |> , Recv ''text_2'' <| sMV ''Text2'', sMV ''Text3'', sMV ''Text4'' |> , Send ''2'' <| sAV ''P'', sMV ''A'', sMV ''Text4'', PEnc <| sC ''isoiec_9798_2_5_special_TTP_enc_2_1'', sMV ''TVPa'', sN ''Kab'', sMV ''B'', sMV ''Text3'' |> ( sKbd (MVar ''A'') (AVar ''P'') ), PEnc <| sC ''isoiec_9798_2_5_special_TTP_enc_2_2'', sN ''TNp'', sN ''Kab'', sMV ''A'', sMV ''Text2'' |> ( sKbd (MVar ''B'') (AVar ''P'') ) |> ]" role isoiec_9798_2_6_special_TTP_bdkey_A where "isoiec_9798_2_6_special_TTP_bdkey_A = [ Recv ''1'' <| sMV ''B'', sAV ''A'', sMV ''Rb'', sMV ''Text1'' |> , Recv ''text_2'' ( sMV ''Text2'' ) , Send ''2'' <| sAV ''A'', sAV ''P'', sN ''Ra'', sMV ''Rb'', sMV ''B'', sMV ''Text2'' |> , Recv ''3'' <| sAV ''P'', sAV ''A'', sMV ''Text5'', PEnc <| sC ''isoiec_9798_2_6_special_TTP_enc_3_1'', sN ''Ra'', sMV ''Kab'', sMV ''B'', sMV ''Text4'' |> ( sKbd (AVar ''A'') (AVar ''P'') ), sMV ''TokenPA_for_B'' |> , Recv ''text_4'' <| sMV ''Text6'', sMV ''Text7'' |> , Send ''4'' <| sAV ''A'', sMV ''B'', sMV ''Text7'', sAV ''P'', sMV ''TokenPA_for_B'', PEnc <| sC ''isoiec_9798_2_6_special_TTP_enc_4'', sN ''Rpa'', sMV ''Rb'', sMV ''Text6'' |> ( sMV ''Kab'' ) |> , Recv ''5'' <| sMV ''B'', sAV ''A'', sMV ''Text9'', PEnc <| sC ''isoiec_9798_2_6_special_TTP_enc_5'', sMV ''Rb'', sN ''Rpa'', sMV ''Text8'' |> ( sMV ''Kab'' ) |> ]" role isoiec_9798_2_6_special_TTP_bdkey_B where "isoiec_9798_2_6_special_TTP_bdkey_B = [ Recv ''text_1'' ( sMV ''Text1'' ) , Send ''1'' <| sAV ''B'', sAV ''A'', sN ''Rb'', sMV ''Text1'' |> , Recv ''4'' <| sAV ''A'', sAV ''B'', sMV ''Text7'', sMV ''P'', PEnc <| sC ''isoiec_9798_2_6_special_TTP_enc_3_2'', sN ''Rb'', sMV ''Kab'', sAV ''A'', sMV ''Text3'' |> ( sKbd (AVar ''B'') (MVar ''P'') ), PEnc <| sC ''isoiec_9798_2_6_special_TTP_enc_4'', sMV ''Rpa'', sN ''Rb'', sMV ''Text6'' |> ( sMV ''Kab'' ) |> , Recv ''text_5'' <| sMV ''Text8'', sMV ''Text9'' |> , Send ''5'' <| sAV ''B'', sAV ''A'', sMV ''Text9'', PEnc <| sC ''isoiec_9798_2_6_special_TTP_enc_5'', sN ''Rb'', sMV ''Rpa'', sMV ''Text8'' |> ( sMV ''Kab'' ) |> ]" role isoiec_9798_2_6_special_TTP_bdkey_P where "isoiec_9798_2_6_special_TTP_bdkey_P = [ Recv ''2'' <| sMV ''A'', sAV ''P'', sMV ''Ra'', sMV ''Rb'', sMV ''B'', sMV ''Text2'' |> , Recv ''text_3'' <| sMV ''Text3'', sMV ''Text4'', sMV ''Text5'' |> , Send ''3'' <| sAV ''P'', sMV ''A'', sMV ''Text5'', PEnc <| sC ''isoiec_9798_2_6_special_TTP_enc_3_1'', sMV ''Ra'', sN ''Kab'', sMV ''B'', sMV ''Text4'' |> ( sKbd (MVar ''A'') (AVar ''P'') ), PEnc <| sC ''isoiec_9798_2_6_special_TTP_enc_3_2'', sMV ''Rb'', sN ''Kab'', sMV ''A'', sMV ''Text3'' |> ( sKbd (MVar ''B'') (AVar ''P'') ) |> ]" protocol isoiec_9798_2_bdkey where "isoiec_9798_2_bdkey = { isoiec_9798_2_1_bdkey_A, isoiec_9798_2_1_bdkey_B, isoiec_9798_2_2_bdkey_A, isoiec_9798_2_2_bdkey_B, isoiec_9798_2_3_bdkey_A, isoiec_9798_2_3_bdkey_B, isoiec_9798_2_4_bdkey_A, isoiec_9798_2_4_bdkey_B, isoiec_9798_2_5_bdkey_A, isoiec_9798_2_5_bdkey_B, isoiec_9798_2_5_bdkey_P, isoiec_9798_2_6_bdkey_A, isoiec_9798_2_6_bdkey_B, isoiec_9798_2_6_bdkey_P, isoiec_9798_2_5_special_TTP_bdkey_A, isoiec_9798_2_5_special_TTP_bdkey_B, isoiec_9798_2_5_special_TTP_bdkey_P, isoiec_9798_2_6_special_TTP_bdkey_A, isoiec_9798_2_6_special_TTP_bdkey_B, isoiec_9798_2_6_special_TTP_bdkey_P }" locale restricted_isoiec_9798_2_bdkey_state = isoiec_9798_2_bdkey_state + assumes isoiec_9798_2_5_special_TTP_bdkey_different_actors_A_P: "!! tid0 tid1. [| roleMap r tid0 = Some isoiec_9798_2_5_special_TTP_bdkey_A; roleMap r tid1 = Some isoiec_9798_2_5_special_TTP_bdkey_P; s(AV ''P'' tid1) = s(AV ''A'' tid0) |] ==> False" assumes isoiec_9798_2_6_special_TTP_bdkey_different_actors_A_P: "!! tid0 tid1. [| roleMap r tid0 = Some isoiec_9798_2_6_special_TTP_bdkey_A; roleMap r tid1 = Some isoiec_9798_2_6_special_TTP_bdkey_P; s(AV ''P'' tid1) = s(AV ''A'' tid0) |] ==> False" assumes isoiec_9798_2_6_special_TTP_bdkey_different_actors_B_P: "!! tid0 tid1. [| roleMap r tid0 = Some isoiec_9798_2_6_special_TTP_bdkey_B; roleMap r tid1 = Some isoiec_9798_2_6_special_TTP_bdkey_P; s(AV ''P'' tid1) = s(AV ''B'' tid0) |] ==> False" type_invariant isoiec_9798_2_bdkey_composed_typing for isoiec_9798_2_bdkey where "isoiec_9798_2_bdkey_composed_typing = mk_typing [ ((isoiec_9798_2_1_bdkey_B, ''A''), (KnownT isoiec_9798_2_1_bdkey_B_1)) , ((isoiec_9798_2_3_bdkey_B, ''A''), (KnownT isoiec_9798_2_3_bdkey_B_1)) , ((isoiec_9798_2_5_bdkey_B, ''A''), (KnownT isoiec_9798_2_5_bdkey_B_3)) , ((isoiec_9798_2_5_bdkey_P, ''A''), (KnownT isoiec_9798_2_5_bdkey_P_1)) , ((isoiec_9798_2_5_special_TTP_bdkey_B, ''A''), (KnownT isoiec_9798_2_5_special_TTP_bdkey_B_3)) , ((isoiec_9798_2_5_special_TTP_bdkey_P, ''A''), (KnownT isoiec_9798_2_5_special_TTP_bdkey_P_1)) , ((isoiec_9798_2_6_bdkey_P, ''A''), (KnownT isoiec_9798_2_6_bdkey_P_2)) , ((isoiec_9798_2_6_special_TTP_bdkey_P, ''A''), (KnownT isoiec_9798_2_6_special_TTP_bdkey_P_2)) , ((isoiec_9798_2_2_bdkey_A, ''B''), (KnownT isoiec_9798_2_2_bdkey_A_1)) , ((isoiec_9798_2_4_bdkey_A, ''B''), (KnownT isoiec_9798_2_4_bdkey_A_1)) , ((isoiec_9798_2_5_bdkey_P, ''B''), (KnownT isoiec_9798_2_5_bdkey_P_1)) , ((isoiec_9798_2_5_special_TTP_bdkey_P, ''B''), (KnownT isoiec_9798_2_5_special_TTP_bdkey_P_1)) , ((isoiec_9798_2_6_bdkey_A, ''B''), (KnownT isoiec_9798_2_6_bdkey_A_1)) , ((isoiec_9798_2_6_bdkey_P, ''B''), (KnownT isoiec_9798_2_6_bdkey_P_2)) , ((isoiec_9798_2_6_special_TTP_bdkey_A, ''B''), (KnownT isoiec_9798_2_6_special_TTP_bdkey_A_1)) , ((isoiec_9798_2_6_special_TTP_bdkey_P, ''B''), (KnownT isoiec_9798_2_6_special_TTP_bdkey_P_2)) , ((isoiec_9798_2_5_bdkey_A, ''Kab''), (SumT (KnownT isoiec_9798_2_5_bdkey_A_2) (NonceT isoiec_9798_2_5_bdkey_P ''Kab''))) , ((isoiec_9798_2_5_bdkey_B, ''Kab''), (SumT (KnownT isoiec_9798_2_5_bdkey_B_3) (NonceT isoiec_9798_2_5_bdkey_P ''Kab''))) , ((isoiec_9798_2_5_special_TTP_bdkey_A, ''Kab''), (SumT (KnownT isoiec_9798_2_5_special_TTP_bdkey_A_2) (NonceT isoiec_9798_2_5_special_TTP_bdkey_P ''Kab''))) , ((isoiec_9798_2_5_special_TTP_bdkey_B, ''Kab''), (SumT (KnownT isoiec_9798_2_5_special_TTP_bdkey_B_3) (NonceT isoiec_9798_2_5_special_TTP_bdkey_P ''Kab''))) , ((isoiec_9798_2_6_bdkey_A, ''Kab''), (SumT (KnownT isoiec_9798_2_6_bdkey_A_3) (NonceT isoiec_9798_2_6_bdkey_P ''Kab''))) , ((isoiec_9798_2_6_bdkey_B, ''Kab''), (SumT (KnownT isoiec_9798_2_6_bdkey_B_4) (NonceT isoiec_9798_2_6_bdkey_P ''Kab''))) , ((isoiec_9798_2_6_special_TTP_bdkey_A, ''Kab''), (SumT (KnownT isoiec_9798_2_6_special_TTP_bdkey_A_3) (NonceT isoiec_9798_2_6_special_TTP_bdkey_P ''Kab''))) , ((isoiec_9798_2_6_special_TTP_bdkey_B, ''Kab''), (SumT (KnownT isoiec_9798_2_6_special_TTP_bdkey_B_4) (NonceT isoiec_9798_2_6_special_TTP_bdkey_P ''Kab''))) , ((isoiec_9798_2_5_bdkey_B, ''P''), (KnownT isoiec_9798_2_5_bdkey_B_3)) , ((isoiec_9798_2_5_special_TTP_bdkey_B, ''P''), (KnownT isoiec_9798_2_5_special_TTP_bdkey_B_3)) , ((isoiec_9798_2_6_bdkey_B, ''P''), (KnownT isoiec_9798_2_6_bdkey_B_4)) , ((isoiec_9798_2_6_special_TTP_bdkey_B, ''P''), (KnownT isoiec_9798_2_6_special_TTP_bdkey_B_4)) , ((isoiec_9798_2_4_bdkey_B, ''RA''), (SumT (KnownT isoiec_9798_2_4_bdkey_B_2) (NonceT isoiec_9798_2_4_bdkey_A ''RA''))) , ((isoiec_9798_2_2_bdkey_A, ''RB''), (KnownT isoiec_9798_2_2_bdkey_A_1)) , ((isoiec_9798_2_4_bdkey_A, ''RB''), (KnownT isoiec_9798_2_4_bdkey_A_1)) , ((isoiec_9798_2_6_bdkey_P, ''Ra''), (KnownT isoiec_9798_2_6_bdkey_P_2)) , ((isoiec_9798_2_6_special_TTP_bdkey_P, ''Ra''), (KnownT isoiec_9798_2_6_special_TTP_bdkey_P_2)) , ((isoiec_9798_2_6_bdkey_A, ''Rb''), (KnownT isoiec_9798_2_6_bdkey_A_1)) , ((isoiec_9798_2_6_bdkey_P, ''Rb''), (KnownT isoiec_9798_2_6_bdkey_P_2)) , ((isoiec_9798_2_6_special_TTP_bdkey_A, ''Rb''), (KnownT isoiec_9798_2_6_special_TTP_bdkey_A_1)) , ((isoiec_9798_2_6_special_TTP_bdkey_P, ''Rb''), (KnownT isoiec_9798_2_6_special_TTP_bdkey_P_2)) , ((isoiec_9798_2_6_bdkey_B, ''Rpa''), (SumT (KnownT isoiec_9798_2_6_bdkey_B_4) (NonceT isoiec_9798_2_6_bdkey_A ''Rpa''))) , ((isoiec_9798_2_6_special_TTP_bdkey_B, ''Rpa''), (SumT (KnownT isoiec_9798_2_6_special_TTP_bdkey_B_4) (NonceT isoiec_9798_2_6_special_TTP_bdkey_A ''Rpa''))) , ((isoiec_9798_2_1_bdkey_B, ''TNA''), (SumT (KnownT isoiec_9798_2_1_bdkey_B_1) (NonceT isoiec_9798_2_1_bdkey_A ''TNA''))) , ((isoiec_9798_2_3_bdkey_B, ''TNA''), (SumT (KnownT isoiec_9798_2_3_bdkey_B_1) (NonceT isoiec_9798_2_3_bdkey_A ''TNA''))) , ((isoiec_9798_2_3_bdkey_A, ''TNB''), (SumT (KnownT isoiec_9798_2_3_bdkey_A_2) (NonceT isoiec_9798_2_3_bdkey_B ''TNB''))) , ((isoiec_9798_2_5_bdkey_B, ''TNa''), (SumT (KnownT isoiec_9798_2_5_bdkey_B_3) (NonceT isoiec_9798_2_5_bdkey_A ''TNa''))) , ((isoiec_9798_2_5_special_TTP_bdkey_B, ''TNa''), (SumT (KnownT isoiec_9798_2_5_special_TTP_bdkey_B_3) (NonceT isoiec_9798_2_5_special_TTP_bdkey_A ''TNa''))) , ((isoiec_9798_2_5_bdkey_A, ''TNb''), (SumT (KnownT isoiec_9798_2_5_bdkey_A_4) (NonceT isoiec_9798_2_5_bdkey_B ''TNb''))) , ((isoiec_9798_2_5_special_TTP_bdkey_A, ''TNb''), (SumT (KnownT isoiec_9798_2_5_special_TTP_bdkey_A_4) (NonceT isoiec_9798_2_5_special_TTP_bdkey_B ''TNb''))) , ((isoiec_9798_2_5_bdkey_B, ''TNp''), (SumT (KnownT isoiec_9798_2_5_bdkey_B_3) (NonceT isoiec_9798_2_5_bdkey_P ''TNp''))) , ((isoiec_9798_2_5_special_TTP_bdkey_B, ''TNp''), (SumT (KnownT isoiec_9798_2_5_special_TTP_bdkey_B_3) (NonceT isoiec_9798_2_5_special_TTP_bdkey_P ''TNp''))) , ((isoiec_9798_2_5_bdkey_P, ''TVPa''), (KnownT isoiec_9798_2_5_bdkey_P_1)) , ((isoiec_9798_2_5_special_TTP_bdkey_P, ''TVPa''), (KnownT isoiec_9798_2_5_special_TTP_bdkey_P_1)) , ((isoiec_9798_2_1_bdkey_A, ''Text1''), (KnownT isoiec_9798_2_1_bdkey_A_text_1)) , ((isoiec_9798_2_1_bdkey_B, ''Text1''), (KnownT isoiec_9798_2_1_bdkey_B_1)) , ((isoiec_9798_2_2_bdkey_A, ''Text1''), (KnownT isoiec_9798_2_2_bdkey_A_1)) , ((isoiec_9798_2_2_bdkey_B, ''Text1''), (KnownT isoiec_9798_2_2_bdkey_B_text_1)) , ((isoiec_9798_2_3_bdkey_A, ''Text1''), (KnownT isoiec_9798_2_3_bdkey_A_text_1)) , ((isoiec_9798_2_3_bdkey_B, ''Text1''), (KnownT isoiec_9798_2_3_bdkey_B_1)) , ((isoiec_9798_2_4_bdkey_A, ''Text1''), (KnownT isoiec_9798_2_4_bdkey_A_1)) , ((isoiec_9798_2_4_bdkey_B, ''Text1''), (KnownT isoiec_9798_2_4_bdkey_B_text_1)) , ((isoiec_9798_2_5_bdkey_A, ''Text1''), (KnownT isoiec_9798_2_5_bdkey_A_text_1)) , ((isoiec_9798_2_5_bdkey_P, ''Text1''), (KnownT isoiec_9798_2_5_bdkey_P_1)) , ((isoiec_9798_2_5_special_TTP_bdkey_A, ''Text1''), (KnownT isoiec_9798_2_5_special_TTP_bdkey_A_text_1)) , ((isoiec_9798_2_5_special_TTP_bdkey_P, ''Text1''), (KnownT isoiec_9798_2_5_special_TTP_bdkey_P_1)) , ((isoiec_9798_2_6_bdkey_A, ''Text1''), (KnownT isoiec_9798_2_6_bdkey_A_1)) , ((isoiec_9798_2_6_bdkey_B, ''Text1''), (KnownT isoiec_9798_2_6_bdkey_B_text_1)) , ((isoiec_9798_2_6_special_TTP_bdkey_A, ''Text1''), (KnownT isoiec_9798_2_6_special_TTP_bdkey_A_1)) , ((isoiec_9798_2_6_special_TTP_bdkey_B, ''Text1''), (KnownT isoiec_9798_2_6_special_TTP_bdkey_B_text_1)) , ((isoiec_9798_2_1_bdkey_A, ''Text2''), (KnownT isoiec_9798_2_1_bdkey_A_text_1)) , ((isoiec_9798_2_1_bdkey_B, ''Text2''), (KnownT isoiec_9798_2_1_bdkey_B_1)) , ((isoiec_9798_2_2_bdkey_A, ''Text2''), (KnownT isoiec_9798_2_2_bdkey_A_text_2)) , ((isoiec_9798_2_2_bdkey_B, ''Text2''), (KnownT isoiec_9798_2_2_bdkey_B_2)) , ((isoiec_9798_2_3_bdkey_A, ''Text2''), (KnownT isoiec_9798_2_3_bdkey_A_text_1)) , ((isoiec_9798_2_3_bdkey_B, ''Text2''), (KnownT isoiec_9798_2_3_bdkey_B_1)) , ((isoiec_9798_2_4_bdkey_A, ''Text2''), (KnownT isoiec_9798_2_4_bdkey_A_text_2)) , ((isoiec_9798_2_4_bdkey_B, ''Text2''), (KnownT isoiec_9798_2_4_bdkey_B_2)) , ((isoiec_9798_2_5_bdkey_B, ''Text2''), (KnownT isoiec_9798_2_5_bdkey_B_3)) , ((isoiec_9798_2_5_bdkey_P, ''Text2''), (KnownT isoiec_9798_2_5_bdkey_P_text_2)) , ((isoiec_9798_2_5_special_TTP_bdkey_B, ''Text2''), (KnownT isoiec_9798_2_5_special_TTP_bdkey_B_3)) , ((isoiec_9798_2_5_special_TTP_bdkey_P, ''Text2''), (KnownT isoiec_9798_2_5_special_TTP_bdkey_P_text_2)) , ((isoiec_9798_2_6_bdkey_A, ''Text2''), (KnownT isoiec_9798_2_6_bdkey_A_text_2)) , ((isoiec_9798_2_6_bdkey_P, ''Text2''), (KnownT isoiec_9798_2_6_bdkey_P_2)) , ((isoiec_9798_2_6_special_TTP_bdkey_A, ''Text2''), (KnownT isoiec_9798_2_6_special_TTP_bdkey_A_text_2)) , ((isoiec_9798_2_6_special_TTP_bdkey_P, ''Text2''), (KnownT isoiec_9798_2_6_special_TTP_bdkey_P_2)) , ((isoiec_9798_2_2_bdkey_A, ''Text3''), (KnownT isoiec_9798_2_2_bdkey_A_text_2)) , ((isoiec_9798_2_2_bdkey_B, ''Text3''), (KnownT isoiec_9798_2_2_bdkey_B_2)) , ((isoiec_9798_2_3_bdkey_A, ''Text3''), (KnownT isoiec_9798_2_3_bdkey_A_2)) , ((isoiec_9798_2_3_bdkey_B, ''Text3''), (KnownT isoiec_9798_2_3_bdkey_B_text_2)) , ((isoiec_9798_2_4_bdkey_A, ''Text3''), (KnownT isoiec_9798_2_4_bdkey_A_text_2)) , ((isoiec_9798_2_4_bdkey_B, ''Text3''), (KnownT isoiec_9798_2_4_bdkey_B_2)) , ((isoiec_9798_2_5_bdkey_A, ''Text3''), (KnownT isoiec_9798_2_5_bdkey_A_2)) , ((isoiec_9798_2_5_bdkey_P, ''Text3''), (KnownT isoiec_9798_2_5_bdkey_P_text_2)) , ((isoiec_9798_2_5_special_TTP_bdkey_A, ''Text3''), (KnownT isoiec_9798_2_5_special_TTP_bdkey_A_2)) , ((isoiec_9798_2_5_special_TTP_bdkey_P, ''Text3''), (KnownT isoiec_9798_2_5_special_TTP_bdkey_P_text_2)) , ((isoiec_9798_2_6_bdkey_B, ''Text3''), (KnownT isoiec_9798_2_6_bdkey_B_4)) , ((isoiec_9798_2_6_bdkey_P, ''Text3''), (KnownT isoiec_9798_2_6_bdkey_P_text_3)) , ((isoiec_9798_2_6_special_TTP_bdkey_B, ''Text3''), (KnownT isoiec_9798_2_6_special_TTP_bdkey_B_4)) , ((isoiec_9798_2_6_special_TTP_bdkey_P, ''Text3''), (KnownT isoiec_9798_2_6_special_TTP_bdkey_P_text_3)) , ((isoiec_9798_2_3_bdkey_A, ''Text4''), (KnownT isoiec_9798_2_3_bdkey_A_2)) , ((isoiec_9798_2_3_bdkey_B, ''Text4''), (KnownT isoiec_9798_2_3_bdkey_B_text_2)) , ((isoiec_9798_2_4_bdkey_A, ''Text4''), (KnownT isoiec_9798_2_4_bdkey_A_3)) , ((isoiec_9798_2_4_bdkey_B, ''Text4''), (KnownT isoiec_9798_2_4_bdkey_B_text_3)) , ((isoiec_9798_2_5_bdkey_A, ''Text4''), (KnownT isoiec_9798_2_5_bdkey_A_2)) , ((isoiec_9798_2_5_bdkey_P, ''Text4''), (KnownT isoiec_9798_2_5_bdkey_P_text_2)) , ((isoiec_9798_2_5_special_TTP_bdkey_A, ''Text4''), (KnownT isoiec_9798_2_5_special_TTP_bdkey_A_2)) , ((isoiec_9798_2_5_special_TTP_bdkey_P, ''Text4''), (KnownT isoiec_9798_2_5_special_TTP_bdkey_P_text_2)) , ((isoiec_9798_2_6_bdkey_A, ''Text4''), (KnownT isoiec_9798_2_6_bdkey_A_3)) , ((isoiec_9798_2_6_bdkey_P, ''Text4''), (KnownT isoiec_9798_2_6_bdkey_P_text_3)) , ((isoiec_9798_2_6_special_TTP_bdkey_A, ''Text4''), (KnownT isoiec_9798_2_6_special_TTP_bdkey_A_3)) , ((isoiec_9798_2_6_special_TTP_bdkey_P, ''Text4''), (KnownT isoiec_9798_2_6_special_TTP_bdkey_P_text_3)) , ((isoiec_9798_2_4_bdkey_A, ''Text5''), (KnownT isoiec_9798_2_4_bdkey_A_3)) , ((isoiec_9798_2_4_bdkey_B, ''Text5''), (KnownT isoiec_9798_2_4_bdkey_B_text_3)) , ((isoiec_9798_2_5_bdkey_A, ''Text5''), (KnownT isoiec_9798_2_5_bdkey_A_text_3)) , ((isoiec_9798_2_5_bdkey_B, ''Text5''), (KnownT isoiec_9798_2_5_bdkey_B_3)) , ((isoiec_9798_2_5_special_TTP_bdkey_A, ''Text5''), (KnownT isoiec_9798_2_5_special_TTP_bdkey_A_text_3)) , ((isoiec_9798_2_5_special_TTP_bdkey_B, ''Text5''), (KnownT isoiec_9798_2_5_special_TTP_bdkey_B_3)) , ((isoiec_9798_2_6_bdkey_A, ''Text5''), (KnownT isoiec_9798_2_6_bdkey_A_3)) , ((isoiec_9798_2_6_bdkey_P, ''Text5''), (KnownT isoiec_9798_2_6_bdkey_P_text_3)) , ((isoiec_9798_2_6_special_TTP_bdkey_A, ''Text5''), (KnownT isoiec_9798_2_6_special_TTP_bdkey_A_3)) , ((isoiec_9798_2_6_special_TTP_bdkey_P, ''Text5''), (KnownT isoiec_9798_2_6_special_TTP_bdkey_P_text_3)) , ((isoiec_9798_2_5_bdkey_A, ''Text6''), (KnownT isoiec_9798_2_5_bdkey_A_text_3)) , ((isoiec_9798_2_5_bdkey_B, ''Text6''), (KnownT isoiec_9798_2_5_bdkey_B_3)) , ((isoiec_9798_2_5_special_TTP_bdkey_A, ''Text6''), (KnownT isoiec_9798_2_5_special_TTP_bdkey_A_text_3)) , ((isoiec_9798_2_5_special_TTP_bdkey_B, ''Text6''), (KnownT isoiec_9798_2_5_special_TTP_bdkey_B_3)) , ((isoiec_9798_2_6_bdkey_A, ''Text6''), (KnownT isoiec_9798_2_6_bdkey_A_text_4)) , ((isoiec_9798_2_6_bdkey_B, ''Text6''), (KnownT isoiec_9798_2_6_bdkey_B_4)) , ((isoiec_9798_2_6_special_TTP_bdkey_A, ''Text6''), (KnownT isoiec_9798_2_6_special_TTP_bdkey_A_text_4)) , ((isoiec_9798_2_6_special_TTP_bdkey_B, ''Text6''), (KnownT isoiec_9798_2_6_special_TTP_bdkey_B_4)) , ((isoiec_9798_2_5_bdkey_A, ''Text7''), (KnownT isoiec_9798_2_5_bdkey_A_4)) , ((isoiec_9798_2_5_bdkey_B, ''Text7''), (KnownT isoiec_9798_2_5_bdkey_B_text_4)) , ((isoiec_9798_2_5_special_TTP_bdkey_A, ''Text7''), (KnownT isoiec_9798_2_5_special_TTP_bdkey_A_4)) , ((isoiec_9798_2_5_special_TTP_bdkey_B, ''Text7''), (KnownT isoiec_9798_2_5_special_TTP_bdkey_B_text_4)) , ((isoiec_9798_2_6_bdkey_A, ''Text7''), (KnownT isoiec_9798_2_6_bdkey_A_text_4)) , ((isoiec_9798_2_6_bdkey_B, ''Text7''), (KnownT isoiec_9798_2_6_bdkey_B_4)) , ((isoiec_9798_2_6_special_TTP_bdkey_A, ''Text7''), (KnownT isoiec_9798_2_6_special_TTP_bdkey_A_text_4)) , ((isoiec_9798_2_6_special_TTP_bdkey_B, ''Text7''), (KnownT isoiec_9798_2_6_special_TTP_bdkey_B_4)) , ((isoiec_9798_2_5_bdkey_A, ''Text8''), (KnownT isoiec_9798_2_5_bdkey_A_4)) , ((isoiec_9798_2_5_bdkey_B, ''Text8''), (KnownT isoiec_9798_2_5_bdkey_B_text_4)) , ((isoiec_9798_2_5_special_TTP_bdkey_A, ''Text8''), (KnownT isoiec_9798_2_5_special_TTP_bdkey_A_4)) , ((isoiec_9798_2_5_special_TTP_bdkey_B, ''Text8''), (KnownT isoiec_9798_2_5_special_TTP_bdkey_B_text_4)) , ((isoiec_9798_2_6_bdkey_A, ''Text8''), (KnownT isoiec_9798_2_6_bdkey_A_5)) , ((isoiec_9798_2_6_bdkey_B, ''Text8''), (KnownT isoiec_9798_2_6_bdkey_B_text_5)) , ((isoiec_9798_2_6_special_TTP_bdkey_A, ''Text8''), (KnownT isoiec_9798_2_6_special_TTP_bdkey_A_5)) , ((isoiec_9798_2_6_special_TTP_bdkey_B, ''Text8''), (KnownT isoiec_9798_2_6_special_TTP_bdkey_B_text_5)) , ((isoiec_9798_2_6_bdkey_A, ''Text9''), (KnownT isoiec_9798_2_6_bdkey_A_5)) , ((isoiec_9798_2_6_bdkey_B, ''Text9''), (KnownT isoiec_9798_2_6_bdkey_B_text_5)) , ((isoiec_9798_2_6_special_TTP_bdkey_A, ''Text9''), (KnownT isoiec_9798_2_6_special_TTP_bdkey_A_5)) , ((isoiec_9798_2_6_special_TTP_bdkey_B, ''Text9''), (KnownT isoiec_9798_2_6_special_TTP_bdkey_B_text_5)) , ((isoiec_9798_2_5_bdkey_A, ''TokenPA_for_B''), (KnownT isoiec_9798_2_5_bdkey_A_2)) , ((isoiec_9798_2_5_special_TTP_bdkey_A, ''TokenPA_for_B''), (KnownT isoiec_9798_2_5_special_TTP_bdkey_A_2)) , ((isoiec_9798_2_6_bdkey_A, ''TokenPA_for_B''), (KnownT isoiec_9798_2_6_bdkey_A_3)) , ((isoiec_9798_2_6_special_TTP_bdkey_A, ''TokenPA_for_B''), (KnownT isoiec_9798_2_6_special_TTP_bdkey_A_3)) ]" sublocale isoiec_9798_2_bdkey_state < isoiec_9798_2_bdkey_composed_typing_state proof - have "(t,r,s) : approx isoiec_9798_2_bdkey_composed_typing" proof(cases rule: reachable_in_approxI_ext [OF isoiec_9798_2_bdkey_composed_typing.monoTyp, completeness_cases_rule]) case (isoiec_9798_2_1_bdkey_A_text_1_Text1 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_1_bdkey_A_text_1_Text2 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_1_bdkey_B_1_A t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_1_bdkey_B_1_TNA t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_1_enc_1'', s(MV ''TNA'' tid0), s(AV ''B'' tid0), s(MV ''Text1'' tid0) |} ( Kbd ( s(AV ''B'' tid0) ) ( s(MV ''A'' tid0) ) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_1_bdkey_B_1_Text1 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_1_enc_1'', s(MV ''TNA'' tid0), s(AV ''B'' tid0), s(MV ''Text1'' tid0) |} ( Kbd ( s(AV ''B'' tid0) ) ( s(MV ''A'' tid0) ) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_1_bdkey_B_1_Text2 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_2_bdkey_A_1_B t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_2_bdkey_A_1_RB t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_2_bdkey_A_1_Text1 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_2_bdkey_A_text_2_Text2 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_2_bdkey_A_text_2_Text3 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_2_bdkey_B_2_Text2 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_2_enc_2'', LN ''RB'' tid0, s(AV ''B'' tid0), s(MV ''Text2'' tid0) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(AV ''B'' tid0) ) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_2_bdkey_B_2_Text3 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_3_bdkey_A_text_1_Text1 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_3_bdkey_A_text_1_Text2 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_3_bdkey_A_2_TNB t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_3_enc_2'', s(MV ''TNB'' tid0), s(AV ''A'' tid0), s(MV ''Text3'' tid0) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(AV ''B'' tid0) ) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_3_bdkey_A_2_Text3 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_3_enc_2'', s(MV ''TNB'' tid0), s(AV ''A'' tid0), s(MV ''Text3'' tid0) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(AV ''B'' tid0) ) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_3_bdkey_A_2_Text4 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_3_bdkey_B_1_A t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_3_bdkey_B_1_TNA t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_3_enc_1'', s(MV ''TNA'' tid0), s(AV ''B'' tid0), s(MV ''Text1'' tid0) |} ( Kbd ( s(AV ''B'' tid0) ) ( s(MV ''A'' tid0) ) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_3_bdkey_B_1_Text1 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_3_enc_1'', s(MV ''TNA'' tid0), s(AV ''B'' tid0), s(MV ''Text1'' tid0) |} ( Kbd ( s(AV ''B'' tid0) ) ( s(MV ''A'' tid0) ) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_3_bdkey_B_1_Text2 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_3_bdkey_B_text_2_Text3 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_3_bdkey_B_text_2_Text4 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_4_bdkey_A_1_B t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_4_bdkey_A_1_RB t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_4_bdkey_A_1_Text1 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_4_bdkey_A_text_2_Text2 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_4_bdkey_A_text_2_Text3 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_4_bdkey_A_3_Text4 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_4_enc_2'', s(MV ''RB'' tid0), LN ''RA'' tid0, s(MV ''Text4'' tid0) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(MV ''B'' tid0) ) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_4_bdkey_A_3_Text5 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_4_bdkey_B_2_RA t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_4_enc_1'', s(MV ''RA'' tid0), LN ''RB'' tid0, s(AV ''B'' tid0), s(MV ''Text2'' tid0) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(AV ''B'' tid0) ) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_4_bdkey_B_2_Text2 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_4_enc_1'', s(MV ''RA'' tid0), LN ''RB'' tid0, s(AV ''B'' tid0), s(MV ''Text2'' tid0) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(AV ''B'' tid0) ) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_4_bdkey_B_2_Text3 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_4_bdkey_B_text_3_Text4 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_4_bdkey_B_text_3_Text5 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_bdkey_A_2_Kab t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_5_enc_2_1'', LN ''TVPa'' tid0, s(MV ''Kab'' tid0), s(AV ''A'' tid0), s(AV ''B'' tid0), s(MV ''Text3'' tid0) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(AV ''P'' tid0) ) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_5_bdkey_A_2_Text3 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_5_enc_2_1'', LN ''TVPa'' tid0, s(MV ''Kab'' tid0), s(AV ''A'' tid0), s(AV ''B'' tid0), s(MV ''Text3'' tid0) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(AV ''P'' tid0) ) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_5_bdkey_A_2_Text4 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_bdkey_A_2_TokenPA_for_B t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_bdkey_A_text_3_Text5 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_bdkey_A_text_3_Text6 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_bdkey_A_4_TNb t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_5_enc_4'', s(MV ''TNb'' tid0), s(AV ''A'' tid0), s(MV ''Text7'' tid0) |} ( s(MV ''Kab'' tid0) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_5_bdkey_A_4_Text7 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_5_enc_4'', s(MV ''TNb'' tid0), s(AV ''A'' tid0), s(MV ''Text7'' tid0) |} ( s(MV ''Kab'' tid0) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_5_bdkey_A_4_Text8 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_bdkey_B_3_A t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_bdkey_B_3_Kab t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_5_enc_2_2'', s(MV ''TNp'' tid0), s(MV ''Kab'' tid0), s(MV ''A'' tid0), s(AV ''B'' tid0), s(MV ''Text2'' tid0) |} ( Kbd ( s(AV ''B'' tid0) ) ( s(MV ''P'' tid0) ) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_5_bdkey_B_3_P t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_bdkey_B_3_TNa t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_5_enc_3'', s(MV ''TNa'' tid0), s(AV ''B'' tid0), s(MV ''Text5'' tid0) |} ( s(MV ''Kab'' tid0) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_5_bdkey_B_3_TNp t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_5_enc_2_2'', s(MV ''TNp'' tid0), s(MV ''Kab'' tid0), s(MV ''A'' tid0), s(AV ''B'' tid0), s(MV ''Text2'' tid0) |} ( Kbd ( s(AV ''B'' tid0) ) ( s(MV ''P'' tid0) ) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_5_bdkey_B_3_Text2 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_5_enc_2_2'', s(MV ''TNp'' tid0), s(MV ''Kab'' tid0), s(MV ''A'' tid0), s(AV ''B'' tid0), s(MV ''Text2'' tid0) |} ( Kbd ( s(AV ''B'' tid0) ) ( s(MV ''P'' tid0) ) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_5_bdkey_B_3_Text5 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_5_enc_3'', s(MV ''TNa'' tid0), s(AV ''B'' tid0), s(MV ''Text5'' tid0) |} ( s(MV ''Kab'' tid0) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_5_bdkey_B_3_Text6 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_bdkey_B_text_4_Text7 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_bdkey_B_text_4_Text8 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_bdkey_P_1_A t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_bdkey_P_1_B t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_bdkey_P_1_TVPa t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_bdkey_P_1_Text1 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_bdkey_P_text_2_Text2 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_bdkey_P_text_2_Text3 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_bdkey_P_text_2_Text4 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_bdkey_A_1_B t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_bdkey_A_1_Rb t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_bdkey_A_1_Text1 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_bdkey_A_3_Kab t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_6_enc_3_1'', LN ''Ra'' tid0, s(MV ''Kab'' tid0), s(AV ''A'' tid0), s(MV ''B'' tid0), s(MV ''Text4'' tid0) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(AV ''P'' tid0) ) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_6_bdkey_A_3_Text4 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_6_enc_3_1'', LN ''Ra'' tid0, s(MV ''Kab'' tid0), s(AV ''A'' tid0), s(MV ''B'' tid0), s(MV ''Text4'' tid0) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(AV ''P'' tid0) ) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_6_bdkey_A_3_Text5 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_bdkey_A_3_TokenPA_for_B t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_bdkey_A_text_4_Text6 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_bdkey_A_text_4_Text7 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_bdkey_A_5_Text8 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_6_enc_5'', s(MV ''Rb'' tid0), LN ''Rpa'' tid0, s(MV ''Text8'' tid0) |} ( s(MV ''Kab'' tid0) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_6_bdkey_A_5_Text9 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_bdkey_B_4_Kab t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_6_enc_3_2'', LN ''Rb'' tid0, s(MV ''Kab'' tid0), s(AV ''A'' tid0), s(AV ''B'' tid0), s(MV ''Text3'' tid0) |} ( Kbd ( s(AV ''B'' tid0) ) ( s(MV ''P'' tid0) ) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_6_bdkey_B_4_P t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_bdkey_B_4_Rpa t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_6_enc_4'', s(MV ''Rpa'' tid0), LN ''Rb'' tid0, s(MV ''Text6'' tid0) |} ( s(MV ''Kab'' tid0) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_6_bdkey_B_4_Text3 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_6_enc_3_2'', LN ''Rb'' tid0, s(MV ''Kab'' tid0), s(AV ''A'' tid0), s(AV ''B'' tid0), s(MV ''Text3'' tid0) |} ( Kbd ( s(AV ''B'' tid0) ) ( s(MV ''P'' tid0) ) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_6_bdkey_B_4_Text6 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_6_enc_4'', s(MV ''Rpa'' tid0), LN ''Rb'' tid0, s(MV ''Text6'' tid0) |} ( s(MV ''Kab'' tid0) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_6_bdkey_B_4_Text7 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_bdkey_B_text_5_Text8 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_bdkey_B_text_5_Text9 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_bdkey_P_2_A t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_bdkey_P_2_B t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_bdkey_P_2_Ra t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_bdkey_P_2_Rb t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_bdkey_P_2_Text2 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_bdkey_P_text_3_Text3 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_bdkey_P_text_3_Text4 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_bdkey_P_text_3_Text5 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_special_TTP_bdkey_A_2_Kab t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_5_special_TTP_enc_2_1'', LN ''TVPa'' tid0, s(MV ''Kab'' tid0), s(AV ''B'' tid0), s(MV ''Text3'' tid0) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(AV ''P'' tid0) ) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_5_special_TTP_bdkey_A_2_Text3 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_5_special_TTP_enc_2_1'', LN ''TVPa'' tid0, s(MV ''Kab'' tid0), s(AV ''B'' tid0), s(MV ''Text3'' tid0) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(AV ''P'' tid0) ) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_5_special_TTP_bdkey_A_2_Text4 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_special_TTP_bdkey_A_2_TokenPA_for_B t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_special_TTP_bdkey_A_text_3_Text5 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_special_TTP_bdkey_A_text_3_Text6 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_special_TTP_bdkey_A_4_TNb t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_5_special_TTP_enc_4'', s(MV ''TNb'' tid0), s(AV ''A'' tid0), s(MV ''Text7'' tid0) |} ( s(MV ''Kab'' tid0) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_5_special_TTP_bdkey_A_4_Text7 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_5_special_TTP_enc_4'', s(MV ''TNb'' tid0), s(AV ''A'' tid0), s(MV ''Text7'' tid0) |} ( s(MV ''Kab'' tid0) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_5_special_TTP_bdkey_A_4_Text8 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_special_TTP_bdkey_B_3_A t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_special_TTP_bdkey_B_3_Kab t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_5_special_TTP_enc_2_2'', s(MV ''TNp'' tid0), s(MV ''Kab'' tid0), s(MV ''A'' tid0), s(MV ''Text2'' tid0) |} ( Kbd ( s(AV ''B'' tid0) ) ( s(MV ''P'' tid0) ) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_5_special_TTP_bdkey_B_3_P t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_special_TTP_bdkey_B_3_TNa t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_5_special_TTP_enc_3'', s(MV ''TNa'' tid0), s(AV ''B'' tid0), s(MV ''Text5'' tid0) |} ( s(MV ''Kab'' tid0) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_5_special_TTP_bdkey_B_3_TNp t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_5_special_TTP_enc_2_2'', s(MV ''TNp'' tid0), s(MV ''Kab'' tid0), s(MV ''A'' tid0), s(MV ''Text2'' tid0) |} ( Kbd ( s(AV ''B'' tid0) ) ( s(MV ''P'' tid0) ) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_5_special_TTP_bdkey_B_3_Text2 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_5_special_TTP_enc_2_2'', s(MV ''TNp'' tid0), s(MV ''Kab'' tid0), s(MV ''A'' tid0), s(MV ''Text2'' tid0) |} ( Kbd ( s(AV ''B'' tid0) ) ( s(MV ''P'' tid0) ) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_5_special_TTP_bdkey_B_3_Text5 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_5_special_TTP_enc_3'', s(MV ''TNa'' tid0), s(AV ''B'' tid0), s(MV ''Text5'' tid0) |} ( s(MV ''Kab'' tid0) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_5_special_TTP_bdkey_B_3_Text6 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_special_TTP_bdkey_B_text_4_Text7 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_special_TTP_bdkey_B_text_4_Text8 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_special_TTP_bdkey_P_1_A t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_special_TTP_bdkey_P_1_B t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_special_TTP_bdkey_P_1_TVPa t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_special_TTP_bdkey_P_1_Text1 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_special_TTP_bdkey_P_text_2_Text2 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_special_TTP_bdkey_P_text_2_Text3 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_5_special_TTP_bdkey_P_text_2_Text4 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_special_TTP_bdkey_A_1_B t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_special_TTP_bdkey_A_1_Rb t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_special_TTP_bdkey_A_1_Text1 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_special_TTP_bdkey_A_3_Kab t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_6_special_TTP_enc_3_1'', LN ''Ra'' tid0, s(MV ''Kab'' tid0), s(MV ''B'' tid0), s(MV ''Text4'' tid0) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(AV ''P'' tid0) ) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_6_special_TTP_bdkey_A_3_Text4 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_6_special_TTP_enc_3_1'', LN ''Ra'' tid0, s(MV ''Kab'' tid0), s(MV ''B'' tid0), s(MV ''Text4'' tid0) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(AV ''P'' tid0) ) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_6_special_TTP_bdkey_A_3_Text5 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_special_TTP_bdkey_A_3_TokenPA_for_B t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_special_TTP_bdkey_A_text_4_Text6 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_special_TTP_bdkey_A_text_4_Text7 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_special_TTP_bdkey_A_5_Text8 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_6_special_TTP_enc_5'', s(MV ''Rb'' tid0), LN ''Rpa'' tid0, s(MV ''Text8'' tid0) |} ( s(MV ''Kab'' tid0) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_6_special_TTP_bdkey_A_5_Text9 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_special_TTP_bdkey_B_4_Kab t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_6_special_TTP_enc_3_2'', LN ''Rb'' tid0, s(MV ''Kab'' tid0), s(AV ''A'' tid0), s(MV ''Text3'' tid0) |} ( Kbd ( s(AV ''B'' tid0) ) ( s(MV ''P'' tid0) ) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_6_special_TTP_bdkey_B_4_P t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_special_TTP_bdkey_B_4_Rpa t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_6_special_TTP_enc_4'', s(MV ''Rpa'' tid0), LN ''Rb'' tid0, s(MV ''Text6'' tid0) |} ( s(MV ''Kab'' tid0) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_6_special_TTP_bdkey_B_4_Text3 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_6_special_TTP_enc_3_2'', LN ''Rb'' tid0, s(MV ''Kab'' tid0), s(AV ''A'' tid0), s(MV ''Text3'' tid0) |} ( Kbd ( s(AV ''B'' tid0) ) ( s(MV ''P'' tid0) ) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_6_special_TTP_bdkey_B_4_Text6 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts proof(sources! " Enc {| LC ''isoiec_9798_2_6_special_TTP_enc_4'', s(MV ''Rpa'' tid0), LN ''Rb'' tid0, s(MV ''Text6'' tid0) |} ( s(MV ''Kab'' tid0) ) ") qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)? next case (isoiec_9798_2_6_special_TTP_bdkey_B_4_Text7 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_special_TTP_bdkey_B_text_5_Text8 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_special_TTP_bdkey_B_text_5_Text9 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_special_TTP_bdkey_P_2_A t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_special_TTP_bdkey_P_2_B t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_special_TTP_bdkey_P_2_Ra t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_special_TTP_bdkey_P_2_Rb t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_special_TTP_bdkey_P_2_Text2 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_special_TTP_bdkey_P_text_3_Text3 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_special_TTP_bdkey_P_text_3_Text4 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) next case (isoiec_9798_2_6_special_TTP_bdkey_P_text_3_Text5 t r s tid0) note facts = this then interpret state: isoiec_9798_2_bdkey_composed_typing_state t r s by unfold_locales auto show ?case using facts by (fastforce intro: event_predOrdI split: if_splits) qed thus "isoiec_9798_2_bdkey_composed_typing_state t r s" by unfold_locales auto qed text{* Prove secrecy of long-term keys. *} context isoiec_9798_2_bdkey_state begin (* This rule is unsafe in general, but OK here, as we are only reasoning about static compromise. *) lemma static_longterm_key_reveal[dest!]: "predOrd t (LKR a) e ==> RLKR a : reveals t" by (auto intro: compr_predOrdI) lemma longterm_private_key_secrecy: assumes facts: "SK m : knows t" "RLKR m ~: reveals t" shows "False" using facts by (sources "SK m") lemma longterm_sym_ud_key_secrecy: assumes facts: "K m1 m2 : knows t" "RLKR m1 ~: reveals t" "RLKR m2 ~: reveals t" shows "False" using facts by (sources "K m1 m2") lemma longterm_sym_bd_key_secrecy: assumes facts: "Kbd m1 m2 : knows t" "RLKR m1 ~: reveals t" "RLKR m2 ~: reveals t" "m1 : Agent" "m2 : Agent" shows "False" proof - from facts have "KShr (agents {m1, m2}) : knows t" by (auto simp: Kbd_def) thus ?thesis using facts proof (sources "KShr (agents {m1, m2})") qed (auto simp: agents_def Agent_def) qed lemmas ltk_secrecy = longterm_sym_ud_key_secrecy longterm_sym_ud_key_secrecy[OF in_knows_predOrd1] longterm_sym_bd_key_secrecy longterm_sym_bd_key_secrecy[OF in_knows_predOrd1] longterm_private_key_secrecy longterm_private_key_secrecy[OF in_knows_predOrd1] end lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_1_bdkey_B_non_injective_agreement: assumes facts: "roleMap r tid0 = Some isoiec_9798_2_1_bdkey_B" "RLKR(s(AV ''B'' tid0)) ~: reveals t" "RLKR(s(MV ''A'' tid0)) ~: reveals t" "( tid0, isoiec_9798_2_1_bdkey_B_1 ) : steps t" shows "(? tid1. roleMap r tid1 = Some isoiec_9798_2_1_bdkey_A & ( tid1, isoiec_9798_2_1_bdkey_A_1 ) : steps t & {| s(AV ''A'' tid1), s(AV ''B'' tid1), LN ''TNA'' tid1, s(MV ''Text1'' tid1) |} = {| s(MV ''A'' tid0), s(AV ''B'' tid0), s(MV ''TNA'' tid0), s(MV ''Text1'' tid0) |})" proof - note_prefix_closed facts = facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_1_enc_1'', s(MV ''TNA'' tid0), s(AV ''B'' tid0), s(MV ''Text1'' tid0) |} ( Kbd ( s(AV ''B'' tid0) ) ( s(MV ''A'' tid0) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_1_bdkey_A_1_enc tid1) note_unified facts = this facts thus ?thesis by (fastforce intro: event_predOrdI split: if_splits) qed (insert facts, fastforce+)? qed lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_2_bdkey_B_injective_agreement: "let prems = (% tid0. roleMap r tid0 = Some isoiec_9798_2_2_bdkey_B & RLKR(s(AV ''A'' tid0)) ~: reveals t & RLKR(s(AV ''B'' tid0)) ~: reveals t & ( tid0, isoiec_9798_2_2_bdkey_B_2 ) : steps t); concs = (% tid0 tid1. roleMap r tid1 = Some isoiec_9798_2_2_bdkey_A & ( tid1, isoiec_9798_2_2_bdkey_A_2 ) : steps t & {| s(AV ''A'' tid1), s(MV ''B'' tid1), s(MV ''RB'' tid1), s(MV ''Text2'' tid1) |} = {| s(AV ''A'' tid0), s(AV ''B'' tid0), LN ''RB'' tid0, s(MV ''Text2'' tid0) |}) in ? f. inj_on f (Collect prems) & (! i. prems i --> concs i (f i))" (is "let prems = ?prems; concs = ?concs in ?P prems concs") proof - { fix tid0 tid1 assume facts: "?prems tid0" have " ? tid1. ?concs tid0 tid1" proof - note_unified facts = facts note_prefix_closed facts = facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_2_enc_2'', LN ''RB'' tid0, s(AV ''B'' tid0), s(MV ''Text2'' tid0) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(AV ''B'' tid0) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_2_bdkey_A_2_enc tid1) note_unified facts = this facts thus ?thesis by (fastforce intro: event_predOrdI split: if_splits) qed (insert facts, fastforce+)? qed } note niagree = this { fix i1 i2 j assume "?concs i1 j & ?concs i2 j" note_unified facts = this have "i1 = i2" using facts by simp } note conc_inj = this show ?thesis by (fast intro!: iagree_to_niagree elim!: niagree conc_inj) qed lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_3_bdkey_A_non_injective_agreement: assumes facts: "roleMap r tid0 = Some isoiec_9798_2_3_bdkey_A" "RLKR(s(AV ''A'' tid0)) ~: reveals t" "RLKR(s(AV ''B'' tid0)) ~: reveals t" "( tid0, isoiec_9798_2_3_bdkey_A_2 ) : steps t" shows "(? tid1. roleMap r tid1 = Some isoiec_9798_2_3_bdkey_B & ( tid1, isoiec_9798_2_3_bdkey_B_2 ) : steps t & {| s(MV ''A'' tid1), s(AV ''B'' tid1), LN ''TNB'' tid1, s(MV ''Text3'' tid1) |} = {| s(AV ''A'' tid0), s(AV ''B'' tid0), s(MV ''TNB'' tid0), s(MV ''Text3'' tid0) |})" proof - note_prefix_closed facts = facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_3_enc_2'', s(MV ''TNB'' tid0), s(AV ''A'' tid0), s(MV ''Text3'' tid0) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(AV ''B'' tid0) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_3_bdkey_B_2_enc tid1) note_unified facts = this facts thus ?thesis by (fastforce intro: event_predOrdI split: if_splits) qed (insert facts, fastforce+)? qed lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_3_bdkey_B_non_injective_agreement: assumes facts: "roleMap r tid0 = Some isoiec_9798_2_3_bdkey_B" "RLKR(s(AV ''B'' tid0)) ~: reveals t" "RLKR(s(MV ''A'' tid0)) ~: reveals t" "( tid0, isoiec_9798_2_3_bdkey_B_1 ) : steps t" shows "(? tid1. roleMap r tid1 = Some isoiec_9798_2_3_bdkey_A & ( tid1, isoiec_9798_2_3_bdkey_A_1 ) : steps t & {| s(AV ''A'' tid1), s(AV ''B'' tid1), LN ''TNA'' tid1, s(MV ''Text1'' tid1) |} = {| s(MV ''A'' tid0), s(AV ''B'' tid0), s(MV ''TNA'' tid0), s(MV ''Text1'' tid0) |})" proof - note_prefix_closed facts = facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_3_enc_1'', s(MV ''TNA'' tid0), s(AV ''B'' tid0), s(MV ''Text1'' tid0) |} ( Kbd ( s(AV ''B'' tid0) ) ( s(MV ''A'' tid0) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_3_bdkey_A_1_enc tid1) note_unified facts = this facts thus ?thesis by (fastforce intro: event_predOrdI split: if_splits) qed (insert facts, fastforce+)? qed lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_4_bdkey_A_injective_agreement: "let prems = (% tid0. roleMap r tid0 = Some isoiec_9798_2_4_bdkey_A & RLKR(s(AV ''A'' tid0)) ~: reveals t & RLKR(s(MV ''B'' tid0)) ~: reveals t & ( tid0, isoiec_9798_2_4_bdkey_A_3 ) : steps t); concs = (% tid0 tid1. roleMap r tid1 = Some isoiec_9798_2_4_bdkey_B & ( tid1, isoiec_9798_2_4_bdkey_B_3 ) : steps t & {| s(AV ''A'' tid1), s(AV ''B'' tid1), s(MV ''RA'' tid1), LN ''RB'' tid1, s(MV ''Text2'' tid1), s(MV ''Text4'' tid1) |} = {| s(AV ''A'' tid0), s(MV ''B'' tid0), LN ''RA'' tid0, s(MV ''RB'' tid0), s(MV ''Text2'' tid0), s(MV ''Text4'' tid0) |}) in ? f. inj_on f (Collect prems) & (! i. prems i --> concs i (f i))" (is "let prems = ?prems; concs = ?concs in ?P prems concs") proof - { fix tid0 tid1 assume facts: "?prems tid0" have " ? tid1. ?concs tid0 tid1" proof - note_unified facts = facts note_prefix_closed facts = facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_4_enc_2'', s(MV ''RB'' tid0), LN ''RA'' tid0, s(MV ''Text4'' tid0) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(MV ''B'' tid0) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_4_bdkey_B_3_enc tid1) note_unified facts = this facts hence "Kbd ( s(AV ''A'' tid1) ) ( s(AV ''B'' tid1) ) = Kbd ( s(AV ''A'' tid0) ) ( s(MV ''B'' tid0) )" by simp note facts = this facts thus ?thesis proof(cases rule: Kbd_cases) case noswap note_unified facts = this facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_4_enc_1'', LN ''RA'' tid0, LN ''RB'' tid1, s(AV ''B'' tid1), s(MV ''Text2'' tid1) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(AV ''B'' tid1) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_4_bdkey_A_2_enc tid2) note_unified facts = this facts thus ?thesis by (fastforce intro: event_predOrdI split: if_splits) qed (insert facts, fastforce+)? next case swapped note_unified facts = this facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_4_enc_1'', LN ''RA'' tid0, LN ''RB'' tid1, s(AV ''A'' tid0), s(MV ''Text2'' tid1) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(AV ''A'' tid1) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_4_bdkey_A_2_enc tid2) note_unified facts = this facts thus ?thesis by (fastforce intro: event_predOrdI split: if_splits) qed (insert facts, fastforce+)? qed (fastforce+)? qed (insert facts, fastforce+)? qed } note niagree = this { fix i1 i2 j assume "?concs i1 j & ?concs i2 j" note_unified facts = this have "i1 = i2" using facts by simp } note conc_inj = this show ?thesis by (fast intro!: iagree_to_niagree elim!: niagree conc_inj) qed lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_4_bdkey_B_injective_agreement: "let prems = (% tid0. roleMap r tid0 = Some isoiec_9798_2_4_bdkey_B & RLKR(s(AV ''A'' tid0)) ~: reveals t & RLKR(s(AV ''B'' tid0)) ~: reveals t & ( tid0, isoiec_9798_2_4_bdkey_B_2 ) : steps t); concs = (% tid0 tid1. roleMap r tid1 = Some isoiec_9798_2_4_bdkey_A & ( tid1, isoiec_9798_2_4_bdkey_A_2 ) : steps t & {| s(AV ''A'' tid1), s(MV ''B'' tid1), LN ''RA'' tid1, s(MV ''RB'' tid1), s(MV ''Text2'' tid1) |} = {| s(AV ''A'' tid0), s(AV ''B'' tid0), s(MV ''RA'' tid0), LN ''RB'' tid0, s(MV ''Text2'' tid0) |}) in ? f. inj_on f (Collect prems) & (! i. prems i --> concs i (f i))" (is "let prems = ?prems; concs = ?concs in ?P prems concs") proof - { fix tid0 tid1 assume facts: "?prems tid0" have " ? tid1. ?concs tid0 tid1" proof - note_unified facts = facts note_prefix_closed facts = facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_4_enc_1'', s(MV ''RA'' tid0), LN ''RB'' tid0, s(AV ''B'' tid0), s(MV ''Text2'' tid0) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(AV ''B'' tid0) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_4_bdkey_A_2_enc tid1) note_unified facts = this facts thus ?thesis by (fastforce intro: event_predOrdI split: if_splits) qed (insert facts, fastforce+)? qed } note niagree = this { fix i1 i2 j assume "?concs i1 j & ?concs i2 j" note_unified facts = this have "i1 = i2" using facts by simp } note conc_inj = this show ?thesis by (fast intro!: iagree_to_niagree elim!: niagree conc_inj) qed lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_5_bdkey_P_secret_Kab: assumes facts: "roleMap r tid0 = Some isoiec_9798_2_5_bdkey_P" "RLKR(s(AV ''P'' tid0)) ~: reveals t" "RLKR(s(MV ''A'' tid0)) ~: reveals t" "RLKR(s(MV ''B'' tid0)) ~: reveals t" "LN ''Kab'' tid0 : knows t" shows "False" using facts proof(sources! " LN ''Kab'' tid0 ") case isoiec_9798_2_5_bdkey_P_2_Kab note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case isoiec_9798_2_5_bdkey_P_2_Kab_1 note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) qed (insert facts, fastforce+)? lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_5_bdkey_A_secret_Kab: assumes facts: "roleMap r tid0 = Some isoiec_9798_2_5_bdkey_A" "RLKR(s(AV ''A'' tid0)) ~: reveals t" "RLKR(s(AV ''B'' tid0)) ~: reveals t" "RLKR(s(AV ''P'' tid0)) ~: reveals t" "( tid0, isoiec_9798_2_5_bdkey_A_2 ) : steps t" "s(MV ''Kab'' tid0) : knows t" shows "False" proof - note_prefix_closed facts = facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_5_enc_2_1'', LN ''TVPa'' tid0, s(MV ''Kab'' tid0), s(AV ''A'' tid0), s(AV ''B'' tid0), s(MV ''Text3'' tid0) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(AV ''P'' tid0) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_5_bdkey_P_2_enc tid1) note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_5_bdkey_P_secret_Kab intro: event_predOrdI) qed (insert facts, fastforce+)? qed lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_5_bdkey_B_secret_Kab: assumes facts: "roleMap r tid0 = Some isoiec_9798_2_5_bdkey_B" "RLKR(s(AV ''B'' tid0)) ~: reveals t" "RLKR(s(MV ''A'' tid0)) ~: reveals t" "RLKR(s(MV ''P'' tid0)) ~: reveals t" "( tid0, isoiec_9798_2_5_bdkey_B_3 ) : steps t" "s(MV ''Kab'' tid0) : knows t" shows "False" proof - note_prefix_closed facts = facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_5_enc_2_2'', s(MV ''TNp'' tid0), s(MV ''Kab'' tid0), s(MV ''A'' tid0), s(AV ''B'' tid0), s(MV ''Text2'' tid0) |} ( Kbd ( s(AV ''B'' tid0) ) ( s(MV ''P'' tid0) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_5_bdkey_P_2_enc_1 tid1) note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_5_bdkey_P_secret_Kab intro: event_predOrdI) qed (insert facts, fastforce+)? qed lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_5_bdkey_A_injective_agreement_B: "let prems = (% tid0. roleMap r tid0 = Some isoiec_9798_2_5_bdkey_A & RLKR(s(AV ''A'' tid0)) ~: reveals t & RLKR(s(AV ''B'' tid0)) ~: reveals t & RLKR(s(AV ''P'' tid0)) ~: reveals t & ( tid0, isoiec_9798_2_5_bdkey_A_4 ) : steps t); concs = (% tid0 tid1. roleMap r tid1 = Some isoiec_9798_2_5_bdkey_B & ( tid1, isoiec_9798_2_5_bdkey_B_4 ) : steps t & {| s(MV ''A'' tid1), s(AV ''B'' tid1), s(MV ''P'' tid1), s(MV ''Kab'' tid1), s(MV ''TNa'' tid1), s(MV ''Text5'' tid1), LN ''TNb'' tid1, s(MV ''Text7'' tid1) |} = {| s(AV ''A'' tid0), s(AV ''B'' tid0), s(AV ''P'' tid0), s(MV ''Kab'' tid0), LN ''TNa'' tid0, s(MV ''Text5'' tid0), s(MV ''TNb'' tid0), s(MV ''Text7'' tid0) |}) in ? f. inj_on f (Collect prems) & (! i. prems i --> concs i (f i))" (is "let prems = ?prems; concs = ?concs in ?P prems concs") proof - { fix tid0 tid1 assume facts: "?prems tid0" have " ? tid1. ?concs tid0 tid1" proof - note_unified facts = facts note_prefix_closed facts = facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_5_enc_2_1'', LN ''TVPa'' tid0, s(MV ''Kab'' tid0), s(AV ''A'' tid0), s(AV ''B'' tid0), s(MV ''Text3'' tid0) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(AV ''P'' tid0) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_5_bdkey_P_2_enc tid1) note_unified facts = this facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_5_enc_4'', s(MV ''TNb'' tid0), s(AV ''A'' tid0), s(MV ''Text7'' tid0) |} ( LN ''Kab'' tid1 ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_5_bdkey_P_secret_Kab intro: event_predOrdI) next case (isoiec_9798_2_5_bdkey_B_4_enc tid2) note_unified facts = this facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_5_enc_2_2'', s(MV ''TNp'' tid2), LN ''Kab'' tid1, s(AV ''A'' tid0), s(AV ''B'' tid2), s(MV ''Text2'' tid2) |} ( Kbd ( s(AV ''B'' tid2) ) ( s(MV ''P'' tid2) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_5_bdkey_P_secret_Kab intro: event_predOrdI) next case (isoiec_9798_2_5_bdkey_P_2_enc_1 tid3) note_unified facts = this facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_5_enc_3'', s(MV ''TNa'' tid2), s(AV ''B'' tid0), s(MV ''Text5'' tid2) |} ( LN ''Kab'' tid1 ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_5_bdkey_P_secret_Kab intro: event_predOrdI) next case (isoiec_9798_2_5_bdkey_A_3_enc tid3) note_unified facts = this facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_5_enc_2_1'', LN ''TVPa'' tid3, LN ''Kab'' tid1, s(AV ''A'' tid3), s(AV ''B'' tid0), s(MV ''Text3'' tid3) |} ( Kbd ( s(AV ''A'' tid3) ) ( s(AV ''P'' tid3) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_5_bdkey_P_secret_Kab intro: event_predOrdI) next case (isoiec_9798_2_5_bdkey_P_2_enc tid4) note_unified facts = this facts thus ?thesis by (fastforce intro: event_predOrdI split: if_splits) qed (insert facts, fastforce+)? qed (insert facts, fastforce+)? qed (insert facts, fastforce+)? qed (insert facts, fastforce+)? qed (insert facts, fastforce+)? qed } note niagree = this { fix i1 i2 j assume "?concs i1 j & ?concs i2 j" note_unified facts = this have "i1 = i2" using facts by simp } note conc_inj = this show ?thesis by (fast intro!: iagree_to_niagree elim!: niagree conc_inj) qed lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_5_bdkey_B_non_injective_agreement_A: assumes facts: "roleMap r tid0 = Some isoiec_9798_2_5_bdkey_B" "RLKR(s(AV ''B'' tid0)) ~: reveals t" "RLKR(s(MV ''A'' tid0)) ~: reveals t" "RLKR(s(MV ''P'' tid0)) ~: reveals t" "( tid0, isoiec_9798_2_5_bdkey_B_3 ) : steps t" shows "(? tid1. roleMap r tid1 = Some isoiec_9798_2_5_bdkey_A & ( tid1, isoiec_9798_2_5_bdkey_A_3 ) : steps t & {| s(AV ''A'' tid1), s(AV ''B'' tid1), s(AV ''P'' tid1), s(MV ''Kab'' tid1), LN ''TNa'' tid1, s(MV ''Text5'' tid1) |} = {| s(MV ''A'' tid0), s(AV ''B'' tid0), s(MV ''P'' tid0), s(MV ''Kab'' tid0), s(MV ''TNa'' tid0), s(MV ''Text5'' tid0) |})" proof - note_prefix_closed facts = facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_5_enc_2_2'', s(MV ''TNp'' tid0), s(MV ''Kab'' tid0), s(MV ''A'' tid0), s(AV ''B'' tid0), s(MV ''Text2'' tid0) |} ( Kbd ( s(AV ''B'' tid0) ) ( s(MV ''P'' tid0) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_5_bdkey_P_2_enc_1 tid1) note_unified facts = this facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_5_enc_3'', s(MV ''TNa'' tid0), s(AV ''B'' tid0), s(MV ''Text5'' tid0) |} ( LN ''Kab'' tid1 ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_5_bdkey_P_secret_Kab intro: event_predOrdI) next case (isoiec_9798_2_5_bdkey_A_3_enc tid2) note_unified facts = this facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_5_enc_2_1'', LN ''TVPa'' tid2, LN ''Kab'' tid1, s(AV ''A'' tid2), s(AV ''B'' tid0), s(MV ''Text3'' tid2) |} ( Kbd ( s(AV ''A'' tid2) ) ( s(AV ''P'' tid2) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_5_bdkey_P_secret_Kab intro: event_predOrdI) next case (isoiec_9798_2_5_bdkey_P_2_enc tid3) note_unified facts = this facts thus ?thesis by (fastforce intro: event_predOrdI split: if_splits) qed (insert facts, fastforce+)? qed (insert facts, fastforce+)? qed (insert facts, fastforce+)? qed lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_5_bdkey_A_injective_agreement_P: "let prems = (% tid0. roleMap r tid0 = Some isoiec_9798_2_5_bdkey_A & RLKR(s(AV ''A'' tid0)) ~: reveals t & RLKR(s(AV ''B'' tid0)) ~: reveals t & RLKR(s(AV ''P'' tid0)) ~: reveals t & ( tid0, isoiec_9798_2_5_bdkey_A_2 ) : steps t); concs = (% tid0 tid1. roleMap r tid1 = Some isoiec_9798_2_5_bdkey_P & ( tid1, isoiec_9798_2_5_bdkey_P_2 ) : steps t & {| s(MV ''A'' tid1), s(MV ''B'' tid1), s(AV ''P'' tid1), LN ''Kab'' tid1, s(MV ''TVPa'' tid1), s(MV ''Text3'' tid1) |} = {| s(AV ''A'' tid0), s(AV ''B'' tid0), s(AV ''P'' tid0), s(MV ''Kab'' tid0), LN ''TVPa'' tid0, s(MV ''Text3'' tid0) |}) in ? f. inj_on f (Collect prems) & (! i. prems i --> concs i (f i))" (is "let prems = ?prems; concs = ?concs in ?P prems concs") proof - { fix tid0 tid1 assume facts: "?prems tid0" have " ? tid1. ?concs tid0 tid1" proof - note_unified facts = facts note_prefix_closed facts = facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_5_enc_2_1'', LN ''TVPa'' tid0, s(MV ''Kab'' tid0), s(AV ''A'' tid0), s(AV ''B'' tid0), s(MV ''Text3'' tid0) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(AV ''P'' tid0) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_5_bdkey_P_2_enc tid1) note_unified facts = this facts thus ?thesis by (fastforce intro: event_predOrdI split: if_splits) qed (insert facts, fastforce+)? qed } note niagree = this { fix i1 i2 j assume "?concs i1 j & ?concs i2 j" note_unified facts = this have "i1 = i2" using facts by simp } note conc_inj = this show ?thesis by (fast intro!: iagree_to_niagree elim!: niagree conc_inj) qed lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_5_bdkey_B_non_injective_agreement_P: assumes facts: "roleMap r tid0 = Some isoiec_9798_2_5_bdkey_B" "RLKR(s(AV ''B'' tid0)) ~: reveals t" "RLKR(s(MV ''A'' tid0)) ~: reveals t" "RLKR(s(MV ''P'' tid0)) ~: reveals t" "( tid0, isoiec_9798_2_5_bdkey_B_3 ) : steps t" shows "(? tid1. roleMap r tid1 = Some isoiec_9798_2_5_bdkey_P & ( tid1, isoiec_9798_2_5_bdkey_P_2 ) : steps t & {| s(MV ''A'' tid1), s(MV ''B'' tid1), s(AV ''P'' tid1), LN ''Kab'' tid1, LN ''TNp'' tid1, s(MV ''Text2'' tid1) |} = {| s(MV ''A'' tid0), s(AV ''B'' tid0), s(MV ''P'' tid0), s(MV ''Kab'' tid0), s(MV ''TNp'' tid0), s(MV ''Text2'' tid0) |})" proof - note_prefix_closed facts = facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_5_enc_2_2'', s(MV ''TNp'' tid0), s(MV ''Kab'' tid0), s(MV ''A'' tid0), s(AV ''B'' tid0), s(MV ''Text2'' tid0) |} ( Kbd ( s(AV ''B'' tid0) ) ( s(MV ''P'' tid0) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_5_bdkey_P_2_enc_1 tid1) note_unified facts = this facts thus ?thesis by (fastforce intro: event_predOrdI split: if_splits) qed (insert facts, fastforce+)? qed lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_6_bdkey_P_secret_Kab: assumes facts: "roleMap r tid0 = Some isoiec_9798_2_6_bdkey_P" "RLKR(s(AV ''P'' tid0)) ~: reveals t" "RLKR(s(MV ''A'' tid0)) ~: reveals t" "RLKR(s(MV ''B'' tid0)) ~: reveals t" "LN ''Kab'' tid0 : knows t" shows "False" using facts proof(sources! " LN ''Kab'' tid0 ") case isoiec_9798_2_6_bdkey_P_3_Kab note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case isoiec_9798_2_6_bdkey_P_3_Kab_1 note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) qed (insert facts, fastforce+)? lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_6_bdkey_A_secret_Kab: assumes facts: "roleMap r tid0 = Some isoiec_9798_2_6_bdkey_A" "RLKR(s(AV ''A'' tid0)) ~: reveals t" "RLKR(s(AV ''P'' tid0)) ~: reveals t" "RLKR(s(MV ''B'' tid0)) ~: reveals t" "( tid0, isoiec_9798_2_6_bdkey_A_3 ) : steps t" "s(MV ''Kab'' tid0) : knows t" shows "False" proof - note_prefix_closed facts = facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_6_enc_3_1'', LN ''Ra'' tid0, s(MV ''Kab'' tid0), s(AV ''A'' tid0), s(MV ''B'' tid0), s(MV ''Text4'' tid0) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(AV ''P'' tid0) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_6_bdkey_P_3_enc tid1) note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_6_bdkey_P_secret_Kab intro: event_predOrdI) qed (insert facts, fastforce+)? qed lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_6_bdkey_B_secret_Kab: assumes facts: "roleMap r tid0 = Some isoiec_9798_2_6_bdkey_B" "RLKR(s(AV ''A'' tid0)) ~: reveals t" "RLKR(s(AV ''B'' tid0)) ~: reveals t" "RLKR(s(MV ''P'' tid0)) ~: reveals t" "( tid0, isoiec_9798_2_6_bdkey_B_4 ) : steps t" "s(MV ''Kab'' tid0) : knows t" shows "False" proof - note_prefix_closed facts = facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_6_enc_3_2'', LN ''Rb'' tid0, s(MV ''Kab'' tid0), s(AV ''A'' tid0), s(AV ''B'' tid0), s(MV ''Text3'' tid0) |} ( Kbd ( s(AV ''B'' tid0) ) ( s(MV ''P'' tid0) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_6_bdkey_P_3_enc_1 tid1) note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_6_bdkey_P_secret_Kab intro: event_predOrdI) qed (insert facts, fastforce+)? qed lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_6_bdkey_A_injective_agreement_B: "let prems = (% tid0. roleMap r tid0 = Some isoiec_9798_2_6_bdkey_A & RLKR(s(AV ''A'' tid0)) ~: reveals t & RLKR(s(AV ''P'' tid0)) ~: reveals t & RLKR(s(MV ''B'' tid0)) ~: reveals t & ( tid0, isoiec_9798_2_6_bdkey_A_5 ) : steps t); concs = (% tid0 tid1. roleMap r tid1 = Some isoiec_9798_2_6_bdkey_B & ( tid1, isoiec_9798_2_6_bdkey_B_5 ) : steps t & {| s(AV ''A'' tid1), s(AV ''B'' tid1), s(MV ''P'' tid1), s(MV ''Kab'' tid1), s(MV ''Rpa'' tid1), LN ''Rb'' tid1, s(MV ''Text6'' tid1), s(MV ''Text8'' tid1) |} = {| s(AV ''A'' tid0), s(MV ''B'' tid0), s(AV ''P'' tid0), s(MV ''Kab'' tid0), LN ''Rpa'' tid0, s(MV ''Rb'' tid0), s(MV ''Text6'' tid0), s(MV ''Text8'' tid0) |}) in ? f. inj_on f (Collect prems) & (! i. prems i --> concs i (f i))" (is "let prems = ?prems; concs = ?concs in ?P prems concs") proof - { fix tid0 tid1 assume facts: "?prems tid0" have " ? tid1. ?concs tid0 tid1" proof - note_unified facts = facts note_prefix_closed facts = facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_6_enc_3_1'', LN ''Ra'' tid0, s(MV ''Kab'' tid0), s(AV ''A'' tid0), s(MV ''B'' tid0), s(MV ''Text4'' tid0) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(AV ''P'' tid0) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_6_bdkey_P_3_enc tid1) note_unified facts = this facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_6_enc_5'', s(MV ''Rb'' tid0), LN ''Rpa'' tid0, s(MV ''Text8'' tid0) |} ( LN ''Kab'' tid1 ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_6_bdkey_P_secret_Kab intro: event_predOrdI) next case (isoiec_9798_2_6_bdkey_B_5_enc tid2) note_unified facts = this facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_6_enc_3_2'', LN ''Rb'' tid2, LN ''Kab'' tid1, s(AV ''A'' tid2), s(AV ''B'' tid2), s(MV ''Text3'' tid2) |} ( Kbd ( s(AV ''B'' tid2) ) ( s(MV ''P'' tid2) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_6_bdkey_P_secret_Kab intro: event_predOrdI) next case (isoiec_9798_2_6_bdkey_P_3_enc_1 tid3) note_unified facts = this facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_6_enc_4'', LN ''Rpa'' tid0, LN ''Rb'' tid2, s(MV ''Text6'' tid2) |} ( LN ''Kab'' tid1 ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_6_bdkey_P_secret_Kab intro: event_predOrdI) next case (isoiec_9798_2_6_bdkey_A_4_enc tid3) note_unified facts = this facts thus ?thesis by (fastforce intro: event_predOrdI split: if_splits) qed (insert facts, fastforce+)? qed (insert facts, fastforce+)? qed (insert facts, fastforce+)? qed (insert facts, fastforce+)? qed } note niagree = this { fix i1 i2 j assume "?concs i1 j & ?concs i2 j" note_unified facts = this have "i1 = i2" using facts by simp } note conc_inj = this show ?thesis by (fast intro!: iagree_to_niagree elim!: niagree conc_inj) qed lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_6_bdkey_B_injective_agreement_A: "let prems = (% tid0. roleMap r tid0 = Some isoiec_9798_2_6_bdkey_B & RLKR(s(AV ''A'' tid0)) ~: reveals t & RLKR(s(AV ''B'' tid0)) ~: reveals t & RLKR(s(MV ''P'' tid0)) ~: reveals t & ( tid0, isoiec_9798_2_6_bdkey_B_4 ) : steps t); concs = (% tid0 tid1. roleMap r tid1 = Some isoiec_9798_2_6_bdkey_A & ( tid1, isoiec_9798_2_6_bdkey_A_4 ) : steps t & {| s(AV ''A'' tid1), s(MV ''B'' tid1), s(AV ''P'' tid1), s(MV ''Kab'' tid1), LN ''Rpa'' tid1, s(MV ''Rb'' tid1), s(MV ''Text6'' tid1) |} = {| s(AV ''A'' tid0), s(AV ''B'' tid0), s(MV ''P'' tid0), s(MV ''Kab'' tid0), s(MV ''Rpa'' tid0), LN ''Rb'' tid0, s(MV ''Text6'' tid0) |}) in ? f. inj_on f (Collect prems) & (! i. prems i --> concs i (f i))" (is "let prems = ?prems; concs = ?concs in ?P prems concs") proof - { fix tid0 tid1 assume facts: "?prems tid0" have " ? tid1. ?concs tid0 tid1" proof - note_unified facts = facts note_prefix_closed facts = facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_6_enc_3_2'', LN ''Rb'' tid0, s(MV ''Kab'' tid0), s(AV ''A'' tid0), s(AV ''B'' tid0), s(MV ''Text3'' tid0) |} ( Kbd ( s(AV ''B'' tid0) ) ( s(MV ''P'' tid0) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_6_bdkey_P_3_enc_1 tid1) note_unified facts = this facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_6_enc_4'', s(MV ''Rpa'' tid0), LN ''Rb'' tid0, s(MV ''Text6'' tid0) |} ( LN ''Kab'' tid1 ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_6_bdkey_P_secret_Kab intro: event_predOrdI) next case (isoiec_9798_2_6_bdkey_A_4_enc tid2) note_unified facts = this facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_6_enc_3_1'', LN ''Ra'' tid2, LN ''Kab'' tid1, s(AV ''A'' tid2), s(MV ''B'' tid2), s(MV ''Text4'' tid2) |} ( Kbd ( s(AV ''A'' tid2) ) ( s(AV ''P'' tid2) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_6_bdkey_P_secret_Kab intro: event_predOrdI) next case (isoiec_9798_2_6_bdkey_P_3_enc tid3) note_unified facts = this facts thus ?thesis by (fastforce intro: event_predOrdI split: if_splits) qed (insert facts, fastforce+)? qed (insert facts, fastforce+)? qed (insert facts, fastforce+)? qed } note niagree = this { fix i1 i2 j assume "?concs i1 j & ?concs i2 j" note_unified facts = this have "i1 = i2" using facts by simp } note conc_inj = this show ?thesis by (fast intro!: iagree_to_niagree elim!: niagree conc_inj) qed lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_6_bdkey_A_injective_agreement_P: "let prems = (% tid0. roleMap r tid0 = Some isoiec_9798_2_6_bdkey_A & RLKR(s(AV ''A'' tid0)) ~: reveals t & RLKR(s(AV ''P'' tid0)) ~: reveals t & RLKR(s(MV ''B'' tid0)) ~: reveals t & ( tid0, isoiec_9798_2_6_bdkey_A_3 ) : steps t); concs = (% tid0 tid1. roleMap r tid1 = Some isoiec_9798_2_6_bdkey_P & ( tid1, isoiec_9798_2_6_bdkey_P_3 ) : steps t & {| s(MV ''A'' tid1), s(MV ''B'' tid1), s(AV ''P'' tid1), s(MV ''Ra'' tid1), LN ''Kab'' tid1, s(MV ''Text4'' tid1) |} = {| s(AV ''A'' tid0), s(MV ''B'' tid0), s(AV ''P'' tid0), LN ''Ra'' tid0, s(MV ''Kab'' tid0), s(MV ''Text4'' tid0) |}) in ? f. inj_on f (Collect prems) & (! i. prems i --> concs i (f i))" (is "let prems = ?prems; concs = ?concs in ?P prems concs") proof - { fix tid0 tid1 assume facts: "?prems tid0" have " ? tid1. ?concs tid0 tid1" proof - note_unified facts = facts note_prefix_closed facts = facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_6_enc_3_1'', LN ''Ra'' tid0, s(MV ''Kab'' tid0), s(AV ''A'' tid0), s(MV ''B'' tid0), s(MV ''Text4'' tid0) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(AV ''P'' tid0) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_6_bdkey_P_3_enc tid1) note_unified facts = this facts thus ?thesis by (fastforce intro: event_predOrdI split: if_splits) qed (insert facts, fastforce+)? qed } note niagree = this { fix i1 i2 j assume "?concs i1 j & ?concs i2 j" note_unified facts = this have "i1 = i2" using facts by simp } note conc_inj = this show ?thesis by (fast intro!: iagree_to_niagree elim!: niagree conc_inj) qed lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_6_bdkey_B_injective_agreement_P: "let prems = (% tid0. roleMap r tid0 = Some isoiec_9798_2_6_bdkey_B & RLKR(s(AV ''A'' tid0)) ~: reveals t & RLKR(s(AV ''B'' tid0)) ~: reveals t & RLKR(s(MV ''P'' tid0)) ~: reveals t & ( tid0, isoiec_9798_2_6_bdkey_B_4 ) : steps t); concs = (% tid0 tid1. roleMap r tid1 = Some isoiec_9798_2_6_bdkey_P & ( tid1, isoiec_9798_2_6_bdkey_P_3 ) : steps t & {| s(MV ''A'' tid1), s(MV ''B'' tid1), s(AV ''P'' tid1), s(MV ''Rb'' tid1), LN ''Kab'' tid1, s(MV ''Text3'' tid1) |} = {| s(AV ''A'' tid0), s(AV ''B'' tid0), s(MV ''P'' tid0), LN ''Rb'' tid0, s(MV ''Kab'' tid0), s(MV ''Text3'' tid0) |}) in ? f. inj_on f (Collect prems) & (! i. prems i --> concs i (f i))" (is "let prems = ?prems; concs = ?concs in ?P prems concs") proof - { fix tid0 tid1 assume facts: "?prems tid0" have " ? tid1. ?concs tid0 tid1" proof - note_unified facts = facts note_prefix_closed facts = facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_6_enc_3_2'', LN ''Rb'' tid0, s(MV ''Kab'' tid0), s(AV ''A'' tid0), s(AV ''B'' tid0), s(MV ''Text3'' tid0) |} ( Kbd ( s(AV ''B'' tid0) ) ( s(MV ''P'' tid0) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_6_bdkey_P_3_enc_1 tid1) note_unified facts = this facts thus ?thesis by (fastforce intro: event_predOrdI split: if_splits) qed (insert facts, fastforce+)? qed } note niagree = this { fix i1 i2 j assume "?concs i1 j & ?concs i2 j" note_unified facts = this have "i1 = i2" using facts by simp } note conc_inj = this show ?thesis by (fast intro!: iagree_to_niagree elim!: niagree conc_inj) qed lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_5_special_TTP_bdkey_P_secret_Kab: assumes facts: "roleMap r tid0 = Some isoiec_9798_2_5_special_TTP_bdkey_P" "RLKR(s(AV ''P'' tid0)) ~: reveals t" "RLKR(s(MV ''A'' tid0)) ~: reveals t" "RLKR(s(MV ''B'' tid0)) ~: reveals t" "LN ''Kab'' tid0 : knows t" shows "False" using facts proof(sources! " LN ''Kab'' tid0 ") case isoiec_9798_2_5_special_TTP_bdkey_P_2_Kab note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case isoiec_9798_2_5_special_TTP_bdkey_P_2_Kab_1 note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) qed (insert facts, fastforce+)? lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_5_special_TTP_bdkey_A_secret_Kab: assumes facts: "roleMap r tid0 = Some isoiec_9798_2_5_special_TTP_bdkey_A" "RLKR(s(AV ''A'' tid0)) ~: reveals t" "RLKR(s(AV ''B'' tid0)) ~: reveals t" "RLKR(s(AV ''P'' tid0)) ~: reveals t" "( tid0, isoiec_9798_2_5_special_TTP_bdkey_A_2 ) : steps t" "s(MV ''Kab'' tid0) : knows t" shows "False" proof - note_prefix_closed facts = facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_5_special_TTP_enc_2_1'', LN ''TVPa'' tid0, s(MV ''Kab'' tid0), s(AV ''B'' tid0), s(MV ''Text3'' tid0) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(AV ''P'' tid0) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_5_special_TTP_bdkey_P_2_enc tid1) note_unified facts = this facts hence "Kbd ( s(AV ''P'' tid1) ) ( s(MV ''A'' tid1) ) = Kbd ( s(AV ''A'' tid0) ) ( s(AV ''P'' tid0) )" by simp note facts = this facts thus ?thesis proof(cases rule: Kbd_cases) case noswap note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_5_special_TTP_bdkey_different_actors_A_P intro: event_predOrdI) next case swapped note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_5_special_TTP_bdkey_P_secret_Kab intro: event_predOrdI) qed (fastforce+)? qed (insert facts, fastforce+)? qed lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_5_special_TTP_bdkey_B_secret_Kab: assumes facts: "roleMap r tid0 = Some isoiec_9798_2_5_special_TTP_bdkey_B" "RLKR(s(AV ''B'' tid0)) ~: reveals t" "RLKR(s(MV ''A'' tid0)) ~: reveals t" "RLKR(s(MV ''P'' tid0)) ~: reveals t" "( tid0, isoiec_9798_2_5_special_TTP_bdkey_B_3 ) : steps t" "s(MV ''Kab'' tid0) : knows t" shows "False" proof - note_prefix_closed facts = facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_5_special_TTP_enc_2_2'', s(MV ''TNp'' tid0), s(MV ''Kab'' tid0), s(MV ''A'' tid0), s(MV ''Text2'' tid0) |} ( Kbd ( s(AV ''B'' tid0) ) ( s(MV ''P'' tid0) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_5_special_TTP_bdkey_P_2_enc_1 tid1) note_unified facts = this facts hence "Kbd ( s(AV ''P'' tid1) ) ( s(MV ''B'' tid1) ) = Kbd ( s(AV ''B'' tid0) ) ( s(MV ''P'' tid0) )" by simp note facts = this facts thus ?thesis proof(cases rule: Kbd_cases) case noswap note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_5_special_TTP_bdkey_P_secret_Kab intro: event_predOrdI) next case swapped note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_5_special_TTP_bdkey_P_secret_Kab intro: event_predOrdI) qed (fastforce+)? qed (insert facts, fastforce+)? qed lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_5_special_TTP_bdkey_A_injective_agreement_B: "let prems = (% tid0. roleMap r tid0 = Some isoiec_9798_2_5_special_TTP_bdkey_A & RLKR(s(AV ''A'' tid0)) ~: reveals t & RLKR(s(AV ''B'' tid0)) ~: reveals t & RLKR(s(AV ''P'' tid0)) ~: reveals t & ( tid0, isoiec_9798_2_5_special_TTP_bdkey_A_4 ) : steps t); concs = (% tid0 tid1. roleMap r tid1 = Some isoiec_9798_2_5_special_TTP_bdkey_B & ( tid1, isoiec_9798_2_5_special_TTP_bdkey_B_4 ) : steps t & {| s(MV ''A'' tid1), s(AV ''B'' tid1), s(MV ''P'' tid1), s(MV ''Kab'' tid1), s(MV ''TNa'' tid1), s(MV ''Text5'' tid1), LN ''TNb'' tid1, s(MV ''Text7'' tid1) |} = {| s(AV ''A'' tid0), s(AV ''B'' tid0), s(AV ''P'' tid0), s(MV ''Kab'' tid0), LN ''TNa'' tid0, s(MV ''Text5'' tid0), s(MV ''TNb'' tid0), s(MV ''Text7'' tid0) |}) in ? f. inj_on f (Collect prems) & (! i. prems i --> concs i (f i))" (is "let prems = ?prems; concs = ?concs in ?P prems concs") proof - { fix tid0 tid1 assume facts: "?prems tid0" have " ? tid1. ?concs tid0 tid1" proof - note_unified facts = facts note_prefix_closed facts = facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_5_special_TTP_enc_2_1'', LN ''TVPa'' tid0, s(MV ''Kab'' tid0), s(AV ''B'' tid0), s(MV ''Text3'' tid0) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(AV ''P'' tid0) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_5_special_TTP_bdkey_P_2_enc tid1) note_unified facts = this facts hence "Kbd ( s(AV ''P'' tid1) ) ( s(MV ''A'' tid1) ) = Kbd ( s(AV ''A'' tid0) ) ( s(AV ''P'' tid0) )" by simp note facts = this facts thus ?thesis proof(cases rule: Kbd_cases) case noswap note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_5_special_TTP_bdkey_different_actors_A_P intro: event_predOrdI) next case swapped note_unified facts = this facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_5_special_TTP_enc_4'', s(MV ''TNb'' tid0), s(AV ''A'' tid0), s(MV ''Text7'' tid0) |} ( LN ''Kab'' tid1 ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_5_special_TTP_bdkey_P_secret_Kab intro: event_predOrdI) next case (isoiec_9798_2_5_special_TTP_bdkey_B_4_enc tid2) note_unified facts = this facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_5_special_TTP_enc_3'', s(MV ''TNa'' tid2), s(AV ''B'' tid2), s(MV ''Text5'' tid2) |} ( LN ''Kab'' tid1 ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_5_special_TTP_bdkey_P_secret_Kab intro: event_predOrdI) next case (isoiec_9798_2_5_special_TTP_bdkey_A_3_enc tid3) note_unified facts = this facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_5_special_TTP_enc_2_1'', LN ''TVPa'' tid3, LN ''Kab'' tid1, s(AV ''B'' tid2), s(MV ''Text3'' tid3) |} ( Kbd ( s(AV ''A'' tid3) ) ( s(AV ''P'' tid3) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_5_special_TTP_bdkey_P_secret_Kab intro: event_predOrdI) next case (isoiec_9798_2_5_special_TTP_bdkey_P_2_enc tid4) note_unified facts = this facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_5_special_TTP_enc_2_2'', s(MV ''TNp'' tid2), LN ''Kab'' tid1, s(AV ''A'' tid0), s(MV ''Text2'' tid2) |} ( Kbd ( s(AV ''B'' tid0) ) ( s(MV ''P'' tid2) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_5_special_TTP_bdkey_P_secret_Kab intro: event_predOrdI) next case (isoiec_9798_2_5_special_TTP_bdkey_P_2_enc_1 tid3) note_unified facts = this facts thus ?thesis by (fastforce intro: event_predOrdI split: if_splits) qed (insert facts, fastforce+)? qed (insert facts, fastforce+)? qed (insert facts, fastforce+)? qed (insert facts, fastforce+)? qed (fastforce+)? qed (insert facts, fastforce+)? qed } note niagree = this { fix i1 i2 j assume "?concs i1 j & ?concs i2 j" note_unified facts = this have "i1 = i2" using facts by simp } note conc_inj = this show ?thesis by (fast intro!: iagree_to_niagree elim!: niagree conc_inj) qed lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_5_special_TTP_bdkey_B_non_injective_agreement_A: assumes facts: "roleMap r tid0 = Some isoiec_9798_2_5_special_TTP_bdkey_B" "RLKR(s(AV ''B'' tid0)) ~: reveals t" "RLKR(s(MV ''A'' tid0)) ~: reveals t" "RLKR(s(MV ''P'' tid0)) ~: reveals t" "( tid0, isoiec_9798_2_5_special_TTP_bdkey_B_3 ) : steps t" shows "(? tid1. roleMap r tid1 = Some isoiec_9798_2_5_special_TTP_bdkey_A & ( tid1, isoiec_9798_2_5_special_TTP_bdkey_A_3 ) : steps t & {| s(AV ''A'' tid1), s(AV ''B'' tid1), s(AV ''P'' tid1), s(MV ''Kab'' tid1), LN ''TNa'' tid1, s(MV ''Text5'' tid1) |} = {| s(MV ''A'' tid0), s(AV ''B'' tid0), s(MV ''P'' tid0), s(MV ''Kab'' tid0), s(MV ''TNa'' tid0), s(MV ''Text5'' tid0) |})" proof - note_prefix_closed facts = facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_5_special_TTP_enc_3'', s(MV ''TNa'' tid0), s(AV ''B'' tid0), s(MV ''Text5'' tid0) |} ( s(MV ''Kab'' tid0) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_5_special_TTP_bdkey_B_secret_Kab intro: event_predOrdI) next case (isoiec_9798_2_5_special_TTP_bdkey_A_3_enc tid1) note_unified facts = this facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_5_special_TTP_enc_2_1'', LN ''TVPa'' tid1, s(MV ''Kab'' tid0), s(AV ''B'' tid0), s(MV ''Text3'' tid1) |} ( Kbd ( s(AV ''A'' tid1) ) ( s(AV ''P'' tid1) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_5_special_TTP_bdkey_B_secret_Kab intro: event_predOrdI) next case (isoiec_9798_2_5_special_TTP_bdkey_P_2_enc tid2) note_unified facts = this facts hence "Kbd ( s(AV ''P'' tid2) ) ( s(MV ''A'' tid2) ) = Kbd ( s(AV ''A'' tid1) ) ( s(AV ''P'' tid1) )" by simp note facts = this facts thus ?thesis proof(cases rule: Kbd_cases) case noswap note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_5_special_TTP_bdkey_different_actors_A_P intro: event_predOrdI) next case swapped note_unified facts = this facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_5_special_TTP_enc_2_2'', s(MV ''TNp'' tid0), LN ''Kab'' tid2, s(MV ''A'' tid0), s(MV ''Text2'' tid0) |} ( Kbd ( s(AV ''B'' tid0) ) ( s(MV ''P'' tid0) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_5_special_TTP_bdkey_P_2_enc_1 tid3) note_unified facts = this facts thus ?thesis by (fastforce intro: event_predOrdI split: if_splits) qed (insert facts, fastforce+)? qed (fastforce+)? qed (insert facts, fastforce+)? qed (insert facts, fastforce+)? qed lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_5_special_TTP_bdkey_A_injective_agreement_P: "let prems = (% tid0. roleMap r tid0 = Some isoiec_9798_2_5_special_TTP_bdkey_A & RLKR(s(AV ''A'' tid0)) ~: reveals t & RLKR(s(AV ''B'' tid0)) ~: reveals t & RLKR(s(AV ''P'' tid0)) ~: reveals t & ( tid0, isoiec_9798_2_5_special_TTP_bdkey_A_2 ) : steps t); concs = (% tid0 tid1. roleMap r tid1 = Some isoiec_9798_2_5_special_TTP_bdkey_P & ( tid1, isoiec_9798_2_5_special_TTP_bdkey_P_2 ) : steps t & {| s(MV ''A'' tid1), s(MV ''B'' tid1), s(AV ''P'' tid1), LN ''Kab'' tid1, s(MV ''TVPa'' tid1), s(MV ''Text3'' tid1) |} = {| s(AV ''A'' tid0), s(AV ''B'' tid0), s(AV ''P'' tid0), s(MV ''Kab'' tid0), LN ''TVPa'' tid0, s(MV ''Text3'' tid0) |}) in ? f. inj_on f (Collect prems) & (! i. prems i --> concs i (f i))" (is "let prems = ?prems; concs = ?concs in ?P prems concs") proof - { fix tid0 tid1 assume facts: "?prems tid0" have " ? tid1. ?concs tid0 tid1" proof - note_unified facts = facts note_prefix_closed facts = facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_5_special_TTP_enc_2_1'', LN ''TVPa'' tid0, s(MV ''Kab'' tid0), s(AV ''B'' tid0), s(MV ''Text3'' tid0) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(AV ''P'' tid0) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_5_special_TTP_bdkey_P_2_enc tid1) note_unified facts = this facts hence "Kbd ( s(AV ''P'' tid1) ) ( s(MV ''A'' tid1) ) = Kbd ( s(AV ''A'' tid0) ) ( s(AV ''P'' tid0) )" by simp note facts = this facts thus ?thesis proof(cases rule: Kbd_cases) case noswap note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_5_special_TTP_bdkey_different_actors_A_P intro: event_predOrdI) next case swapped note_unified facts = this facts thus ?thesis by (fastforce intro: event_predOrdI split: if_splits) qed (fastforce+)? qed (insert facts, fastforce+)? qed } note niagree = this { fix i1 i2 j assume "?concs i1 j & ?concs i2 j" note_unified facts = this have "i1 = i2" using facts by simp } note conc_inj = this show ?thesis by (fast intro!: iagree_to_niagree elim!: niagree conc_inj) qed lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_5_special_TTP_bdkey_B_non_injective_agreement_P: assumes facts: "roleMap r tid0 = Some isoiec_9798_2_5_special_TTP_bdkey_B" "RLKR(s(AV ''B'' tid0)) ~: reveals t" "RLKR(s(MV ''A'' tid0)) ~: reveals t" "RLKR(s(MV ''P'' tid0)) ~: reveals t" "( tid0, isoiec_9798_2_5_special_TTP_bdkey_B_3 ) : steps t" shows "(? tid1. roleMap r tid1 = Some isoiec_9798_2_5_special_TTP_bdkey_P & ( tid1, isoiec_9798_2_5_special_TTP_bdkey_P_2 ) : steps t & {| s(MV ''A'' tid1), s(MV ''B'' tid1), s(AV ''P'' tid1), LN ''Kab'' tid1, LN ''TNp'' tid1, s(MV ''Text2'' tid1) |} = {| s(MV ''A'' tid0), s(AV ''B'' tid0), s(MV ''P'' tid0), s(MV ''Kab'' tid0), s(MV ''TNp'' tid0), s(MV ''Text2'' tid0) |})" proof - note_prefix_closed facts = facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_5_special_TTP_enc_2_2'', s(MV ''TNp'' tid0), s(MV ''Kab'' tid0), s(MV ''A'' tid0), s(MV ''Text2'' tid0) |} ( Kbd ( s(AV ''B'' tid0) ) ( s(MV ''P'' tid0) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_5_special_TTP_bdkey_P_2_enc_1 tid1) note_unified facts = this facts hence "Kbd ( s(AV ''P'' tid1) ) ( s(MV ''B'' tid1) ) = Kbd ( s(AV ''B'' tid0) ) ( s(MV ''P'' tid0) )" by simp note facts = this facts thus ?thesis proof(cases rule: Kbd_cases) case noswap note_unified facts = this facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_5_special_TTP_enc_3'', s(MV ''TNa'' tid0), s(AV ''B'' tid0), s(MV ''Text5'' tid0) |} ( LN ''Kab'' tid1 ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_5_special_TTP_bdkey_P_secret_Kab intro: event_predOrdI) next case (isoiec_9798_2_5_special_TTP_bdkey_A_3_enc tid2) note_unified facts = this facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_5_special_TTP_enc_2_1'', LN ''TVPa'' tid2, LN ''Kab'' tid1, s(AV ''B'' tid0), s(MV ''Text3'' tid2) |} ( Kbd ( s(AV ''A'' tid2) ) ( s(AV ''P'' tid2) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_5_special_TTP_bdkey_P_secret_Kab intro: event_predOrdI) next case (isoiec_9798_2_5_special_TTP_bdkey_P_2_enc tid3) note_unified facts = this facts thus ?thesis by (fastforce intro: event_predOrdI split: if_splits) qed (insert facts, fastforce+)? qed (insert facts, fastforce+)? next case swapped note_unified facts = this facts thus ?thesis by (fastforce intro: event_predOrdI split: if_splits) qed (fastforce+)? qed (insert facts, fastforce+)? qed lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_6_special_TTP_bdkey_P_secret_Kab: assumes facts: "roleMap r tid0 = Some isoiec_9798_2_6_special_TTP_bdkey_P" "RLKR(s(AV ''P'' tid0)) ~: reveals t" "RLKR(s(MV ''A'' tid0)) ~: reveals t" "RLKR(s(MV ''B'' tid0)) ~: reveals t" "LN ''Kab'' tid0 : knows t" shows "False" using facts proof(sources! " LN ''Kab'' tid0 ") case isoiec_9798_2_6_special_TTP_bdkey_P_3_Kab note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case isoiec_9798_2_6_special_TTP_bdkey_P_3_Kab_1 note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) qed (insert facts, fastforce+)? lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_6_special_TTP_bdkey_A_secret_Kab: assumes facts: "roleMap r tid0 = Some isoiec_9798_2_6_special_TTP_bdkey_A" "RLKR(s(AV ''A'' tid0)) ~: reveals t" "RLKR(s(AV ''P'' tid0)) ~: reveals t" "RLKR(s(MV ''B'' tid0)) ~: reveals t" "( tid0, isoiec_9798_2_6_special_TTP_bdkey_A_3 ) : steps t" "s(MV ''Kab'' tid0) : knows t" shows "False" proof - note_prefix_closed facts = facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_6_special_TTP_enc_3_1'', LN ''Ra'' tid0, s(MV ''Kab'' tid0), s(MV ''B'' tid0), s(MV ''Text4'' tid0) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(AV ''P'' tid0) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_6_special_TTP_bdkey_P_3_enc tid1) note_unified facts = this facts hence "Kbd ( s(AV ''P'' tid1) ) ( s(MV ''A'' tid1) ) = Kbd ( s(AV ''A'' tid0) ) ( s(AV ''P'' tid0) )" by simp note facts = this facts thus ?thesis proof(cases rule: Kbd_cases) case noswap note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_6_special_TTP_bdkey_different_actors_A_P intro: event_predOrdI) next case swapped note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_6_special_TTP_bdkey_P_secret_Kab intro: event_predOrdI) qed (fastforce+)? qed (insert facts, fastforce+)? qed lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_6_special_TTP_bdkey_B_secret_Kab: assumes facts: "roleMap r tid0 = Some isoiec_9798_2_6_special_TTP_bdkey_B" "RLKR(s(AV ''A'' tid0)) ~: reveals t" "RLKR(s(AV ''B'' tid0)) ~: reveals t" "RLKR(s(MV ''P'' tid0)) ~: reveals t" "( tid0, isoiec_9798_2_6_special_TTP_bdkey_B_4 ) : steps t" "s(MV ''Kab'' tid0) : knows t" shows "False" proof - note_prefix_closed facts = facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_6_special_TTP_enc_3_2'', LN ''Rb'' tid0, s(MV ''Kab'' tid0), s(AV ''A'' tid0), s(MV ''Text3'' tid0) |} ( Kbd ( s(AV ''B'' tid0) ) ( s(MV ''P'' tid0) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_6_special_TTP_bdkey_P_3_enc_1 tid1) note_unified facts = this facts hence "Kbd ( s(AV ''P'' tid1) ) ( s(MV ''B'' tid1) ) = Kbd ( s(AV ''B'' tid0) ) ( s(MV ''P'' tid0) )" by simp note facts = this facts thus ?thesis proof(cases rule: Kbd_cases) case noswap note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_6_special_TTP_bdkey_different_actors_B_P intro: event_predOrdI) next case swapped note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_6_special_TTP_bdkey_P_secret_Kab intro: event_predOrdI) qed (fastforce+)? qed (insert facts, fastforce+)? qed lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_6_special_TTP_bdkey_A_injective_agreement_B: "let prems = (% tid0. roleMap r tid0 = Some isoiec_9798_2_6_special_TTP_bdkey_A & RLKR(s(AV ''A'' tid0)) ~: reveals t & RLKR(s(AV ''P'' tid0)) ~: reveals t & RLKR(s(MV ''B'' tid0)) ~: reveals t & ( tid0, isoiec_9798_2_6_special_TTP_bdkey_A_5 ) : steps t); concs = (% tid0 tid1. roleMap r tid1 = Some isoiec_9798_2_6_special_TTP_bdkey_B & ( tid1, isoiec_9798_2_6_special_TTP_bdkey_B_5 ) : steps t & {| s(AV ''A'' tid1), s(AV ''B'' tid1), s(MV ''P'' tid1), s(MV ''Kab'' tid1), s(MV ''Rpa'' tid1), LN ''Rb'' tid1, s(MV ''Text6'' tid1), s(MV ''Text8'' tid1) |} = {| s(AV ''A'' tid0), s(MV ''B'' tid0), s(AV ''P'' tid0), s(MV ''Kab'' tid0), LN ''Rpa'' tid0, s(MV ''Rb'' tid0), s(MV ''Text6'' tid0), s(MV ''Text8'' tid0) |}) in ? f. inj_on f (Collect prems) & (! i. prems i --> concs i (f i))" (is "let prems = ?prems; concs = ?concs in ?P prems concs") proof - { fix tid0 tid1 assume facts: "?prems tid0" have " ? tid1. ?concs tid0 tid1" proof - note_unified facts = facts note_prefix_closed facts = facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_6_special_TTP_enc_3_1'', LN ''Ra'' tid0, s(MV ''Kab'' tid0), s(MV ''B'' tid0), s(MV ''Text4'' tid0) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(AV ''P'' tid0) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_6_special_TTP_bdkey_P_3_enc tid1) note_unified facts = this facts hence "Kbd ( s(AV ''P'' tid1) ) ( s(MV ''A'' tid1) ) = Kbd ( s(AV ''A'' tid0) ) ( s(AV ''P'' tid0) )" by simp note facts = this facts thus ?thesis proof(cases rule: Kbd_cases) case noswap note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_6_special_TTP_bdkey_different_actors_A_P intro: event_predOrdI) next case swapped note_unified facts = this facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_6_special_TTP_enc_5'', s(MV ''Rb'' tid0), LN ''Rpa'' tid0, s(MV ''Text8'' tid0) |} ( LN ''Kab'' tid1 ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_6_special_TTP_bdkey_P_secret_Kab intro: event_predOrdI) next case (isoiec_9798_2_6_special_TTP_bdkey_B_5_enc tid2) note_unified facts = this facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_6_special_TTP_enc_3_2'', LN ''Rb'' tid2, LN ''Kab'' tid1, s(AV ''A'' tid2), s(MV ''Text3'' tid2) |} ( Kbd ( s(AV ''B'' tid2) ) ( s(MV ''P'' tid2) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_6_special_TTP_bdkey_P_secret_Kab intro: event_predOrdI) next case (isoiec_9798_2_6_special_TTP_bdkey_P_3_enc_1 tid3) note_unified facts = this facts hence "Kbd ( s(AV ''P'' tid0) ) ( s(MV ''B'' tid0) ) = Kbd ( s(AV ''B'' tid2) ) ( s(MV ''P'' tid2) )" by simp note facts = this facts thus ?thesis proof(cases rule: Kbd_cases) case noswap note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_6_special_TTP_bdkey_different_actors_B_P intro: event_predOrdI) next case swapped note_unified facts = this facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_6_special_TTP_enc_4'', LN ''Rpa'' tid0, LN ''Rb'' tid2, s(MV ''Text6'' tid2) |} ( LN ''Kab'' tid1 ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_6_special_TTP_bdkey_P_secret_Kab intro: event_predOrdI) next case (isoiec_9798_2_6_special_TTP_bdkey_A_4_enc tid3) note_unified facts = this facts thus ?thesis by (fastforce intro: event_predOrdI split: if_splits) qed (insert facts, fastforce+)? qed (fastforce+)? qed (insert facts, fastforce+)? qed (insert facts, fastforce+)? qed (fastforce+)? qed (insert facts, fastforce+)? qed } note niagree = this { fix i1 i2 j assume "?concs i1 j & ?concs i2 j" note_unified facts = this have "i1 = i2" using facts by simp } note conc_inj = this show ?thesis by (fast intro!: iagree_to_niagree elim!: niagree conc_inj) qed lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_6_special_TTP_bdkey_B_injective_agreement_A: "let prems = (% tid0. roleMap r tid0 = Some isoiec_9798_2_6_special_TTP_bdkey_B & RLKR(s(AV ''A'' tid0)) ~: reveals t & RLKR(s(AV ''B'' tid0)) ~: reveals t & RLKR(s(MV ''P'' tid0)) ~: reveals t & ( tid0, isoiec_9798_2_6_special_TTP_bdkey_B_4 ) : steps t); concs = (% tid0 tid1. roleMap r tid1 = Some isoiec_9798_2_6_special_TTP_bdkey_A & ( tid1, isoiec_9798_2_6_special_TTP_bdkey_A_4 ) : steps t & {| s(AV ''A'' tid1), s(MV ''B'' tid1), s(AV ''P'' tid1), s(MV ''Kab'' tid1), LN ''Rpa'' tid1, s(MV ''Rb'' tid1), s(MV ''Text6'' tid1) |} = {| s(AV ''A'' tid0), s(AV ''B'' tid0), s(MV ''P'' tid0), s(MV ''Kab'' tid0), s(MV ''Rpa'' tid0), LN ''Rb'' tid0, s(MV ''Text6'' tid0) |}) in ? f. inj_on f (Collect prems) & (! i. prems i --> concs i (f i))" (is "let prems = ?prems; concs = ?concs in ?P prems concs") proof - { fix tid0 tid1 assume facts: "?prems tid0" have " ? tid1. ?concs tid0 tid1" proof - note_unified facts = facts note_prefix_closed facts = facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_6_special_TTP_enc_3_2'', LN ''Rb'' tid0, s(MV ''Kab'' tid0), s(AV ''A'' tid0), s(MV ''Text3'' tid0) |} ( Kbd ( s(AV ''B'' tid0) ) ( s(MV ''P'' tid0) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_6_special_TTP_bdkey_P_3_enc_1 tid1) note_unified facts = this facts hence "Kbd ( s(AV ''P'' tid1) ) ( s(MV ''B'' tid1) ) = Kbd ( s(AV ''B'' tid0) ) ( s(MV ''P'' tid0) )" by simp note facts = this facts thus ?thesis proof(cases rule: Kbd_cases) case noswap note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_6_special_TTP_bdkey_different_actors_B_P intro: event_predOrdI) next case swapped note_unified facts = this facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_6_special_TTP_enc_4'', s(MV ''Rpa'' tid0), LN ''Rb'' tid0, s(MV ''Text6'' tid0) |} ( LN ''Kab'' tid1 ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_6_special_TTP_bdkey_P_secret_Kab intro: event_predOrdI) next case (isoiec_9798_2_6_special_TTP_bdkey_A_4_enc tid2) note_unified facts = this facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_6_special_TTP_enc_3_1'', LN ''Ra'' tid2, LN ''Kab'' tid1, s(MV ''B'' tid2), s(MV ''Text4'' tid2) |} ( Kbd ( s(AV ''A'' tid2) ) ( s(AV ''P'' tid2) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_6_special_TTP_bdkey_P_secret_Kab intro: event_predOrdI) next case (isoiec_9798_2_6_special_TTP_bdkey_P_3_enc tid3) note_unified facts = this facts hence "Kbd ( s(AV ''A'' tid2) ) ( s(AV ''P'' tid2) ) = Kbd ( s(AV ''A'' tid0) ) ( s(AV ''P'' tid1) )" by simp note facts = this facts thus ?thesis proof(cases rule: Kbd_cases) case noswap note_unified facts = this facts thus ?thesis by (fastforce intro: event_predOrdI split: if_splits) next case swapped note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_6_special_TTP_bdkey_different_actors_A_P intro: event_predOrdI) qed (fastforce+)? qed (insert facts, fastforce+)? qed (insert facts, fastforce+)? qed (fastforce+)? qed (insert facts, fastforce+)? qed } note niagree = this { fix i1 i2 j assume "?concs i1 j & ?concs i2 j" note_unified facts = this have "i1 = i2" using facts by simp } note conc_inj = this show ?thesis by (fast intro!: iagree_to_niagree elim!: niagree conc_inj) qed lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_6_special_TTP_bdkey_A_injective_agreement_P: "let prems = (% tid0. roleMap r tid0 = Some isoiec_9798_2_6_special_TTP_bdkey_A & RLKR(s(AV ''A'' tid0)) ~: reveals t & RLKR(s(AV ''P'' tid0)) ~: reveals t & RLKR(s(MV ''B'' tid0)) ~: reveals t & ( tid0, isoiec_9798_2_6_special_TTP_bdkey_A_3 ) : steps t); concs = (% tid0 tid1. roleMap r tid1 = Some isoiec_9798_2_6_special_TTP_bdkey_P & ( tid1, isoiec_9798_2_6_special_TTP_bdkey_P_3 ) : steps t & {| s(MV ''A'' tid1), s(MV ''B'' tid1), s(AV ''P'' tid1), s(MV ''Ra'' tid1), LN ''Kab'' tid1, s(MV ''Text4'' tid1) |} = {| s(AV ''A'' tid0), s(MV ''B'' tid0), s(AV ''P'' tid0), LN ''Ra'' tid0, s(MV ''Kab'' tid0), s(MV ''Text4'' tid0) |}) in ? f. inj_on f (Collect prems) & (! i. prems i --> concs i (f i))" (is "let prems = ?prems; concs = ?concs in ?P prems concs") proof - { fix tid0 tid1 assume facts: "?prems tid0" have " ? tid1. ?concs tid0 tid1" proof - note_unified facts = facts note_prefix_closed facts = facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_6_special_TTP_enc_3_1'', LN ''Ra'' tid0, s(MV ''Kab'' tid0), s(MV ''B'' tid0), s(MV ''Text4'' tid0) |} ( Kbd ( s(AV ''A'' tid0) ) ( s(AV ''P'' tid0) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_6_special_TTP_bdkey_P_3_enc tid1) note_unified facts = this facts hence "Kbd ( s(AV ''P'' tid1) ) ( s(MV ''A'' tid1) ) = Kbd ( s(AV ''A'' tid0) ) ( s(AV ''P'' tid0) )" by simp note facts = this facts thus ?thesis proof(cases rule: Kbd_cases) case noswap note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_6_special_TTP_bdkey_different_actors_A_P intro: event_predOrdI) next case swapped note_unified facts = this facts thus ?thesis by (fastforce intro: event_predOrdI split: if_splits) qed (fastforce+)? qed (insert facts, fastforce+)? qed } note niagree = this { fix i1 i2 j assume "?concs i1 j & ?concs i2 j" note_unified facts = this have "i1 = i2" using facts by simp } note conc_inj = this show ?thesis by (fast intro!: iagree_to_niagree elim!: niagree conc_inj) qed lemma (in restricted_isoiec_9798_2_bdkey_state) isoiec_9798_2_6_special_TTP_bdkey_B_injective_agreement_P: "let prems = (% tid0. roleMap r tid0 = Some isoiec_9798_2_6_special_TTP_bdkey_B & RLKR(s(AV ''A'' tid0)) ~: reveals t & RLKR(s(AV ''B'' tid0)) ~: reveals t & RLKR(s(MV ''P'' tid0)) ~: reveals t & ( tid0, isoiec_9798_2_6_special_TTP_bdkey_B_4 ) : steps t); concs = (% tid0 tid1. roleMap r tid1 = Some isoiec_9798_2_6_special_TTP_bdkey_P & ( tid1, isoiec_9798_2_6_special_TTP_bdkey_P_3 ) : steps t & {| s(MV ''A'' tid1), s(MV ''B'' tid1), s(AV ''P'' tid1), s(MV ''Rb'' tid1), LN ''Kab'' tid1, s(MV ''Text3'' tid1) |} = {| s(AV ''A'' tid0), s(AV ''B'' tid0), s(MV ''P'' tid0), LN ''Rb'' tid0, s(MV ''Kab'' tid0), s(MV ''Text3'' tid0) |}) in ? f. inj_on f (Collect prems) & (! i. prems i --> concs i (f i))" (is "let prems = ?prems; concs = ?concs in ?P prems concs") proof - { fix tid0 tid1 assume facts: "?prems tid0" have " ? tid1. ?concs tid0 tid1" proof - note_unified facts = facts note_prefix_closed facts = facts thus ?thesis proof(sources! " Enc {| LC ''isoiec_9798_2_6_special_TTP_enc_3_2'', LN ''Rb'' tid0, s(MV ''Kab'' tid0), s(AV ''A'' tid0), s(MV ''Text3'' tid0) |} ( Kbd ( s(AV ''B'' tid0) ) ( s(MV ''P'' tid0) ) ) ") case fake note_unified facts = this facts thus ?thesis by (fastforce dest!: ltk_secrecy) next case (isoiec_9798_2_6_special_TTP_bdkey_P_3_enc_1 tid1) note_unified facts = this facts hence "Kbd ( s(AV ''P'' tid1) ) ( s(MV ''B'' tid1) ) = Kbd ( s(AV ''B'' tid0) ) ( s(MV ''P'' tid0) )" by simp note facts = this facts thus ?thesis proof(cases rule: Kbd_cases) case noswap note_unified facts = this facts thus ?thesis by (fastforce dest: isoiec_9798_2_6_special_TTP_bdkey_different_actors_B_P intro: event_predOrdI) next case swapped note_unified facts = this facts thus ?thesis by (fastforce intro: event_predOrdI split: if_splits) qed (fastforce+)? qed (insert facts, fastforce+)? qed } note niagree = this { fix i1 i2 j assume "?concs i1 j & ?concs i2 j" note_unified facts = this have "i1 = i2" using facts by simp } note conc_inj = this show ?thesis by (fast intro!: iagree_to_niagree elim!: niagree conc_inj) qed end