/* * Modeled from ISO/IEC 9798-2 * Modeler: Cas Cremers, Dec. 2010 * Ported to scyther-proof: Simon Meier, Feb. 2011 * * Modeling notes: * - Variant of ISO/IEC 9798-2 with bidirectional keys k[A,B]. * - time-variant-parameters, time-stamps, and sequence numbers are * modeled by nonces leaked to the adversary at the start of a role. * - The TextX fields are chosen by the adversary. */ theory isoiec_9798_2_bdkey begin /****************************************************************************** * Protocol 1 ****************************************************************************** * * symmetric * one-pass * unilateral * * Note: the identity B may be ommitted, if * (a) the environment disallows such attacks, or * (b) a unidirectional key is used * (This formulation directly stems from the standard.) */ protocol isoiec_9798_2_1_bdkey { leak_A. A -> : TNA text_1. -> A: Text1, Text2 1. A -> B: A, B, Text2, {'isoiec_9798_2_1_enc_1', TNA, B, Text1 }k[A,B] } // Here we dont get any injective agreement, as there could be two B thread // receiving the same message from one A. property (of isoiec_9798_2_1_bdkey) B_non_injective_agreement: niagree(B_1[A,B,TNA,Text1] -> A_1[A,B,TNA,Text1], {A, B}) /****************************************************************************** * Protocol 2 ****************************************************************************** * * symmetric * two-pass * unilateral * * Note: the identity B may be ommitted, if * (a) the environment disallows such attacks, or * (b) a unidirectional key is used */ protocol isoiec_9798_2_2_bdkey { text_1. -> B: Text1 1. B -> A: B, A, RB, Text1 text_2. -> A: Text2, Text3 2. A -> B: A, B, Text3, {'isoiec_9798_2_2_enc_2', RB, B, Text2}k[B,A] } property (of isoiec_9798_2_2_bdkey) B_injective_agreement: iagree(B_2[A,B,RB,Text2] -> A_2[A,B,RB,Text2], {A, B}) /****************************************************************************** * Protocol 3 ****************************************************************************** * * symmetric * two-pass * mutual * * Note: the identities inside the encryptions may be ommitted, if * (a) the environment disallows such attacks, or * (b) a unidirectional key is used */ protocol isoiec_9798_2_3_bdkey { leak_A. A -> : TNA leak_B. B -> : TNB text_1. -> A: Text1, Text2 1. A -> B: A, B, Text2, {'isoiec_9798_2_3_enc_1', TNA, B, Text1 }k[A,B] text_2. -> B: Text3, Text4 2. B -> A: B, A, Text4, {'isoiec_9798_2_3_enc_2', TNB, A, Text3 }k[B,A] } // NOTE: We do not get injective agreement here, in neither direction. The // problem is the same as in isoiec_9798_2_1_bdkey. However, we are missing // the opportunity to strengthen the property for A, as we could just embed // TNA in the message sent from B. properties (of isoiec_9798_2_3_bdkey) A_non_injective_agreement: niagree(A_2[A,B,TNB,Text3] -> B_2[A,B,TNB,Text3], {A, B}) B_non_injective_agreement: niagree(B_1[A,B,TNA,Text1] -> A_1[A,B,TNA,Text1], {A, B}) /****************************************************************************** * Protocol 4 ****************************************************************************** * * symmetric * three-pass * mutual * * Note: the identity B inside the encryption may be ommitted, if * (a) the environment disallows such attacks, or * (b) a unidirectional key is used * */ protocol isoiec_9798_2_4_bdkey { text_1. -> B: Text1 1. B -> A: B, A, RB, Text1 text_2. -> A: Text2, Text3 2. A -> B: A, B, Text3, {'isoiec_9798_2_4_enc_1', RA, RB, B, Text2 }k[A,B] text_3. -> B: Text4, Text5 3. B -> A: B, A, Text5, {'isoiec_9798_2_4_enc_2', RB, RA, Text4 }k[A,B] } properties (of isoiec_9798_2_4_bdkey) A_injective_agreement: iagree(A_3[A,B,RA,RB,Text2,Text4] -> B_3[A,B,RA,RB,Text2,Text4], {A, B}) B_injective_agreement: iagree(B_2[A,B,RA,RB,Text2] -> A_2[A,B,RA,RB,Text2], {A, B}) /****************************************************************************** * Protocol 5 ****************************************************************************** * * symmetric * ttp * four-pass * mutual * * Modeling notes: * - The use of TNb in message 4, as specified by the ISO standard, is * different from other models, in which it was TNa. * - Added additional identity to messages in Step 2 to avoid identity swapping. * - We send identity P in Step 3 in order for B to be able to lookup key k(B,P) */ protocol isoiec_9798_2_5_bdkey { leak_A. A -> : TVPa, TNa leak_B. B -> : TNb leak_P. P -> : TNp text_1. -> A: Text1 1. A -> P: A, P, TVPa, B, Text1 text_2. -> P: Text2, Text3, Text4 2. P -> : P, A, Text4, { 'isoiec_9798_2_5_enc_2_1', TVPa, Kab, A, B, Text3 }k[A,P] , { 'isoiec_9798_2_5_enc_2_2', TNp , Kab, A, B, Text2 }k[B,P] -> A: P, A, Text4, { 'isoiec_9798_2_5_enc_2_1', TVPa, Kab, A, B, Text3 }k[A,P] , TokenPA_for_B text_3. -> A: Text5, Text6 3. A -> : A, B, Text6, P, TokenPA_for_B , { 'isoiec_9798_2_5_enc_3', TNa, B, Text5 }Kab -> B: A, B, Text6, P, { 'isoiec_9798_2_5_enc_2_2', TNp, Kab, A, B, Text2 }k[B,P] , { 'isoiec_9798_2_5_enc_3', TNa, B, Text5 }Kab text_4. -> B: Text7, Text8 4. B -> A: B, A, Text8, { 'isoiec_9798_2_5_enc_4', TNb, A, Text7 }Kab } properties (of isoiec_9798_2_5_bdkey) P_secret_Kab: secret(P, -, Kab, {A, B, P}) A_secret_Kab: secret(A, 2, Kab, {A, B, P}) B_secret_Kab: secret(B, 3, Kab, {A, B, P}) // Agreement properties strengthened with respect to Cas Cremers' models: // (a) we also verify agreement on the freshness data TNa, TNb // (b) we also verify agreement with the trusted third party // A_injective_agreement_B: iagree(A_4[A,B,P,Kab,TNa,Text5,TNb,Text7] -> B_4[A,B,P,Kab,TNa,Text5,TNb,Text7], {A, B, P}) // Injective agreement does not hold. See // isoiec_9798_2_5_special_TTP_bdkey for more information. B_non_injective_agreement_A: niagree(B_3[A,B,P,Kab,TNa,Text5] -> A_3[A,B,P,Kab,TNa,Text5], {A, B, P}) A_injective_agreement_P: iagree(A_2[A,B,P,Kab,TVPa,Text3] -> P_2[A,B,P,Kab,TVPa,Text3], {A, B, P}) // Injective agreement does not hold. See // isoiec_9798_2_5_special_TTP_bdkey for more information. B_non_injective_agreement_P: niagree(B_3[A,B,P,Kab,TNp,Text2] -> P_2[A,B,P,Kab,TNp,Text2], {A, B, P}) /****************************************************************************** * Protocol 6 ****************************************************************************** * * symmetric * ttp * five-pass * mutual * * Modeling notes: * - We send identity P in Step 4 in order for B to be able to lookup key k(B,P) * - Added additional identity to messages in Step 3 to avoid identity swapping. * * MPA Attack reported by Mathuria: * - Type flaw MPA when in parallel with Abadi-Needham protocol. */ protocol isoiec_9798_2_6_bdkey { text_1. -> B: Text1 1. B -> A: B, A, Rb, Text1 text_2. -> A: Text2 2. A -> P: A, P, Ra, Rb, B, Text2 text_3. -> P: Text3, Text4, Text5 3. P -> : P, A, Text5, {'isoiec_9798_2_6_enc_3_1', Ra, Kab, A, B, Text4}k[A,P] , {'isoiec_9798_2_6_enc_3_2', Rb, Kab, A, B, Text3}k[B,P] -> A: P, A, Text5, {'isoiec_9798_2_6_enc_3_1', Ra, Kab, A, B, Text4}k[A,P] , TokenPA_for_B text_4. -> A: Text6, Text7 4. A -> : A, B, Text7, P, TokenPA_for_B , {'isoiec_9798_2_6_enc_4', Rpa, Rb, Text6}Kab -> B: A, B, Text7, P, {'isoiec_9798_2_6_enc_3_2', Rb, Kab, A, B, Text3}k[B,P] , {'isoiec_9798_2_6_enc_4', Rpa, Rb, Text6}Kab text_5. -> B: Text8, Text9 5. B -> A: B, A, Text9, {'isoiec_9798_2_6_enc_5', Rb, Rpa, Text8}Kab } properties (of isoiec_9798_2_6_bdkey) P_secret_Kab: secret(P, -, Kab, {A, B, P}) A_secret_Kab: secret(A, 3, Kab, {A, B, P}) B_secret_Kab: secret(B, 4, Kab, {A, B, P}) // Agreement properties strengthened with respect to Cas Cremers' models: // (a) we also verify agreement on the freshness data // (b) we also verify agreement with the trusted third party // A_injective_agreement_B: iagree(A_5[A,B,P,Kab,Rpa,Rb,Text6,Text8] -> B_5[A,B,P,Kab,Rpa,Rb,Text6,Text8], {A, B, P}) B_injective_agreement_A: iagree(B_4[A,B,P,Kab,Rpa,Rb,Text6] -> A_4[A,B,P,Kab,Rpa,Rb,Text6], {A, B, P}) A_injective_agreement_P: iagree(A_3[A,B,P,Ra,Kab,Text4] -> P_3[A,B,P,Ra,Kab,Text4], {A, B, P}) B_injective_agreement_P: iagree(B_4[A,B,P,Rb,Kab,Text3] -> P_3[A,B,P,Rb,Kab,Text3], {A, B, P}) /****************************************************************************** * Protocol 5 (with the assumption that the TTP does not play other roles) ****************************************************************************** * * symmetric * ttp * four-pass * mutual * * Modeling notes: * - The use of TNb in message 4, as specified by the ISO standard, is * different from other models, in which it was TNa. * - We MUST assume that the trusted third party does not execute the A role. * Otherwise, some authentication properties break (see below). * - We send identity P in Step 3 in order for B to be able to lookup key k[B,P] */ protocol isoiec_9798_2_5_special_TTP_bdkey { leak_A. A -> : TVPa, TNa leak_B. B -> : TNb leak_P. P -> : TNp text_1. -> A: Text1 1. A -> P: A, P, TVPa, B, Text1 text_2. -> P: Text2, Text3, Text4 2. P -> : P, A, Text4, { 'isoiec_9798_2_5_special_TTP_enc_2_1', TVPa, Kab, B, Text3 }k[A,P] , { 'isoiec_9798_2_5_special_TTP_enc_2_2', TNp , Kab, A, Text2 }k[B,P] -> A: P, A, Text4, { 'isoiec_9798_2_5_special_TTP_enc_2_1', TVPa, Kab, B, Text3 }k[A,P] , TokenPA_for_B text_3. -> A: Text5, Text6 3. A -> : A, B, Text6, P, TokenPA_for_B , { 'isoiec_9798_2_5_special_TTP_enc_3', TNa, B, Text5 }Kab -> B: A, B, Text6, P, { 'isoiec_9798_2_5_special_TTP_enc_2_2', TNp, Kab, A, Text2 }k[B,P] , { 'isoiec_9798_2_5_special_TTP_enc_3', TNa, B, Text5 }Kab text_4. -> B: Text7, Text8 4. B -> A: B, A, Text8, { 'isoiec_9798_2_5_special_TTP_enc_4', TNb, A, Text7 }Kab } axiom (of isoiec_9798_2_5_special_TTP_bdkey) different_actors_A_P: premises "role(0) = A" "role(1) = P" "A#0 = P#1" imply "False" properties (of isoiec_9798_2_5_special_TTP_bdkey) P_secret_Kab: secret(P, -, Kab, {A, B, P}) A_secret_Kab: secret(A, 2, Kab, {A, B, P}) B_secret_Kab: secret(B, 3, Kab, {A, B, P}) // Agreement properties strengthened with respect to Cas Cremers' models: // (a) we also verify agreement on the freshness data TNa, TNb // (b) we also verify agreement with the trusted third party // // Note: If no axiom dependency is noted for a property below, then it can // be proven without the axiom. A_injective_agreement_B: iagree(A_4[A,B,P,Kab,TNa,Text5,TNb,Text7] -> B_4[A,B,P,Kab,TNa,Text5,TNb,Text7], {A, B, P}) // Depends on 'different_actors_A_P' // // NO injective agreement can be proven. There may be several B-threads // communicating with the same A-thread! Checking the 'TNb' timestamp in // later steps could be used to remove this problem, up to the clock // resolution. B_non_injective_agreement_A: niagree(B_3[A,B,P,Kab,TNa,Text5] -> A_3[A,B,P,Kab,TNa,Text5], {A, B, P}) // depends on 'different_actors_A_P' A_injective_agreement_P: iagree(A_2[A,B,P,Kab,TVPa,Text3] -> P_2[A,B,P,Kab,TVPa,Text3], {A, B, P}) // No injective agreement, as the TTP does not receive any message from 'B'. B_non_injective_agreement_P: niagree(B_3[A,B,P,Kab,TNp,Text2] -> P_2[A,B,P,Kab,TNp,Text2], {A, B, P}) /****************************************************************************** * Protocol 6 (with the assumption that the TTP does not play other roles) ****************************************************************************** * * symmetric * ttp * five-pass * mutual * * Modeling notes: * - We send identity P in Step 4 in order for B to be able to lookup key k[B,P] * - We MUST assume that the trusted third party does not execute any of the * other roles. Otherwise, some authentication properties break (see below). * * MPA Attack reported by Mathuria: * - Type flaw MPA when in parallel with Abadi-Needham protocol. */ protocol isoiec_9798_2_6_special_TTP_bdkey { text_1. -> B: Text1 1. B -> A: B, A, Rb, Text1 text_2. -> A: Text2 2. A -> P: A, P, Ra, Rb, B, Text2 text_3. -> P: Text3, Text4, Text5 3. P -> : P, A, Text5, {'isoiec_9798_2_6_special_TTP_enc_3_1', Ra, Kab, B, Text4}k[A,P] , {'isoiec_9798_2_6_special_TTP_enc_3_2', Rb, Kab, A, Text3}k[B,P] -> A: P, A, Text5, {'isoiec_9798_2_6_special_TTP_enc_3_1', Ra, Kab, B, Text4}k[A,P] , TokenPA_for_B text_4. -> A: Text6, Text7 4. A -> : A, B, Text7, P, TokenPA_for_B , {'isoiec_9798_2_6_special_TTP_enc_4', Rpa, Rb, Text6}Kab -> B: A, B, Text7, P, {'isoiec_9798_2_6_special_TTP_enc_3_2', Rb, Kab, A, Text3}k[B,P] , {'isoiec_9798_2_6_special_TTP_enc_4', Rpa, Rb, Text6}Kab text_5. -> B: Text8, Text9 5. B -> A: B, A, Text9, {'isoiec_9798_2_6_special_TTP_enc_5', Rb, Rpa, Text8}Kab } axiom (of isoiec_9798_2_6_special_TTP_bdkey) different_actors_A_P: premises "role(0) = A" "role(1) = P" "A#0 = P#1" imply "False" axiom (of isoiec_9798_2_6_special_TTP_bdkey) different_actors_B_P: premises "role(0) = B" "role(1) = P" "B#0 = P#1" imply "False" properties (of isoiec_9798_2_6_special_TTP_bdkey) P_secret_Kab: secret(P, -, Kab, {A, B, P}) A_secret_Kab: secret(A, 3, Kab, {A, B, P}) B_secret_Kab: secret(B, 4, Kab, {A, B, P}) // Agreement properties strengthened with respect to Cas Cremers' models: // (a) we also verify agreement on the freshness data // (b) we also verify agreement with the trusted third party // // Note: If no axiom dependency is noted for a property below, then it can // be proven without the axiom. // depends on 'different_actors_B_P' and 'different_actors_A_P' A_injective_agreement_B: iagree(A_5[A,B,P,Kab,Rpa,Rb,Text6,Text8] -> B_5[A,B,P,Kab,Rpa,Rb,Text6,Text8], {A, B, P}) // depends on 'different_actors_B_P' and 'different_actors_A_P' B_injective_agreement_A: iagree(B_4[A,B,P,Kab,Rpa,Rb,Text6] -> A_4[A,B,P,Kab,Rpa,Rb,Text6], {A, B, P}) // depends on 'different_actors_A_P A_injective_agreement_P: iagree(A_3[A,B,P,Ra,Kab,Text4] -> P_3[A,B,P,Ra,Kab,Text4], {A, B, P}) // depends on 'different_actors_B_P B_injective_agreement_P: iagree(B_4[A,B,P,Rb,Kab,Text3] -> P_3[A,B,P,Rb,Kab,Text3], {A, B, P}) end