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
+