diff --git a/prot-C.spthy b/prot-C.spthy new file mode 100644 index 0000000000000000000000000000000000000000..f2fb4da364bcd54f72e44ebebd01fcbe6b61b10f --- /dev/null +++ b/prot-C.spthy @@ -0,0 +1,75 @@ + +theory protC +begin + +builtins: revealing-signing + +/* +Model for the protocol in Figure 4 (c) + +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), Fr(~n) ] + --[ ]-> + [ Out(<I,R,~n>), Initiator_1(I, R, ~n, Rpk) ] + +rule Responder_1: + [ In(<I,R,n>), !Get_private_key(R, private_key) ] + --[ Running(R, I, n) ]-> + [ Out(<I, revealSign(<R, n>, private_key)>) ] + +rule Initiator_2: + [ In(<I, sig>), Initiator_1(I, R, n, Rpk) ] + --[ 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 (c) fulfills one-way injective agreement +lemma ow_i_agree: + "All I R n #i. Commit(I, R, n) @i + ==> ( Ex I2 #j. Running(R, I2, n) @j + & j < i + & not(Ex I3 R2 #i2. Commit(I3, R2, n) @i2 & not(#i2 = #i)))" + +// This lemma shows that there is indeed a trace which does not fulfill non-injective agreement +lemma not_ni_agree: + exists-trace + "not (All I R n #i. Commit(I, R, n) @i + ==> ( Ex #j. Running(R, I, n) @j ) )" + + +/* +tamarin-prover 1.6.1 +============================================================================== +summary of summaries: + +analyzed: prot-C.spthy + + runnable (exists-trace): verified (5 steps) + ow_i_agree (all-traces): verified (9 steps) + not_ni_agree (exists-trace): verified (5 steps) + +============================================================================== + +*/ + +end \ No newline at end of file