[taler-wallet-core] branch master updated: incomplete alloy model

[gnunet]

This is an automated email from the git hooks/post-receive script.

dold pushed a commit to branch master
in repository wallet-core.

The following commit(s) were added to refs/heads/master by this push:
     new f0e633ca incomplete alloy model
f0e633ca is described below

commit f0e633ca0929ba70fe9c4e6ba3b6ad71a394b4a2
Author: Florian Dold <florian.dold@gmail.com>
AuthorDate: Fri Sep 25 17:07:38 2020 +0530

    incomplete alloy model
---
 contrib/alloy/taler-sync.als | 52 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)

diff --git a/contrib/alloy/taler-sync.als b/contrib/alloy/taler-sync.als
new file mode 100644
index 00000000..f5b36192
--- /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
+

-- 
To stop receiving notification emails like this one, please contact
gnunet@gnunet.org.