scyther-proof-0.3.0: data/examples/iso9798/isoiec-9798-2-bdkey.spthy
/*
* 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]
}
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_non_injective_agreement:
niagree(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]
}
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_non_injective_agreement:
niagree(A_3[A,B,RA,RB,Text2,Text4] -> B_3[A,B,RA,RB,Text2,Text4], {A, B})
B_non_injective_agreement:
niagree(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_non_injective_agreement_B:
niagree(A_4[A,B,P,Kab,TNa,Text5,TNb,Text7] -> B_4[A,B,P,Kab,TNa,Text5,TNb,Text7], {A, B, P})
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_non_injective_agreement_P:
niagree(A_2[A,B,P,Kab,TVPa,Text3] -> P_2[A,B,P,Kab,TVPa,Text3], {A, B, P})
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_non_injective_agreement_B:
niagree(A_5[A,B,P,Kab,Rpa,Rb,Text6,Text8] -> B_5[A,B,P,Kab,Rpa,Rb,Text6,Text8], {A, B, P})
B_non_injective_agreement_A:
niagree(B_4[A,B,P,Kab,Rpa,Rb,Text6] -> A_4[A,B,P,Kab,Rpa,Rb,Text6], {A, B, P})
A_non_injective_agreement_P:
niagree(A_3[A,B,P,Ra,Kab,Text4] -> P_3[A,B,P,Ra,Kab,Text4], {A, B, P})
B_non_injective_agreement_P:
niagree(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 for a property below, then it can be proven
// without the axiom.
A_non_injective_agreement_B:
niagree(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'
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_non_injective_agreement_P:
niagree(A_2[A,B,P,Kab,TVPa,Text3] -> P_2[A,B,P,Kab,TVPa,Text3], {A, B, P})
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 for a property below, then it can be proven
// without the axiom.
// depends on 'different_actors_B_P' and 'different_actors_A_P'
A_non_injective_agreement_B:
niagree(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_non_injective_agreement_A:
niagree(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_non_injective_agreement_P:
niagree(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_non_injective_agreement_P:
niagree(B_4[A,B,P,Rb,Kab,Text3] -> P_3[A,B,P,Rb,Kab,Text3], {A, B, P})
end