Upload New File

prot-A.spthy

+
+theory protA
+begin
+
+builtins: revealing-signing
+
+/*
+Model for the protocol in Figure 4 (a)
+
+Author: Johannes Wilson
+Date:        2023-05-02
+*/
+
+
+rule Register_pk:           // Registering a public key
+    [ Fr(~private_key) ]
+  --[ KeyReg( $A ) ]->
+    [ 
+      !Get_private_key($A, ~private_key), 
+      !Get_public_key($A, pk(~private_key)),
+      Out(pk(~private_key))
+    ]
+
+rule Initiator_1:
+    [ !Get_public_key(R, Rpk), !Get_private_key(I, Iltk) ]
+  --[  ]->
+    [ Out(<I,R>), Initiator_1(I, R, Rpk) ]
+
+rule Responder_1:
+    [ In(<I,R>), !Get_private_key(R, private_key), Fr(~n) ]
+  --[ Running(R, I, ~n) ]->
+    [ Out(<I, revealSign(<R,~n>, private_key)>), Out(~n) ]
+
+rule Initiator_2:
+    [ In(<I, sig>), Initiator_1(I, R, Rpk), In(n) ]
+  --[ Eq(revealVerify(sig, <R, n>, Rpk), true), Commit(I, R, n) ]->
+    []
+
+restriction equality:
+    "All x y #i. Eq(x,y) @i ==> x = y"
+
+lemma runnable:
+    exists-trace
+    "Ex I R n #i. Commit(I, R, n) @i"
+
+// This lemma shows that the protocol in Figure 4 (a) fulfills one-way non-injectve agreement
+lemma ow_ni_agree:
+    "All I R n #i. 
+        Commit(I, R, n) @i 
+        ==>  ( Ex I2 #j. Running(R, I2, n) @j )" 
+
+// This lemma shows that there is indeed a trace which does not fulfill weak agreement
+lemma not_w_agree:
+    exists-trace
+    "not (All I R n #i. Commit(I, R, n) @i 
+        ==> ( Ex n2 #j. Running(R, I, n2) @j ))"
+
+
+/*
+tamarin-prover 1.6.1
+==============================================================================
+summary of summaries:
+
+analyzed: prot-A.spthy
+
+  runnable (exists-trace): verified (5 steps)
+  ow_ni_agree (all-traces): verified (5 steps)
+  not_w_agree (exists-trace): verified (5 steps)
+
+==============================================================================
+*/
+
+end
\ No newline at end of file