// All protocols in a single file to test their parallel composition. // Author: Simon Meier // Created: 2013-03-21 // // Note that we have to specially deal with the 2_5 and 2_6 protocols, as // their automatically computed type invariants are not sound. We therefore // compose them manually and use a manual type invariant, which we derived // from the automatically computed one. These two manually composed protocols // can be found at the end of this file. // // Note also our proof checking automation that we implemented in Isabelle // suffers from a scaling problem when verifying the proof script resutling // ceritfying the correctness of the parallel composition of all protocols in // this file. We therefore do not include checking this file in the // regressions tests. theory isoiec_9798 begin /* // %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% // 2 - bdkey // %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% /* * 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. */ /****************************************************************************** * 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 (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}) // %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% // 2 - udkey // %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% /* * 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 unidirectional keys k(A,B) and all * optional identities dropped. * - 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. */ /****************************************************************************** * Protocol 1 ****************************************************************************** * * symmetric * one-pass * unilateral * * Note: the identity B is ommitted because a unidirectional key is used */ protocol isoiec_9798_2_1_udkey { leak_A. A -> : TNA text_1. -> A: Text1, Text2 1. A -> B: A, B, Text2, {'isoiec_9798_2_1_enc_1', TNA, 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_udkey) 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 is ommitted because a unidirectional key is used */ protocol isoiec_9798_2_2_udkey { 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, Text2}k(A,B) } property (of isoiec_9798_2_2_udkey) 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 are ommitted because a unidirectional key is used */ protocol isoiec_9798_2_3_udkey { 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, Text1 }k(A,B) text_2. -> B: Text3, Text4 2. B -> A: B, A, Text4, {'isoiec_9798_2_3_enc_2', TNB, 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_udkey) 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_2[A,B,TNA,Text1] -> A_1[A,B,TNA,Text1], {A, B}) /****************************************************************************** * Protocol 4 ****************************************************************************** * * symmetric * three-pass * mutual * * Note: the identities are ommitted because a unidirectional key is used * * In case (b), modeled here, the second key is reversed and the identities are * omitted in the ciphertexts. */ protocol isoiec_9798_2_4_udkey { 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, 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(B,A) } properties (of isoiec_9798_2_4_udkey) 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}) // %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% // 3 // %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% /* * Modeled from ISO/IEC 9798 * Modeler: Cas Cremers, Dec. 2010 * Adapted for scyther-proof: Simon Meier, Feb. 2011 * * Modeling notes: * - We allow the adversary to choose the content of all TextX fields. * - time-variant-parameters, time-stamps, and sequence numbers are * modeled by nonces leaked to the adversary at the start of a role. * - Given some pattern 'pkA', then the signature pattern 'sign{m}pkA' is * translated to the message '(m, {m}inv(pkA))' upon execution. */ /**************************************************************************** * Protocol 1 **************************************************************************** * * signature * one-pass * unilateral * * Modeling notes: * - we assume that pk(A) is already known to B */ protocol isoiec_9798_3_1 { leak_A. A -> : TNA text_1. -> A: Text1, Text2 1. A -> B: A, B, Text2, sign{'isoiec_9798_3_1_sig_1', TNA, B, Text1 }pk(A) } // No injective agreement here. properties (of isoiec_9798_3_1) B_non_injective_agreement: niagree(B_1[A,B,TNA,Text1] -> A_1[A,B,TNA,Text1], {A}) /**************************************************************************** * Protocol 2 **************************************************************************** * * signature * two-pass * unilateral * * Modeling notes: * - we assume that pk(A) is already known to B */ protocol isoiec_9798_3_2 { text_1. -> B: Text1 1. B -> A: B, A, Rb, Text1 text_2. -> A: Text2, Text3 2. A -> B: A, B, Text3, sign{'isoiec_9798_3_2_sig_2', Ra, Rb, B, Text2 }pk(A) } properties (of isoiec_9798_3_2) B_injective_agreement: iagree(B_2[A,B,Ra,Rb,Text2] -> A_2[A,B,Ra,Rb,Text2], {A}) /**************************************************************************** * Protocol 3 **************************************************************************** * * signature * two-pass * mutual * parallel * * Modeling notes: * - Here we only verify a sequential model of the protocol. * - We assume that the public keys are already predistributed. */ protocol isoiec_9798_3_3 { leak_A. A -> : TNA leak_B. B -> : TNB text_1. -> A: Text1, Text2 1. A -> B: A, B, Text2, sign{'isoiec_9798_3_3_sig_1', TNA, B, Text1 }pk(A) text_2. -> B: Text3, Text4 2. B -> A: A, B, Text4, sign{'isoiec_9798_3_3_sig_2', TNB, A, Text3 }pk(B) } // No injective agreement. It requires a forth and back message, which does // not exist for role B. For role 'A', we miss an opportunity for injective // authentication, as we could include 'TNA' in the second message exchange. properties (of isoiec_9798_3_3) A_non_injective_agreement: niagree(A_2[A,B,TNB,Text3] -> B_2[A,B,TNB,Text3], {B}) B_non_injective_agreement: niagree(B_1[A,B,TNA,Text1] -> A_1[A,B,TNA,Text1], {A}) /**************************************************************************** * Protocol 4 **************************************************************************** * * signature * three-pass * mutual * * Modeling notes: * - We assume that the public keys are already predistributed. */ protocol isoiec_9798_3_4 { text_1. -> B: Text1 1. B -> A: B, A, RB, Text1 text_2. -> A: Text2, Text3 2. A -> B: A, B, Text3, sign{'isoiec_9798_3_4_sig_1', RA, RB, B, Text2 }pk(A) text_3. -> B: Text4, Text5 3. B -> A: B, A, Text5, sign{'isoiec_9798_3_4_sig_2', RB, RA, A, Text4 }pk(B) } properties (of isoiec_9798_3_4) // The identity A in Step 3 is required for this property to hold. A_injective_agreement: iagree(A_3[A,B,RA,RB,Text2,Text4] -> B_3[A,B,RA,RB,Text2,Text4], {A,B}) // The identity B in Step 2 is required for this property to hold. B_injective_agreement: iagree(B_2[A,B,RA,RB,Text2] -> A_2[A,B,RA,RB,Text2], {A}) /**************************************************************************** * Protocol 5 **************************************************************************** * * signature * two-pass * mutual * parallel * * Modeling notes: * - unnecessary sequentialization in the model. * - we assume that the public keys are already predistributed. */ protocol isoiec_9798_3_5 { text_1. -> A: Text1 1. A -> B: A, B, RA, Text1 text_2. -> B: Text2 2. B -> A: B, A, RB, Text2 text_3. -> B: Text5, Text6 3. B -> A: B, A, Text6, sign{'isoiec_9798_3_5_sig_1', RB, RA, A, Text5 }pk(B) text_4. -> A: Text3, Text4 4. A -> B: A, B, Text4, sign{'isoiec_9798_3_5_sig_2', RA, RB, B, Text3 }pk(A) } properties (of isoiec_9798_3_5) // The identity A in Step 3 is required for this property to hold. A_injective_agreement: iagree(A_3[A,B,RA,RB,Text5] -> B_3[A,B,RA,RB,Text5], {B}) // The identity B in Step 4 is required for this property to hold. B_injective_agreement: iagree(B_4[A,B,RA,RB,Text3,Text5] -> A_4[A,B,RA,RB,Text3,Text5], {A,B}) /**************************************************************************** * Protocol 6 (Option 1) **************************************************************************** * * signature * ttp * five-pass * mutual * * A initiates and also communicates with T * * Modeling notes: * - We model the case where T sends the public keys instead of just verifying * the certificates; i.e., 'ResA = (A, pk(A))' and 'ResB = (B, pk(B))'. * - Option 1 and Option 2 must not share tags! */ protocol isoiec_9798_3_6_1 { text_1. -> A: Text1 1. A -> B: A, B, Ra, Text1 text_2. -> B: Text2, Text3 2. B -> : A, B, Ra, Rb, Text3, sign{'isoiec_9798_3_6_opt_1_sig_2', B, Ra, Rb, A, Text2}pk(B) -> A: A, B, Ra, Rb, Text3, TokenBA text_3. -> A: Text4 3. A -> T: A, T, Rpa, Rb, B, Text4 text_4. -> T: Text5, Text6, Text7 4. T -> : T, A, Text7, A, pk(A), B, pk(B), sign{'isoiec_9798_3_6_opt_1_sig_4_1', Rpa, B, pk(B), Text6}pk(T), sign{'isoiec_9798_3_6_opt_1_sig_4_2', Rb, A, pk(A), Text5}pk(T) -> A: T, A, Text7, A, pk(A), B, pkB, sign{'isoiec_9798_3_6_opt_1_sig_4_1', Rpa, B, pkB, Text6}pk(T), TokenTA_for_B // Here, A checks TokenBA against the public key pkB received from T. // As we lack support for additionally checked equalities, A sends a message // to itself encrypted with a fresh nonce to emulate the equality check. check_4_out. A -> : {'check_4', TokenBA }check_nonce_4 check_4_in. -> A: {'check_4', sign{'isoiec_9798_3_6_opt_1_sig_2', B, Ra, Rb, A, Text2}pkB }check_nonce_4 // Note: we additionally send T such that B knows which key to use for // checking TokenTA_for_B text_5. -> A: Text8, Text9 5. A -> : A, B, Text9, T, TokenTA_for_B, sign{'isoiec_9798_3_6_opt_1_sig_5', Rb, Ra, B, A, Text8}pk(A) -> B: A, B, Text9, T, sign{'isoiec_9798_3_6_opt_1_sig_4_2', Rb, A, pkA, Text5}pk(T), sign{'isoiec_9798_3_6_opt_1_sig_5', Rb, Ra, B, A, Text8}pkA } // All properties except hold injectively. NOTE: Investigate this // authentication "flaw" between Ra5 and Ra in role 'B'. properties (of isoiec_9798_3_6_1) A_injective_agreement: iagree(A_5[A,B,Ra,Rb,Text2] -> B_2[A,B,Ra,Rb,Text2], {B, T}) B_injective_agreement: iagree(B_5[A,B,Ra,Rb,Text8] -> A_5[A,B,Ra,Rb,Text8], {A, T}) // We additionally verify agreement of A and B with the TTP T. A_injective_agreement_T: iagree(A_5[B,T,Rpa,pkB ,Text6] -> T_4[B,T,Rpa,pk(B),Text6], {T}) B_injective_agreement_T: iagree(B_5[A,T,Rb,pkA ,Text5] -> T_4[A,T,Rb,pk(A),Text5], {T}) /**************************************************************************** * Protocol 6 (Option 2) **************************************************************************** * * signature * ttp * five-pass * mutual * * A initiates and also communicates with T * * Modeling notes: * - Option 1 and Option 2 must not share tags! * - We model the case where T sends the public keys instead of just verifying * the certificates; i.e., 'ResA = (A, pk(A))' and 'ResB = (B, pk(B))'. * - Our model might perform a few equality checks more than what is strictly * required by the standard. All of them are practically feasible and we * advise to implement them. We do not verify whether we the security * properties also hold with fewer equality checks. */ protocol isoiec_9798_3_6_2 { text_1. -> A: Text1 1. A -> B: A, B, Ra, Text1 text_2. -> B: Text2, Text3 2. B -> : A, B, Ra, Rb, Text3, sign{'isoiec_9798_3_6_opt_2_sig_2', B, Ra, Rb, A, Text2}pk(B) -> A: A, B, Ra, Rb, Text3, TokenBA text_3. -> A: Text4 3. A -> T: A, T, Rpa, Rb, B, Text4 // Note: Text6 is not used in Option 2 text_4. -> T: Text5, Text7 4. T -> : T, A, Text7, A, pk(A), B, pk(B), sign{ 'isoiec_9798_3_6_opt_2_sig_4', Rpa, Rb, A, pk(A), B, pk(B), Text5 }pk(T) -> A: T, A, Text7, A, pk(A), B, pkB, TokenTA // Here, A first checks TokenTA and then checks TokenBA against the public // key received from T. As we lack support for additionally checked // equalities, A sends a message to itself encrypted with a fresh nonce to // emulate the equality check. check_4_out. A -> : {'check_4', TokenTA, TokenBA }check_nonce_4 check_4_in. -> A: {'check_4', sign{'isoiec_9798_3_6_opt_2_sig_4', Rpa, Rb, A, pkA, B, pkB, Text5 }pk(T), sign{'isoiec_9798_3_6_opt_2_sig_2', B, Ra, Rb, A, Text2}pkB }check_nonce_4 // Note: we additionally send T such that B knows which key to use for // checking TokenTA text_5. -> A: Text8, Text9 5. A -> : A, B, Rpa, Text9, T, TokenTA, sign{'isoiec_9798_3_6_opt_2_sig_5', Rb, Ra, B, A, Text8}pk(A) -> B: A, B, Rpa, Text9, T, sign{'isoiec_9798_3_6_opt_2_sig_4', Rpa, Rb, A, pkA, B, pkB, Text5 }pk(T), sign{'isoiec_9798_3_6_opt_2_sig_5', Rb, Ra, B, A, Text8}pkA } properties (of isoiec_9798_3_6_2) // Note that we do not get agreement on T! A_injective_agreement: iagree(A_5[A,B,Ra,Rb,Text2] -> B_2[A,B,Ra,Rb,Text2], {B, T}) B_injective_agreement: iagree(B_5[A,B,Ra,Rb,Text8] -> A_5[A,B,Ra,Rb,Text8], {A, T}) // We additionally verify agreement of A and B with the TTP T A_injective_agreement_T: iagree(A_5[A,B,T,Rpa,Rb,pkA ,pkB ,Text5] -> T_4[A,B,T,Rpa,Rb,pk(A),pk(B),Text5], {T}) B_injective_agreement_T: iagree(B_5[A,B,T,Rpa,Rb,pkA ,pkB ,Text5] -> T_4[A,B,T,Rpa,Rb,pk(A),pk(B),Text5], {T}) /**************************************************************************** * Protocol 7 (Option 1) **************************************************************************** * * signature * ttp * five-pass * mutual * * B initiates and A communicates with T * * Modeling notes: * - Option 1 and Option 2 must not share tags! * - We model the case where T sends the public keys instead of just verifying * the certificates; i.e., 'ResA = (A, pk(A))' and 'ResB = (B, pk(B))'. * - Our model might perform a few equality checks more than what is strictly * required by the standard. All of them are practically feasible and we * advise to implement them. We do not verify whether we the security * properties also hold with fewer equality checks. */ protocol isoiec_9798_3_7_1 { text_1. -> B: Text1 1. B -> A: B, A, Rb, Text1 text_2. -> A: Text2 2. A -> T: A, T, Rpa, Rb, A, B, Text2 text_3. -> T: Text3, Text4, Text5 3. T -> : T, A, Text5, A, pk(A), B, pk(B), sign{ 'isoiec_9798_3_7_opt_1_sig_3_1', Rpa, B, pk(B), Text4 }pk(T), sign{ 'isoiec_9798_3_7_opt_1_sig_3_2', Rb, A, pk(A), Text3 }pk(T) -> A: T, A, Text5, A, pk(A), B, pkB, sign{ 'isoiec_9798_3_7_opt_1_sig_3_1', Rpa, B, pkB, Text4 }pk(T), TokenTA_for_B // Note: we additionally send T such that B knows which key to use for // checking TokenTA text_4. -> A: Text6, Text7 4. A -> : A, B, Rpa, Text7, T, TokenTA_for_B, sign{'isoiec_9798_3_7_opt_1_sig_4', Rb, Ra, B, A, Text6}pk(A) -> B: A, B, Rpa, Text9, T, sign{'isoiec_9798_3_7_opt_1_sig_3_2', Rb, A, pkA, Text3}pk(T), sign{'isoiec_9798_3_7_opt_1_sig_4', Rb, Ra, B, A, Text6}pkA text_5. -> B: Text8, Text9 5. B -> : A, B, Ra, Rb, Text9, sign{'isoiec_9798_3_7_opt_1_sig_5', Ra, Rb, A, B, Text8}pk(B) -> A: A, B, Ra, Rb, Text9, sign{'isoiec_9798_3_7_opt_1_sig_5', Ra, Rb, A, B, Text8}pkB } properties (of isoiec_9798_3_7_1) // Note that we do not get agreement on T! A_injective_agreement: iagree(A_5[A,B,Ra,Rb,Text8] -> B_5[A,B,Ra,Rb,Text8], {B, T}) B_injective_agreement: iagree(B_4[A,B,Ra,Rb,Text6] -> A_4[A,B,Ra,Rb,Text6], {A, T}) // We additionally verify agreement of A and B with the TTP T A_injective_agreement_T: iagree(A_3[B,T,Rpa,pkB,Text4] -> T_3[B,T,Rpa,pk(B),Text4], {T}) B_injective_agreement_T: iagree(B_4[A,T,Rb,pkA,Text3] -> T_3[A,T,Rb,pk(A),Text3], {T}) /**************************************************************************** * Protocol 7 (Option 2) **************************************************************************** * * signature * ttp * five-pass * mutual * * B initiates and A communicates with T * * Modeling notes: * - Option 1 and Option 2 must not share tags! * - We model the case where T sends the public keys instead of just verifying * the certificates; i.e., 'ResA = (A, pk(A))' and 'ResB = (B, pk(B))'. * - Our model might perform a few equality checks more than what is strictly * required by the standard. All of them are practically feasible and we * advise to implement them. We do not verify whether we the security * properties also hold with fewer equality checks. */ protocol isoiec_9798_3_7_2 { text_1. -> B: Text1 1. B -> A: B, A, Rb, Text1 text_2. -> A: Text2 2. A -> T: A, T, Rpa, Rb, A, B, Text2 // Note: Text4 is not used in Option 2 text_3. -> T: Text3, Text5 3. T -> : T, A, Text5, A, pk(A), B, pk(B), sign{ 'isoiec_9798_3_7_opt_2_sig_3', Rpa, Rb, A, pk(A), B, pk(B), Text3 }pk(T) -> A: T, A, Text5, A, pk(A), B, pkB, TokenTA // Here, A checks TokenTA. As we lack support for additionally checked // equalities, A sends a message to itself encrypted with a fresh nonce to // emulate the equality check. check_3_out. A -> : {'check_4', TokenTA }check_nonce_4 check_3_in. -> A: {'check_4', sign{'isoiec_9798_3_7_opt_2_sig_3', Rpa, Rb, A, pkA, B, pkB, Text3 }pk(T) }check_nonce_4 // Note: we additionally send T such that B knows which key to use for // checking TokenTA text_4. -> A: Text6, Text7 4. A -> : A, B, Rpa, Text7, T, TokenTA, sign{'isoiec_9798_3_7_opt_2_sig_4', Rb, Ra, B, A, Text6}pk(A) -> B: A, B, Rpa, Text9, T, sign{'isoiec_9798_3_7_opt_2_sig_3', Rpa, Rb, A, pkA, B, pkB, Text3 }pk(T), sign{'isoiec_9798_3_7_opt_2_sig_4', Rb, Ra, B, A, Text6}pkA text_5. -> B: Text8, Text9 5. B -> : A, B, Ra, Rb, Text9, sign{'isoiec_9798_3_7_opt_2_sig_5', Ra, Rb, A, B, Text8}pk(B) -> A: A, B, Ra, Rb, Text9, sign{'isoiec_9798_3_7_opt_2_sig_5', Ra, Rb, A, B, Text8}pkB } properties (of isoiec_9798_3_7_2) A_injective_agreement: iagree(A_5[A,B,Ra,Rb,Text8] -> B_5[A,B,Ra,Rb,Text8], {B, T}) B_injective_agreement: iagree(B_4[A,B,Ra,Rb,Text6] -> A_4[A,B,Ra,Rb,Text6], {A, T}) // We additionally verify agreement of A and B with the TTP T A_injective_agreement_T: iagree(A_4[A,B,T,Rpa,Rb,pkA ,pkB ,Text3] -> T_3[A,B,T,Rpa,Rb,pk(A),pk(B),Text3], {T}) B_injective_agreement_T: iagree(B_4[A,B,T,Rpa,Rb,pkA ,pkB ,Text3] -> T_3[A,B,T,Rpa,Rb,pk(A),pk(B),Text3], {T}) // %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% // 4 - bdkey // %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% /* * Modeled from ISO/IEC 9798-4 * Modeler: Cas Cremers, Dec. 2010, Feb. 2011. * Ported to scyther-proof: Simon Meier, Feb. 2011. * * Modeling notes: * - Variant of ISO/IEC 9798-4 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. * - The keyed CCF (f_kab(x)) is modeled as h(('CCF', k[a,b]), x) * */ /****************************************************************************** * Protocol 1 ****************************************************************************** * * ccf * unilateral * one-pass */ protocol isoiec_9798_4_1_bdkey { leak_A. A -> : TNA text_1. -> A: Text1, Text2 1. A -> B: A, B, TNA, Text2, Text1, h(('CCF', k[A,B]), ('isoiec_9798_4_1_ccf_1', TNA, B, Text1)) } // Does not hold injectively. properties (of isoiec_9798_4_1_bdkey) B_non_injective_agreement: niagree(B_1[A,B,TNA,Text1] -> A_1[A,B,TNA,Text1], {A, B}) /****************************************************************************** * Protocol 2 ****************************************************************************** * * ccf * unilateral * two-pass */ protocol isoiec_9798_4_2_bdkey { text_1. -> B: Text1 1. B -> A: B, A, Rb, Text1 text_2. -> A: Text2, Text3 2. A -> B: A, B, Text3, Rb, Text2, h(('CCF', k[A,B]), ('isoiec_9798_4_2_ccf_2', Rb, B, Text2)) } properties (of isoiec_9798_4_2_bdkey) B_injective_agreement: iagree(B_2[A,B,Rb,Text2] -> A_2[A,B,Rb,Text2], {A, B}) /****************************************************************************** * Protocol 3 ****************************************************************************** * * ccf * mutual * two-pass */ protocol isoiec_9798_4_3_bdkey { leak_A. A -> : TNa leak_B. B -> : TNb text_1. -> A: Text1, Text2 1. A -> B: A, B, TNa, Text2, Text1, h(('CCF', k[A,B]), ('isoiec_9798_4_3_ccf_1', TNa, B, Text1)) text_2. -> B: Text3, Text4 2. B -> A: B, A, TNb, Text4, Text3, h(('CCF', k[A,B]), ('isoiec_9798_4_3_ccf_2', TNb, A, Text3)) } // Does not hold injectively. Missing an opportunity to get injective // agreement for role A by adding TNa in the second message. properties (of isoiec_9798_4_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 ****************************************************************************** * * ccf * mutual * three-pass */ protocol isoiec_9798_4_4_bdkey { text_1. -> B: Text1 1. B -> A: B, A, Rb, Text1 text_2. -> A: Text2, Text3 2. A -> B: A, B, Ra, Text3, Text2, h(('CCF', k[A,B]), ('isoiec_9798_4_4_ccf_2', Ra, Rb, B, Text2)) text_3. -> B: Text4, Text5 3. B -> A: B, A, Text5, Text4, h(('CCF', k[A,B]), ('isoiec_9798_4_4_ccf_3', Rb, Ra, Text4)) } properties (of isoiec_9798_4_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}) // %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% // 4 - udkey // %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% /* * Modeled from ISO/IEC 9798-4 * Modeler: Cas Cremers, Dec. 2010, Feb. 2011. * Ported to scyther-proof: Simon Meier, Feb. 2011. * * Modeling notes: * - Variant of ISO/IEC 9798-4 with unidirectional keys k(A,B) and * identities dropped if possible. * - 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. * - The keyed CCF (f_kab(x)) is modeled as h(('CCF', k(a,b)), x) */ /****************************************************************************** * Protocol 1 ****************************************************************************** * * ccf * unilateral * one-pass */ protocol isoiec_9798_4_1_udkey { leak_A. A -> : TNA text_1. -> A: Text1, Text2 1. A -> B: A, B, TNA, Text2, Text1, h(('CCF', k(A,B)), ('isoiec_9798_4_1_ccf_1', TNA, Text1)) } // No injective agreement here, as the message from A can be received by // multiple 'B's. properties (of isoiec_9798_4_1_udkey) B_non_injective_agreement: niagree(B_1[A,B,TNA,Text1] -> A_1[A,B,TNA,Text1], {A, B}) /****************************************************************************** * Protocol 2 ****************************************************************************** * * ccf * unilateral * two-pass */ protocol isoiec_9798_4_2_udkey { text_1. -> B: Text1 1. B -> A: B, A, Rb, Text1 text_2. -> A: Text2, Text3 2. A -> B: A, B, Text3, Rb, Text2, h(('CCF', k(A,B)), ('isoiec_9798_4_2_ccf_2', Rb, Text2)) } properties (of isoiec_9798_4_2_udkey) B_injective_agreement: iagree(B_2[A,B,Rb,Text2] -> A_2[A,B,Rb,Text2], {A, B}) /****************************************************************************** * Protocol 3 ****************************************************************************** * * ccf * mutual * two-pass */ protocol isoiec_9798_4_3_udkey { leak_A. A -> : TNa leak_B. B -> : TNb text_1. -> A: Text1, Text2 1. A -> B: A, B, TNa, Text2, Text1, h(('CCF', k(A,B)), ('isoiec_9798_4_3_ccf_1', TNa, Text1)) text_2. -> B: Text3, Text4 2. B -> A: B, A, TNb, Text4, Text3, h(('CCF', k(A,B)), ('isoiec_9798_4_3_ccf_2', TNb, Text3)) } // The following properties do not hold injectively. This protocols misses a // simple opportunity to get injective agreement for role A by adding TNa in // the second message. properties (of isoiec_9798_4_3_udkey) 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 ****************************************************************************** * * ccf * mutual * three-pass */ protocol isoiec_9798_4_4_udkey { text_1. -> B: Text1 1. B -> A: B, A, Rb, Text1 text_2. -> A: Text2, Text3 2. A -> B: A, B, Ra, Text3, Text2, h(('CCF', k(A,B)), ('isoiec_9798_4_4_ccf_2', Ra, Rb, Text2)) text_3. -> B: Text4, Text5 3. B -> A: B, A, Text5, Text4, h(('CCF', k(A,B)), ('isoiec_9798_4_4_ccf_3', Rb, Ra, Text4)) } properties (of isoiec_9798_4_4_udkey) 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}) // %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% // The 2_5 and 2_6 protocols need manual type annotations to make the parallel // composition proof go through. Therefore, we have to define // %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% /****************************************************************************** * Protocol 5 (udkey and bdkey variants composed in parallel) ****************************************************************************** * * 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 send identity P in Step 3 in order for B to be able to lookup key k(B,P) */ protocol isoiec_9798_2_5 { // original protocol: isoiec_9798_2_5_bdkey leakA. A -> : TVPa, TNa leakB. B -> : TNb leakP. P -> : TNp text1. -> A: Text1 1. A -> P: A, P, TVPa, B, Text1 text2. -> P: Text2, Text3, Text4 2. P -> : P, A, Text4, { 'isoiec_9798_2_5_enc_2_1', TVPa, Kab, B, Text3 }k(A,P) , { 'isoiec_9798_2_5_enc_2_2', TNp , Kab, A, Text2 }k(B,P) -> A: P, A, Text4, { 'isoiec_9798_2_5_enc_2_1', TVPa, Kab, B, Text3 }k(A,P) , TokenPA_for_B text3. -> 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, Text2 }k(B,P) , { 'isoiec_9798_2_5_enc_3', TNa, B, Text5 }Kab text4. -> B: Text7, Text8 4. B -> A: B, A, Text8, { 'isoiec_9798_2_5_enc_4', TNb, A, Text7 }Kab // original protocol: isoiec_9798_2_5_bdkey leakA. Abd -> : TVPa, TNa leakB. Bbd -> : TNb leakP. Pbd -> : TNp text1. -> Abd: Text1 1. Abd -> Pbd: Abd, Pbd, TVPa, Bbd, Text1 text2. -> Pbd: Text2, Text3, Text4 2. Pbd -> : Pbd, Abd, Text4, { 'isoiec_9798_2_5_enc_2_1', TVPa, Kab, Abd, Bbd, Text3 }k[Abd,Pbd] , { 'isoiec_9798_2_5_enc_2_2', TNp , Kab, Abd, Bbd, Text2 }k[Bbd,Pbd] -> Abd: Pbd, Abd, Text4, { 'isoiec_9798_2_5_enc_2_1', TVPa, Kab, Abd, Bbd, Text3 }k[Abd,Pbd] , TokenPA_for_B text3. -> Abd: Text5, Text6 3. Abd -> : Abd, Bbd, Text6, Pbd, TokenPA_for_B , { 'isoiec_9798_2_5_enc_3', TNa, Bbd, Text5 }Kab -> Bbd: Abd, Bbd, Text6, Pbd, { 'isoiec_9798_2_5_enc_2_2', TNp, Kab, Abd, Bbd, Text2 }k[Bbd,Pbd] , { 'isoiec_9798_2_5_enc_3', TNa, Bbd, Text5 }Kab text4. -> Bbd: Text7, Text8 4. Bbd -> Abd: Bbd, Abd, Text8, { 'isoiec_9798_2_5_enc_4', TNb, Abd, Text7 }Kab } property (of isoiec_9798_2_5) typing_2_5: "Abd@Bbd :: Known(Bbd_3) Abd@Pbd :: Known(Pbd_1) A@B :: Known(B_3) A@P :: Known(P_1) Bbd@Pbd :: Known(Pbd_1) B@P :: Known(P_1) B@P :: Known(P_1) Kab@Abd :: (Known(Abd_2) | Kab@Pbd) Kab@Bbd :: (Known(Bbd_3) | Kab@Pbd) Kab@A :: (Known(A_2) | Kab@P) Kab@B :: (Known(B_3) | Kab@P) Pbd@Bbd :: Known(Bbd_3) P@B :: Known(B_3) // The following four lines are what is wrong in the automatically composed // type annotation. TNa@Bbd :: (Known(Bbd_3) | TNa@A | TNa@Abd) TNa@B :: (Known(B_3) | TNa@A | TNa@Abd) TNb@Abd :: (Known(Abd_4) | TNb@B | TNb@Bbd) TNb@A :: (Known(A_4) | TNb@B | TNb@Bbd) TNp@Bbd :: (Known(Bbd_3) | TNp@Pbd) TNp@B :: (Known(B_3) | TNp@P) TVPa@Pbd :: Known(Pbd_1) TVPa@P :: Known(P_1) Text1@Abd :: Known(Abd_text1) Text1@Pbd :: Known(Pbd_1) Text1@A :: Known(A_text1) Text1@P :: Known(P_1) Text2@Bbd :: Known(Bbd_3) Text2@Pbd :: Known(Pbd_text2) Text2@B :: Known(B_3) Text2@P :: Known(P_text2) Text3@Abd :: Known(Abd_2) Text3@Pbd :: Known(Pbd_text2) Text3@A :: Known(A_2) Text3@P :: Known(P_text2) Text4@Abd :: Known(Abd_2) Text4@Pbd :: Known(Pbd_text2) Text4@A :: Known(A_2) Text4@P :: Known(P_text2) Text5@Abd :: Known(Abd_text3) Text5@Bbd :: Known(Bbd_3) Text5@A :: Known(A_text3) Text5@B :: Known(B_3) Text6@Abd :: Known(Abd_text3) Text6@Bbd :: Known(Bbd_3) Text6@A :: Known(A_text3) Text6@B :: Known(B_3) Text7@Abd :: Known(Abd_4) Text7@Bbd :: Known(Bbd_text4) Text7@A :: Known(A_4) Text7@B :: Known(B_text4) Text8@Abd :: Known(Abd_4) Text8@Bbd :: Known(Bbd_text4) Text8@A :: Known(A_4) Text8@B :: Known(B_text4) TokenPA_for_B@Abd :: Known(Abd_2) TokenPA_for_B@A :: Known(A_2)" properties (of isoiec_9798_2_5) // udkey variant 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}) // Injectivity agreement does not hold. See // // 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}) 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}) properties (of isoiec_9798_2_5) // bdkey variant Pbd_secret_Kab: secret(Pbd, -, Kab, {Abd, Bbd, Pbd}) Abd_secret_Kab: secret(Abd, 2, Kab, {Abd, Bbd, Pbd}) Bbd_secret_Kab: secret(Bbd, 3, Kab, {Abd, Bbd, Pbd}) // 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 // Abd_injective_agreement_Bbd: iagree(Abd_4[Abd,Bbd,Pbd,Kab,TNa,Text5,TNb,Text7] -> Bbd_4[Abd,Bbd,Pbd,Kab,TNa,Text5,TNb,Text7], {Abd, Bbd, Pbd}) // Injective agreement does not hold. See // isoiec_9798_2_5_special_TTP_bdkey for more information. Bbd_non_injective_agreement_Abd: niagree(Bbd_3[Abd,Bbd,Pbd,Kab,TNa,Text5] -> Abd_3[Abd,Bbd,Pbd,Kab,TNa,Text5], {Abd, Bbd, Pbd}) Abd_injective_agreement_Pbd: iagree(Abd_2[Abd,Bbd,Pbd,Kab,TVPa,Text3] -> Pbd_2[Abd,Bbd,Pbd,Kab,TVPa,Text3], {Abd, Bbd, Pbd}) // Injective agreement does not hold. See // isoiec_9798_2_5_special_TTP_bdkey for more information. Bbd_non_injective_agreement_Pbd: niagree(Bbd_3[Abd,Bbd,Pbd,Kab,TNp,Text2] -> Pbd_2[Abd,Bbd,Pbd,Kab,TNp,Text2], {Abd, Bbd, Pbd}) */ /****************************************************************************** * 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) * * MPA Attack reported by Mathuria: * - Type flaw MPA when in parallel with Abadi-Needham protocol. */ protocol isoiec_9798_2_6 { // original protocol: isoiec_9798_2_6_udkey text1. -> B: Text1 1. B -> A: B, A, Rb, Text1 text2. -> A: Text2 2. A -> P: A, P, Ra, Rb, B, Text2 text3. -> P: Text3, Text4, Text5 3. P -> : P, A, Text5, {'isoiec_9798_2_6_enc_3_1', Ra, Kab, B, Text4}k(A,P) , {'isoiec_9798_2_6_enc_3_2', Rb, Kab, A, Text3}k(B,P) -> A: P, A, Text5, {'isoiec_9798_2_6_enc_3_1', Ra, Kab, B, Text4}k(A,P) , TokenPA_for_B text4. -> 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, Text3}k(B,P) , {'isoiec_9798_2_6_enc_4', Rpa, Rb, Text6}Kab text5. -> B: Text8, Text9 5. B -> A: B, A, Text9, {'isoiec_9798_2_6_enc_5', Rb, Rpa, Text8}Kab //original protocol isoiec_9798_2_6_bdkey text1. -> Bbd: Text1 1. Bbd -> Abd: Bbd, Abd, Rb, Text1 text2. -> Abd: Text2 2. Abd -> Pbd: Abd, Pbd, Ra, Rb, Bbd, Text2 text3. -> Pbd: Text3, Text4, Text5 3. Pbd -> : Pbd, Abd, Text5, {'isoiec_9798_2_6_enc_3_1', Ra, Kab, Abd, Bbd, Text4}k[Abd,Pbd] , {'isoiec_9798_2_6_enc_3_2', Rb, Kab, Abd, Bbd, Text3}k[Bbd,Pbd] -> Abd: Pbd, Abd, Text5, {'isoiec_9798_2_6_enc_3_1', Ra, Kab, Abd, Bbd, Text4}k[Abd,Pbd] , TokenPA_for_B text4. -> Abd: Text6, Text7 4. Abd -> : Abd, Bbd, Text7, Pbd, TokenPA_for_B , {'isoiec_9798_2_6_enc_4', Rpa, Rb, Text6}Kab -> Bbd: Abd, Bbd, Text7, Pbd, {'isoiec_9798_2_6_enc_3_2', Rb, Kab, Abd, Bbd, Text3}k[Bbd,Pbd] , {'isoiec_9798_2_6_enc_4', Rpa, Rb, Text6}Kab text5. -> Bbd: Text8, Text9 5. Bbd -> Abd: Bbd, Abd, Text9, {'isoiec_9798_2_6_enc_5', Rb, Rpa, Text8}Kab } property (of isoiec_9798_2_6) typing_2_6: "Abd@Pbd :: Known(Pbd_2) A@P :: Known(P_2) Bbd@Abd :: Known(Abd_1) Bbd@Pbd :: Known(Pbd_2) B@A :: Known(A_1) B@P :: Known(P_2) Kab@Abd :: (Known(Abd_3) | Kab@Pbd) Kab@Bbd :: (Known(Bbd_4) | Kab@Pbd) Kab@A :: (Known(A_3) | Kab@P) Kab@B :: (Known(B_4) | Kab@P) Pbd@Bbd :: Known(Bbd_4) P@B :: Known(B_4) Ra@Pbd :: Known(Pbd_2) Ra@P :: Known(P_2) Rb@Abd :: Known(Abd_1) Rb@Pbd :: Known(Pbd_2) Rb@A :: Known(A_1) Rb@P :: Known(P_2) // The following two lines are different from the automatically computed // type invariant for the composed protocols. Rpa@Bbd :: (Known(Bbd_4) | Rpa@A | Rpa@Abd) Rpa@B :: (Known(B_4) | Rpa@A | Rpa@Abd) Text1@Abd :: Known(Abd_1) Text1@Bbd :: Known(Bbd_text1) Text1@A :: Known(A_1) Text1@B :: Known(B_text1) Text2@Abd :: Known(Abd_text2) Text2@Pbd :: Known(Pbd_2) Text2@A :: Known(A_text2) Text2@P :: Known(P_2) Text3@Bbd :: Known(Bbd_4) Text3@Pbd :: Known(Pbd_text3) Text3@B :: Known(B_4) Text3@P :: Known(P_text3) Text4@Abd :: Known(Abd_3) Text4@Pbd :: Known(Pbd_text3) Text4@A :: Known(A_3) Text4@P :: Known(P_text3) Text5@Abd :: Known(Abd_3) Text5@Pbd :: Known(Pbd_text3) Text5@A :: Known(A_3) Text5@P :: Known(P_text3) Text6@Abd :: Known(Abd_text4) Text6@Bbd :: Known(Bbd_4) Text6@A :: Known(A_text4) Text6@B :: Known(B_4) Text7@Abd :: Known(Abd_text4) Text7@Bbd :: Known(Bbd_4) Text7@A :: Known(A_text4) Text7@B :: Known(B_4) Text8@Abd :: Known(Abd_5) Text8@Bbd :: Known(Bbd_text5) Text8@A :: Known(A_5) Text8@B :: Known(B_text5) Text9@Abd :: Known(Abd_5) Text9@Bbd :: Known(Bbd_text5) Text9@A :: Known(A_5) Text9@B :: Known(B_text5) TokenPA_for_B@Abd :: Known(Abd_3) TokenPA_for_B@A :: Known(A_3)" /* properties (of isoiec_9798_2_6) //udkey variant 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}) properties (of isoiec_9798_2_6) //bdkey variant Pbd_secret_Kab: secret(Pbd, -, Kab, {Abd, Bbd, Pbd}) Abd_secret_Kab: secret(Abd, 3, Kab, {Abd, Bbd, Pbd}) Bbd_secret_Kab: secret(Bbd, 4, Kab, {Abd, Bbd, Pbd}) // 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 // Abd_injective_agreement_Bbd: iagree(Abd_5[Abd,Bbd,Pbd,Kab,Rpa,Rb,Text6,Text8] -> Bbd_5[Abd,Bbd,Pbd,Kab,Rpa,Rb,Text6,Text8], {Abd, Bbd, Pbd}) Bbd_injective_agreement_Abd: iagree(Bbd_4[Abd,Bbd,Pbd,Kab,Rpa,Rb,Text6] -> Abd_4[Abd,Bbd,Pbd,Kab,Rpa,Rb,Text6], {Abd, Bbd, Pbd}) Abd_injective_agreement_Pbd: iagree(Abd_3[Abd,Bbd,Pbd,Ra,Kab,Text4] -> Pbd_3[Abd,Bbd,Pbd,Ra,Kab,Text4], {Abd, Bbd, Pbd}) Bbd_injective_agreement_Pbd: iagree(Bbd_4[Abd,Bbd,Pbd,Rb,Kab,Text3] -> Pbd_3[Abd,Bbd,Pbd,Rb,Kab,Text3], {Abd, Bbd, Pbd}) */ end