-
Notifications
You must be signed in to change notification settings - Fork 0
/
PUF_weak_mutual_noisy.spthy
182 lines (153 loc) · 5.09 KB
/
PUF_weak_mutual_noisy.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
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
/******************************************************************************
* Mutual authenticaton with noisy weak PUFs, based on equatonal theory
*
* check with
* tamarin-prover --prove PUF_weak_mutual_noisy.spthy
******************************************************************************/
theory PUF_weak_mutual_noisy
begin
// PUF modelling functions are private
functions: puf/1 [private], pufn/2 [private], gen/1, rep/2
builtins: hashing
// Equantional theory for puf reproduction
equations: rep( pufn(D,n) , gen( puf(D)) ) = puf(D)
/*
* Weak Puf with 1 value: no challenge, it only outputs a fingerprint
* NOTE 1: puf cannot depend on the server, but depends on the device, modelled as puf(D)
* NOTE 2: We let multiple servers to store the (single) CRP. The protocol will disambiguate
* the server including the id in the hash
*
* This version models "noise" with a gen() function producing the helper
* that is used to recover the correct puf(D) value
*/
rule PUFnoise:
[ PUFin(D), Fr(~n) ] --[ PUF(D) ]-> [ PUFout(D, pufn(D,~n)) ]
rule CRPnoise:
[ CRPin(A,D) ] --[ CRP(A,D) ]-> [ !CRPout(A,D,puf(D)) ]
rule BreakPUFnoise:
[ In(D), Fr(~n) ] --[ BreakPUF(D) ]-> [ Out(pufn(D,~n)) ]
rule RevealCRPnoise:
[ !CRPout(A,D,p) ] --[ RevealCRP(A,D) ]-> [ Out(p) ]
// new rule for noisy PUFs
rule BreakGen:
[ In(gen(puf(D))) ] --[ BreakGen(D) ]-> [ Out(puf(D)) ]
/*
* Basic hash-based device mutual authentication.
* For strong agreement it is necessary that A is included in the hash.
*
* A -> D: n,r ( r is the helper used to compute puf by D )
* D -> A: m,h(A,puf,n,m)
* A -> D: h(puf,m)
*
* Similar to ISO/IEC 9798-4-4 but here:
*
* 1. A is not just for breaking simmetry, multiple A's might have valid
* CRPs with D. Moreover, even if we limit CRPs to one server the device
* does not have a state to store this information securely. Thus it
* is necessary to explicitate A so that the device can agree on that ID.
* 2. We do not repeat A and n in the last message: this is an optimization.
* 3. A sends the helper value p in the first message which. D uses r to
* reproduce the error-corrected puf value
*/
rule BuildWeakCRPs:
[ ] --> [ CRPin($A,$D) ] // builds CRPs for Server-Device pairs
rule Alice0:
[ ] --> [ Alice0($A) ]
rule Alice1:
[ Alice0(A),!CRPout(A,D,p), Fr(~n) ]
-->
[ Out(<A,D,~n,gen(p)>), Alice2(A,D,~n,p) ] // gen(p) is sent together with n
rule Alice2:
[ Alice2(A,D,n,p), In(<D,A,m,h(A,p,n,m)>) ]
--[ Run(A,D,<'AtoD',n,m>), Commit(A,D,<'DtoA',n,m>) ]->
[ Out(<A,D,h(p,m)>) ]
rule Don0:
[ ] --> [ Don0($D) ]
rule Don1:
[ Don0(D),In(<A,D,n,r>), Fr(~m) ] // r is helper value
--[ Run(D,A,<'DtoA',n,~m>) ]->
[ PUFin(D), Don2(D,A,n,~m,r) ] // r is passed to next state
rule Don2:
[ Don2(D,A,n,m,r), PUFout(D,y) ] -->
[ Out(<D,A,m,h(A,rep(y,r),n,m)>), Don3(D,A,rep(y,r),n,m) ] // r is used to remove noise
rule Don3:
[ Don3(D,A,y,n,m), In(<A,D,h(y,m)>) ]
--[ Commit(D,A,<'AtoD',n,m>) ]->
[ ]
// ======================================
/*
* Initialization is before deployment
*/
restriction resCRPbeforePUF:
"All A D #i #j. CRP(A,D)@i & PUF(D)@j ==> i < j"
/*
* sanity check: the protocol can commit in both directions
*/
lemma Sanity:
exists-trace
"Ex A D m n #i. Commit(A,D,<'DtoA',n,m>)@i
&
Ex A D m n #i. Commit(A,D,<'AtoD',n,m>)@i
&
not (Ex A D #k. RevealCRP(A,D)@k)
&
not (Ex D #k. BreakPUF(D)@k)
&
not (Ex D #k. BreakGen(D)@k)
"
/*
* Property: Secrecy of PUF with respect to A
* with A = {BreakPUF(D), RevealCRP(a,D), BreakGen(D)}
*
* Intuition:
* puf values are only leaked if CRPs are explicity revealed or
* if puf has been broken (direcly or through helper data)
*/
lemma Secrecy_A:
"All D p #t. K(p)@t & p = puf(D) ==>
(Ex a #j.RevealCRP(a,D)@j & j<t ) // CRP for D is revealed by one server
|
(Ex #j.BreakPUF(D)@j & j<t) // PUF for D is broken
|
(Ex #j.BreakGen(D)@j & j<t)
"
/*
* Property: Mutual authentication with respect to A
* with A = {BreakPUF(D), RevealCRP(a,D), BreakGen(D)}
*
* Intuition:
* 1) each Commit(B,C,x) is preceded by a corresponding Run(C,B,x);
* 2) no other Commit on the same x exists.
* unless CRPs or puf/helper data has been broken.
*
* Note: D in A is istantiated to C or B depending on the protocol direction
*/
lemma MutualAuthentication_A:
"All B C x #t. Commit(B,C,x)@t ==>
(
(Ex #j. Run(C,B,x)@j
& j<t
& not (Ex E G #k. Commit(E,G,x) @k & not (#k = #t)))
| (
(Ex n m. x = <'DtoA',n,m>) & // C is the Device
(
(Ex a #r. RevealCRP(a,C)@r & r<t) // It is enough that one party E that registered C reveals the CRP
|
(Ex #r. BreakPUF(C)@r & r<t)
|
(Ex #r. BreakGen(C)@r & r<t)
)
)
| (
(Ex n m. x = <'AtoD',n,m>) & // B is the device
(
(Ex a #r. RevealCRP(a,B)@r & r<t) // It is enough that one party E that registered B reveals the CRP
|
(Ex #r. BreakPUF(B)@r & r<t)
|
(Ex #r. BreakGen(B)@r & r<t)
)
)
)
"
end