53 lines
1.1 KiB
Alloy
53 lines
1.1 KiB
Alloy
|
/*
|
||
|
|
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
|
||
|
|
|