PKC_example.spthy

theory secrecy_asym_enc 
begin
builtins: asymmetric-encryption 
/* We formalize the following protocol:
*/
//1. A -> B: {B,na}sk(A)

// Public key infrastructure 
rule Register_pk: 
[ Fr(~ltkA) ] --> 
[ !Ltk($A, ~ltkA) , !Pk($A, pk(~ltkA)) , Out(pk(~ltkA)) ]

// Compromising an agent's long-term key 
rule Reveal_ltk: 
[ !Ltk(A, ltkA) ] --[ Reveal(A) ]-> [ Out(ltkA) ]
//
// Role A sends first message 
rule A_1_send: 
[ Fr(~na) , !Ltk(A, ltkA) , !Pk(B, pkB) ]
--[ Send(A, aenc(<A, ~na>, pkB)) , Secret(~na), Honest(A), Honest(B), Role('A') ]-> 
[ St_A_1(A, ltkA, pkB, B, ~na) , Out(aenc(<A, ~na>, pkB)) ]

// Role B receives first message 
rule B_1_receive: 
[ !Ltk(B, ltkB) , !Pk(A, pkA) , In(aenc(<A, na>,pkB)) ]
--[ Recv(B, aenc(<A, na>, pkB)) , Secret(na), Honest(B), Honest(A), Role('B') ]->
[ St_B_1(B, ltkB, pkA, A, na) ]

lemma executable: exists-trace 
"Ex A B m #i #j. Send(A,m)@i & Recv(B,m) @j"

lemma secrecy: 
	"All x #i. Secret(x) @i & Role('A') @i ==> not (Ex #j. K(x)@j)"

lemma secret_A: all-traces 
	"All n #i. Secret(n) @i & Role('A') @i ==> 
	(not (Ex #j. K(n)@j)) | (Ex B #j. Reveal(B)@j & Honest(B)@i)"
	
lemma secret_B: all-traces 
	"All n #i. Secret(n) @i & Role('B') @i ==> 
	(not (Ex #j. K(n)@j)) | (Ex B #j. Reveal(B)@j & Honest(B)@i)"
	
lemma secrecy_PFS_A: exists-trace 
	"not All x #i. Secret(x) @i & Role('A') @i ==> 
	not (Ex #j. K(x)@j) | (Ex B #r. Reveal(B)@r & Honest(B) @i & r < i)"
end