66 lines
1.2 KiB
Plaintext
66 lines
1.2 KiB
Plaintext
|
/*
|
||
|
|
* This is a model of a version of the TLS protocol as modeled in
|
||
|
|
* Boyd, Mathuria "Protocols for Authentication and key establishment"
|
||
|
|
*
|
||
|
|
* It's a very simplified form.
|
||
|
|
*/
|
||
|
|
define(`msg1',`na')
|
||
|
|
define(`msg2',`nb')
|
||
|
|
define(`kab',`hash(pmk,na,nb)')
|
||
|
|
define(`msg3a',`{ pmk }pk(B)')
|
||
|
|
define(`M1',`hash(msg1,msg2,msg3a)')
|
||
|
|
define(`msg3b',`{ M1 }sk(A)')
|
||
|
|
define(`M2',`hash(msg1,msg2,msg3a,msg3b)')
|
||
|
|
define(`msg3c',`{ M2 }kab')
|
||
|
|
define(`msg3',`msg3a,msg3b,msg3c')
|
||
|
|
define(`M3',`msg1,msg2,msg3')
|
||
|
|
define(`msg4',`{ M3 }kab')
|
||
|
|
|
||
|
|
/* below is just Scyther input and no further macro definitions */
|
||
|
|
|
||
|
|
const pk,hash: Function;
|
||
|
|
secret sk,unhash: Function;
|
||
|
|
inversekeys(pk,sk);
|
||
|
|
inversekeys(hash,unhash);
|
||
|
|
|
||
|
|
const Alice, Bob, Eve: Agent;
|
||
|
|
const Terence: Agent;
|
||
|
|
|
||
|
|
protocol tls-bm-1(A,B)
|
||
|
|
{
|
||
|
|
role A
|
||
|
|
{
|
||
|
|
const na: Nonce;
|
||
|
|
const pmk: Nonce;
|
||
|
|
var nb: Nonce;
|
||
|
|
|
||
|
|
send_1( A,B, msg1 );
|
||
|
|
read_2( B,A, msg2 );
|
||
|
|
send_3( A,B, msg3 );
|
||
|
|
read_4( B,A, msg4 );
|
||
|
|
|
||
|
|
claim_A1( A, Secret, kab );
|
||
|
|
claim_A2( A, Nisynch );
|
||
|
|
}
|
||
|
|
|
||
|
|
role B
|
||
|
|
{
|
||
|
|
var na: Nonce;
|
||
|
|
var pmk: Nonce;
|
||
|
|
const nb: Nonce;
|
||
|
|
|
||
|
|
read_1( A,B, msg1 );
|
||
|
|
send_2( B,A, msg2 );
|
||
|
|
read_3( A,B, msg3 );
|
||
|
|
send_4( B,A, msg4 );
|
||
|
|
|
||
|
|
claim_B1( B, Secret, kab );
|
||
|
|
claim_B2( B, Nisynch );
|
||
|
|
}
|
||
|
|
}
|
||
|
|
|
||
|
|
|
||
|
|
untrusted Eve;
|
||
|
|
compromised sk(Eve);
|
||
|
|
|