aboutsummaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
authorFlorian Dold <florian.dold@gmail.com>2020-09-25 17:07:38 +0530
committerFlorian Dold <florian.dold@gmail.com>2020-09-25 17:09:44 +0530
commitf0e633ca0929ba70fe9c4e6ba3b6ad71a394b4a2 (patch)
tree2ca2e36f8758bc6f94a1bc68f9cc5e303c8d3da2 /contrib
parentaf962c90bafb1a66eef712f7fa4a284459b21ea0 (diff)
incomplete alloy model
Diffstat (limited to 'contrib')
-rw-r--r--contrib/alloy/taler-sync.als52
1 files changed, 52 insertions, 0 deletions
diff --git a/contrib/alloy/taler-sync.als b/contrib/alloy/taler-sync.als
new file mode 100644
index 000000000..f5b361926
--- /dev/null
+++ b/contrib/alloy/taler-sync.als
@@ -0,0 +1,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
+