/* * 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. */ theory isoiec_9798_3 begin /**************************************************************************** * 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) } 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) // Note: for this agreement property the identity B must not be dropped B_non_injective_agreement: niagree(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) } 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_non_injective_agreement: niagree(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_non_injective_agreement: niagree(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_non_injective_agreement: niagree(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_non_injective_agreement: niagree(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), // Note: the standard does not require to check that 'Ra5 = Ra'! sign{'isoiec_9798_3_6_opt_1_sig_5', Rb, Ra5, B, A, Text8}pkA } properties (of isoiec_9798_3_6_1) A_non_injective_agreement: niagree(A_5[A,B,Ra,Rb,Text2] -> B_2[A,B,Ra,Rb,Text2], {B, T}) // Possible authentication FLAW: // We do NOT get agreement on Ra because the standard does not require B to // check its occurence in the signature from Step 5 to be equal with the // one in Step 2. // // FIXME: What are the consequences? B_non_injective_agreement: niagree(B_5[A,B,Ra5,Rb,Text8] -> A_5[A,B,Ra,Rb,Text8], {A, T}) // We additionally verify agreement of A and B with the TTP T. A_non_injective_agreement_T: niagree(A_5[B,T,Rpa,pkB ,Text6] -> T_4[B,T,Rpa,pk(B),Text6], {T}) B_non_injective_agreement_T: niagree(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))'. FIXME: Compare equality checks done here to what is prescribed in the standard. We probably do a few more => there may be attacks on the standard. We probably also shouldn't check the public keys delivered by T. */ 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), // Note: the standard does not require to check that 'Ra5 = Ra'! sign{'isoiec_9798_3_6_opt_2_sig_5', Rb, Ra5, B, A, Text8}pkA } properties (of isoiec_9798_3_6_2) // Note that we do not get agreement on T! A_non_injective_agreement: niagree(A_5[A,B,Ra,Rb,Text2] -> B_2[A,B,Ra,Rb,Text2], {B, T}) // Possible authentication FLAW: // We do NOT get agreement on Ra because the standard does not require B to // check its occurence in the signature from Step 5 to be equal with the // one in Step 2. // // FIXME: What are the consequences? B_non_injective_agreement: niagree(B_5[A,B,Ra5,Rb,Text8] -> A_5[A,B,Ra,Rb,Text8], {A, T}) // We additionally verify agreement of A and B with the TTP T A_non_injective_agreement_T: niagree(A_5[A,B,T,Rpa,Rb,pkA ,pkB ,Text5] -> T_4[A,B,T,Rpa,Rb,pk(A),pk(B),Text5], {T}) B_non_injective_agreement_T: niagree(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))'. FIXME: Compare equality checks done here to what is prescribed in the standard. We probably do a few more => there may be attacks on the standard. */ 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_non_injective_agreement: niagree(A_5[A,B,Ra,Rb,Text8] -> B_5[A,B,Ra,Rb,Text8], {B, T}) B_non_injective_agreement: niagree(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_non_injective_agreement_T: niagree(A_3[B,T,Rpa,pkB,Text4] -> T_3[B,T,Rpa,pk(B),Text4], {T}) B_non_injective_agreement_T: niagree(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))'. FIXME: Compare equality checks done here to what is prescribed in the standard. We probably do a few more => there may be attacks on the standard. */ 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_non_injective_agreement: niagree(A_5[A,B,Ra,Rb,Text8] -> B_5[A,B,Ra,Rb,Text8], {B, T}) B_non_injective_agreement: niagree(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_non_injective_agreement_T: niagree(A_4[A,B,T,Rpa,Rb,pkA ,pkB ,Text3] -> T_3[A,B,T,Rpa,Rb,pk(A),pk(B),Text3], {T}) B_non_injective_agreement_T: niagree(B_4[A,B,T,Rpa,Rb,pkA ,pkB ,Text3] -> T_3[A,B,T,Rpa,Rb,pk(A),pk(B),Text3], {T}) end