blob: 3f302b4ad9156527c72ee8c7de5f9bfb08150272 (
plain)
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
|
/*
Simple Alloy4 model for Taler backup&sync.
*/
sig AnastasisMasterSecret { }
// Key pair that each wallet has.
sig WalletDeviceKey { }
sig SyncProvider { }
// Key pair to access the sync account.
sig SyncAccountKey { }
// Abstraction of what's in a sync blob
sig SyncBlobHeader {
// Access matrix, abstracts the DH
// suggested by Christian (https://bugs.gnunet.org/view.php?id=6077#c16959)
// The DH will yield the symmetric blob encryption key for the "inner blob"
access: AnastasisMasterSecret -> WalletDeviceKey,
}
sig SyncAccount {
account_key: SyncAccountKey,
prov: SyncProvider,
hd: SyncBlobHeader,
}
sig WalletState {
device_key: WalletDeviceKey,
anastasis_key: AnastasisMasterSecret,
enrolled: set SyncAccount,
}
fact DifferentDeviceKeys {
all disj w1, w2: WalletState | w1.device_key != w2.device_key
}
fact AnastasisKeyConsistent {
all disj w1, w2: WalletState, s: SyncAccount |
s in (w1.enrolled & w2.enrolled) implies
w1.anastasis_key = w2.anastasis_key
}
fact NoBoringInstances {
#WalletState >= 2
all w: WalletState | #w.enrolled >= 1
}
run {} for 5
|
