-
Notifications
You must be signed in to change notification settings - Fork 0
/
NSL.spthy
138 lines (91 loc) · 6.55 KB
/
NSL.spthy
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
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
theory NeedhamSchroeder
begin
functions: rep/2 [private], check_rep/2, get_rep/1
equations: check_rep(rep(m,loc),loc)=m, get_rep(rep(m,loc))=m
builtins: asymmetric-encryption
heuristic: p /* heuristic for SAPIC */
rule Init_: // [process=top-level] Init
[] --[Init()]-> [State_()]
rule Par_: // [process=top-level] Par
[State_()] --[]-> [State_1(), State_2()]
rule Rep_0_1: // [process=top-level] Rep, 0
[State_1()] --[]-> [!Semistate_11()]
rule Rep_1_1: // [process=top-level] Rep, 1
[!Semistate_11()] --[]-> [State_11()]
rule new_skA_11: // [process=top-level] new skA
[State_11(), Fr(skA)] --[]-> [State_111(skA)]
rule event_HonestApkskA_111: // [process=top-level] event HonestA(pk(skA))
[State_111(skA)] --[Event(), HonestA(pk(skA))]-> [State_1111(skA)]
rule out_pkskA_1111: // [process=top-level] out pk(skA)
[State_1111(skA)] --[]-> [State_11111(skA), Out(pk(skA))]
rule Rep_0_11111: // [process=top-level] Rep, 0
[State_11111(skA)] --[]-> [!Semistate_111111(skA)]
rule Rep_1_11111: // [process=top-level] Rep, 1
[!Semistate_111111(skA)] --[]-> [State_111111(skA)]
rule in_pkxB_111111: // [process=top-level] in pk(xB)
[State_111111(skA), In(pk(xB))] --[]-> [State_1111111(skA, xB)]
rule new_Na_1111111: // [process=top-level] new Na
[State_1111111(skA, xB), Fr(Na)] --[]-> [State_11111111(Na, skA, xB)]
rule event_OUT_I_1aenc_Na_pkskA_pkxB_11111111: // [process=top-level] event OUT_I_1(aenc(<Na, pk(skA)>, pk(xB)))
[State_11111111(Na, skA, xB)] --[Event(), OUT_I_1(aenc(<Na, pk(skA)>, pk(xB)))]-> [State_111111111(Na, skA, xB)]
rule out_aenc_Na_pkskA_pkxB_111111111: // [process=top-level] out aenc(<Na, pk(skA)>, pk(xB))
[State_111111111(Na, skA, xB)] --[]-> [State_1111111111(Na, skA, xB), Out(aenc(<Na, pk(skA)>, pk(xB)))]
rule in_aenc_Na_xNb_pkxB_pkskA_1111111111: // [process=top-level] in aenc(<Na, xNb, pk(xB)>, pk(skA))
[State_1111111111(Na, skA, xB), In(aenc(<Na, xNb, pk(xB)>, pk(skA)))] --[]-> [State_11111111111(Na, skA, xB, xNb)]
rule event_IN_I_2_nrxNb_aenc_Na_xNb_pkxB_pkskA_11111111111: // [process=top-level] event IN_I_2_nr(xNb, aenc(<Na, xNb, pk(xB)>, pk(skA)))
[State_11111111111(Na, skA, xB, xNb)] --[Event(), IN_I_2_nr(xNb, aenc(<Na, xNb, pk(xB)>, pk(skA)))]-> [State_111111111111(Na, skA, xB, xNb)]
rule new_k_111111111111: // [process=top-level] new k
[State_111111111111(Na, skA, xB, xNb), Fr(k)] --[]-> [State_1111111111111(Na, k, skA, xB, xNb)]
rule out_aenc_xNb_k_pkxB_1111111111111: // [process=top-level] out aenc(<xNb, k>, pk(xB))
[State_1111111111111(Na, k, skA, xB, xNb)] --[]-> [State_11111111111111(Na, k, skA, xB, xNb), Out(aenc(<xNb, k>, pk(xB)))]
rule event_SessionApkskA_pkxB_k_11111111111111: // [process=top-level] event SessionA(pk(skA), pk(xB), k)
[State_11111111111111(Na, k, skA, xB, xNb)] --[Event(), SessionA(pk(skA), pk(xB), k)]-> [State_111111111111111(Na, k, skA, xB, xNb)]
rule Zero_111111111111111: // [process=top-level] Zero
[State_111111111111111(Na, k, skA, xB, xNb)] --[]-> []
rule Rep_0_2: // [process=top-level] Rep, 0
[State_2()] --[]-> [!Semistate_21()]
rule Rep_1_2: // [process=top-level] Rep, 1
[!Semistate_21()] --[]-> [State_21()]
rule new_skB_21: // [process=top-level] new skB
[State_21(), Fr(skB)] --[]-> [State_211(skB)]
rule new_skC_211: // [process=top-level] new skC
[State_211(skB), Fr(skC)] --[]-> [State_2111(skB, skC)]
rule event_HonestBpkdiffskB_skC_2111: // [process=top-level] event HonestB(pk(diff(skB, skC)))
[State_2111(skB, skC)] --[Event(), HonestB(pk(diff(skB, skC)))]-> [State_21111(skB, skC)]
rule out_pkskB_21111: // [process=top-level] out pk(skB)
[State_21111(skB, skC)] --[]-> [State_211111(skB, skC), Out(pk(skB))]
rule out_pkskC_211111: // [process=top-level] out pk(skC)
[State_211111(skB, skC)] --[]-> [State_2111111(skB, skC), Out(pk(skC))]
rule Rep_0_2111111: // [process=top-level] Rep, 0
[State_2111111(skB, skC)] --[]-> [!Semistate_21111111(skB, skC)]
rule Rep_1_2111111: // [process=top-level] Rep, 1
[!Semistate_21111111(skB, skC)] --[]-> [State_21111111(skB, skC)]
rule in_aenc_xNa_pkxA_pkaa_21111111: // [process=top-level] in aenc(<xNa, pk(xA)>, pk(aa))
[State_21111111(skB, skC), In(aenc(<xNa, pk(xA)>, pk(aa)))] --[]-> [State_211111111(aa, skB, skC, xA, xNa)]
rule event_IN_R_1_nixNa_aenc_xNa_pkxA_pkaa_211111111: // [process=top-level] event IN_R_1_ni(xNa, aenc(<xNa, pk(xA)>, pk(aa)))
[State_211111111(aa, skB, skC, xA, xNa)] --[Event(), IN_R_1_ni(xNa, aenc(<xNa, pk(xA)>, pk(aa)))]-> [State_2111111111(aa, skB, skC, xA, xNa)]
rule new_Nb_2111111111: // [process=top-level] new Nb
[State_2111111111(aa, skB, skC, xA, xNa), Fr(Nb)] --[]-> [State_21111111111(Nb, aa, skB, skC, xA, xNa)]
rule new_r_21111111111: // [process=top-level] new r
[State_21111111111(Nb, aa, skB, skC, xA, xNa), Fr(r)] --[]-> [State_211111111111(Nb, aa, r, skB, skC, xA, xNa)]
rule event_OUT_R_1aenc_xNa_Nb_pkaa_pkxA_211111111111: // [process=top-level] event OUT_R_1(aenc(<xNa, Nb, pk(aa)>, pk(xA)))
[State_211111111111(Nb, aa, r, skB, skC, xA, xNa)] --[Event(), OUT_R_1(aenc(<xNa, Nb, pk(aa)>, pk(xA)))]-> [State_2111111111111(Nb, aa, r, skB, skC, xA, xNa)]
rule out_aenc_xNa_Nb_pkaa_pkxA_2111111111111: // [process=top-level] out aenc(<xNa, Nb, pk(aa)>, pk(xA))
[State_2111111111111(Nb, aa, r, skB, skC, xA, xNa)] --[]-> [State_21111111111111(Nb, aa, r, skB, skC, xA, xNa), Out(aenc(<xNa, Nb, pk(aa)>, pk(xA)))]
rule in_aenc_Nb_xk_pkaa_21111111111111: // [process=top-level] in aenc(<Nb, xk>, pk(aa))
[State_21111111111111(Nb, aa, r, skB, skC, xA, xNa), In(aenc(<Nb, xk>, pk(aa)))] --[]-> [State_211111111111111(Nb, aa, r, skB, skC, xA, xNa, xk)]
rule event_SessionBpkxA_pkaa_xk_211111111111111: // [process=top-level] event SessionB(pk(xA), pk(aa), xk)
[State_211111111111111(Nb, aa, r, skB, skC, xA, xNa, xk)] --[Event(), SessionB(pk(xA), pk(aa), xk)]-> [State_2111111111111111(Nb, aa, r, skB, skC, xA, xNa, xk)]
rule Zero_2111111111111111: // [process=top-level] Zero
[State_2111111111111111(Nb, aa, r, skB, skC, xA, xNa, xk)] --[]-> []
restriction single_session: // for a single session
"All #i #j. Init()@i & Init()@j ==> #i=#j"
lemma sanity1 : exists-trace
" Ex pka pkb k #t1. SessionA(pka, pkb, k) @ t1"
lemma sanity2 : exists-trace
" Ex pka pkb k #t1. SessionB(pka, pkb, k) @ t1"
lemma source [sources, reuse]:
" ( All ni m1 #i. IN_R_1_ni(ni, m1) @ i ==> ( ( Ex #j. KU(ni) @ j & j < i ) | ( Ex #j. OUT_I_1(m1) @ j ) ) ) & ( All nr m2 #i. IN_I_2_nr(nr, m2) @ i ==> ( ( Ex #j. KU(nr) @ j & j < i ) | ( Ex #j. OUT_R_1(m2) @ j ) ) )"
lemma secrecy :
" not( Ex pka pkb k #t1 #t2. SessionA(pka, pkb, k) @ t1 & K(k) @ t2 & ( Ex #i. HonestA(pka) @ i ) & ( Ex #i. HonestB(pkb) @ i ) )"
end