-
Notifications
You must be signed in to change notification settings - Fork 0
/
nssk.pctl
65 lines (43 loc) · 2.07 KB
/
nssk.pctl
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
const int T;
// Minimum probability that Alice authenticates
Pmin=? [ F (autA) ]
// Minimum probability that Eve authenticates
Pmin=? [ F (autE) ]
// Maximum probability that Eve authenticates by a replay attack
Pmax=? [ F<=T (autE&replay_attack) ]
// Minimum probability that Eve discovers a session key (past or current)
Pmin=? [ F (skE>0) ]
// Maximum probability that Eve discovers a session key (past or current)
Pmax=? [ F<=T (skE>0) ]
// Minimum expected number of Alice's authentications
R{"authentications"}min=? [ C<=T ]
// Maximum expected number of Alice's authentications
R{"authentications"}max=? [ C<=T ]
// Maximum number of exchanged messages until an Eve authentication succedes
R{"messages"}max=? [ F (autE) ]
// Minimum number of exchanged messages until an Eve authentication succedes
R{"messages"}min=? [ F (autE) ]
// Maximum number of units of computational resources needed to Eve to authenticate
R{"resources"}max=? [ F (autE) ]
// Minimum number of units of computational resources needed to Eve to authenticate
R{"resources"}min=? [ F (autE) ]
// Minimum number of rounds needed to Eve to discover the session key
R{"rounds"}min=? [ F (skE>0) ]
// Minimum cost of executing a replay attack
R{"messages"}min=? [ F (autE&replay_attack) ]+R{"resources"}min=? [ F (autE&replay_attack) ]+R{"rounds"}min=? [ F (autE&replay_attack) ]
// Maximum probability that Alice authenticates
Pmax=? [ F (autA) ]
// Key agreement property
P>=1 [ F (skA>0&skA=skB) ]
// Key freshness property
P>=1 [ G ((skC=0|skC=2) U skC=1) ]
// Secrecy property
P>=1 [ G (skE=0) ]
// Property for the synthesis of a strategy in which Eve authenticates via a replay attack using the current key
Pmax=? [ F (autE&replay_attack&!knows_kB&!knows_kA&skE=1) ]
// Property for the synthesis of a strategy in which Eve authenticates via a replay attack using a previous key
Pmax=? [ F (autE&replay_attack&!knows_kB&!knows_kA&skE=2) ]
// Property for the synthesis of a strategy in which Eve authenticates via the Man In The Middle attack
Pmax=? [ F (autE&mitm_attack) ]
// Authentication property
P>=1[F(autA)]