aboutsummaryrefslogtreecommitdiff
path: root/contrib/alloy/taler-sync.als
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