diff --git a/prot-B.spthy b/prot-B.spthy
new file mode 100644
index 0000000000000000000000000000000000000000..10d5a7958489ba5b8e800076fbc8344742e6a9ac
--- /dev/null
+++ b/prot-B.spthy
@@ -0,0 +1,72 @@
+
+theory protB
+begin
+
+builtins: revealing-signing
+
+/*
+Model for the protocol in Figure 4 (b)
+
+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(<~n, revealSign(<I, R>, private_key)>) ]
+
+rule Initiator_2:
+    [ In(<n, sig>), Initiator_1(I, R, Rpk) ]
+  --[ Eq(revealVerify(sig, <I, R>, 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 there is indeed a trace which does not fulfill one-way non-injective agreement
+lemma not_ow_ni_agree:
+    exists-trace
+    "not (All I R n #i. Commit(I, R, n) @i 
+        ==>  ( Ex I2 #j. Running(R, I2, n) @j ) )"
+
+// This lemma shows that the protocol in Figure 4 (b) fulfills weak agreement
+lemma w_agree:
+    "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-B.spthy
+
+  runnable (exists-trace): verified (4 steps)
+  not_ow_ni_agree (exists-trace): verified (4 steps)
+  w_agree (all-traces): verified (5 steps)
+
+==============================================================================
+*/
+
+end
\ No newline at end of file