-
Notifications
You must be signed in to change notification settings - Fork 0
/
secureStorage.pv
112 lines (90 loc) · 3.39 KB
/
secureStorage.pv
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
free c:channel.
(*Public key encryption*)
type pkey.
type skey.
fun pk(skey): pkey.
fun aencrypt(bitstring, pkey):bitstring.
reduc forall x: bitstring, y:skey; adecrypt(aencrypt(x, pk(y)), y) = x.
(*Signatures*)
type signpkey.
type signskey.
fun spk(signskey):signpkey.
fun sign(bitstring, signskey): bitstring.
reduc forall x: bitstring, y: signskey; getmess(sign(x, y)) = x.
reduc forall x: bitstring, y: signskey; checksign(sign(x, y), spk(y)) = x.
(*Shared key encryption*)
type nonce.
fun sencrypt(bitstring, nonce):bitstring.
reduc forall x:bitstring, y:nonce; sdecrypt(sencrypt(x, y), y) = x.
(*Type converter*)
fun nonce_to_bitstring(nonce):bitstring[data, typeConverter].
(* Key generator *)
fun gen_ekey(bitstring, nonce): nonce.
fun gen_ikey(bitstring, nonce): nonce.
(* Domain nonce generator *)
fun gen_domain_nonce(bitstring): nonce.
(* Storage table*)
table storage(bitstring, bitstring).
(* Authentication queries *)
event beginTTPparam(pkey).
event endTTPparam(pkey).
event beginSCparam(pkey).
event endSCparam(pkey).
query x:pkey; inj-event(endTTPparam(x)) ==> inj-event(beginTTPparam(x)).
query x:pkey; inj-event(endSCparam(x)) ==> inj-event(beginSCparam(x)).
(* Secrecy queries *)
free sessionKey: nonce [private].
free payload, srr, blockId, domain, blockEncKey, blockIntegKey:bitstring [private].
query attacker(sessionKey);
attacker(srr);
attacker(domain).
let processSC(sessionKey:nonce, srr:bitstring,
domain:bitstring,
payload:bitstring,
blockId:bitstring,
pkTTP: pkey, skSC:skey) =
in (c, (pkX:pkey));
event beginTTPparam(pkX);
new Nsc: bitstring;
out (c, (aencrypt((Nsc, sessionKey), pkX),
sencrypt((Nsc, srr, domain), sessionKey)));
in (c, (m:bitstring, wt:bitstring));
let (=Nsc,=domain, blockEncKeyX:nonce,
blockIntegKeyX:nonce) = sdecrypt(m, sessionKey) in
out (c, (blockId, sencrypt(payload, blockEncKeyX), wt));
0.
let processTTP(pkSC:pkey, skTTP:skey, mk:nonce) =
in (c, (m:bitstring, n:bitstring));
let(NonceY:bitstring, sessionKeyY:nonce) = adecrypt(m, skTTP) in
let(RepeatedNonceY:bitstring,
srrY:bitstring, domainY:bitstring) = sdecrypt(n, sessionKeyY) in
new Nb:nonce;
out(c, (sencrypt((NonceY, domainY,
gen_ekey(nonce_to_bitstring(gen_domain_nonce(domain)), mk),
gen_ikey(nonce_to_bitstring(gen_domain_nonce(domain)), mk)),
sessionKeyY),
sencrypt((Nb, domain, srr), mk)));
0.
let processSR() =
in (c, (bid:bitstring, payloadY:bitstring, wtY:bitstring));
insert storage(bid, (payloadY, wtY));
0.
query attacker(blockEncKey);
attacker(blockIntegKey);
attacker(blockId);
attacker(blockIntegKey);
attacker(payload).
(*Main*)
process
new symmetricKey:nonce;
new storageReference:bitstring;
new domainReference:bitstring;
new masterKey:nonce;
new payload:bitstring;
new blockId:bitstring;
new skSC:skey; let pkSC = pk(skSC) in out (c, pkSC);
new skTTP:skey; let pkTTP = pk(skTTP) in out (c, pkTTP);
( (!processSC(symmetricKey, storageReference,
domainReference, payload, blockId, pkTTP, skSC)) |
(!processTTP(pkSC, skTTP, masterKey)) |
(!processSR()))