scyther-proof-0.3.0: data/examples/iso9798/isoiec-9798-3.spthy
/*
* 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