/
2DH-NX.spdl
75 lines (62 loc) · 1.81 KB
/
2DH-NX.spdl
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
/*
* 2DH-NX
*
* Two-move Diffie-Hellman simplified, Naxossed
*
* Cas Cremers, 30 April 2009
*
* Design decision:
*
* 1. Tried to be minimal.
*
* 2. Content outside of signature is technically speaking redundant,
* just there for clarity.
*
* 3. Including alpha (the third element of the tuple) in the second
* message serves two purposes. First, it distinguishes message 1 and 2.
* Second, alpha is used as 'session identifier'. If it is replaced by a
* constant, a state-reveal query on a non-matching thread may reveal
* the responders nonce. If desired, an explicit session identifier may
* be added to the first and second message; if so, the alpha can be
* omitted from the second message, if care is taken to distinguish both
* messages (either by labeling or reordering the tuple).
*/
// Hash functions
hashfunction h1,h2,g1,g2;
/*
* Hack to simulate g^ab = g^ba.
* '@' prefix of protocol name denotes helper protocol, which is used by
* Scyther for displaying, and such protocols are ignored in
* auto-generation of protocol modifiers.
*/
protocol @exponentiation(RA)
{
role RA
{
var alpha,beta, T1,T2: Ticket;
recv_!1(RA,RA, g2(g1(T1),T2) );
send_!2(RA,RA, g2(g1(T2),T1) );
}
}
// The protocol description
protocol 2DH-NX(I,R)
{
role I
{
fresh x: Nonce;
var beta: Ticket;
send_Compromise(I,I, h1(sk(I),x) );
send_1(I,R, g1(h1(sk(I),x)),R, { g1(h1(sk(I),x)),R }sk(I) );
recv_2(R,I, beta,I,g1(h1(sk(I),x)), { beta,I, g1(h1(sk(I),x)) }sk(R) );
claim(I,SKR, g2(beta,h1(sk(I),x)) );
}
role R
{
fresh y: Nonce;
var alpha: Ticket;
send_Compromise(R,R, h1(sk(R),y) );
recv_1(I,R, alpha,R, { alpha,R }sk(I) );
send_2(R,I, g1(h1(sk(R),y)),I,alpha, { g1(h1(sk(R),y)),I,alpha }sk(R) );
claim(R,SKR, g2(alpha,h1(sk(R),y)) );
}
}