[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[taler-wallet-core] branch master updated: incomplete alloy model
From: |
gnunet |
Subject: |
[taler-wallet-core] branch master updated: incomplete alloy model |
Date: |
Fri, 25 Sep 2020 13:40:18 +0200 |
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.
[Prev in Thread] |
Current Thread |
[Next in Thread] |
- [taler-wallet-core] branch master updated: incomplete alloy model,
gnunet <=