LoRa_PSK.spthy

theory LoRa_PSK begin
/*
 * Protocol:	  LoRa_PSK protocol  
 * Modeler: 	 Jun Young Kim 
 * Described in: 
 * Date: 	 
 *
 * Status: 	 Working
 */

builtins: symmetric-encryption, hashing
functions: hmac/2 [private]

/* protocol */
rule Key_distribution: 
	[ Fr(~key)]-->[ !PSK($A, ~key)]

rule reveal_PSK:
	[!PSK(A,key)]--[Reveal(A)]->
	[Out(key)]
	
rule A_1: 
	let msgA = <A,senc(~secA, keyA)> in
	[ !PSK(A, keyA), Fr(~secA)]
	--[Send_A(A,msgA)]-> 
	[Out(<msgA, hmac(msgA,keyA)>)]

rule B_1: 
	let msgA = <A,senc(secA, keyA)>
	    msgB = <B,'B_1',senc(~secB,keyB)> in
	 [!PSK(B,keyB), In(<msgA, hmac(msgA,keyA)>),Fr(~secB)] 
	 --[ Recv_B(B, msgA), Secret(secA), Send_B(B, msgB), 
	 Eq(hmac(msgA,keyA), hmac(msgA,keyB))]-> 
	 [Out(<msgB,hmac(msgB,keyB)>)]

rule A_2: 
	let msgB = <B,'B_1',senc(secB,keyB)> in
	[ In(<msgB,hmac(msgB,keyB)>), !PSK(A, keyA)]
	--[Recv_A(A,msgB), Secret(secB),
	Eq(hmac(msgB,keyB), hmac(msgB,keyA))]->[]
	 
lemma protocol_flow: exists-trace
	"Ex A B SA SB #i #j #k. Send_A(A,SA)@i
	& Recv_B(B,SA)@j & Send_B(B,SB)@j
	& Recv_A(A,SB)@k & i < j & j < k"

lemma message_secret_DY: all-traces
	"All s #i. Secret(s) @i & not (Ex A #i. Reveal(A)@i) 
	==> not (Ex #j. K(s)@j)"

lemma message_secret_eCK: all-traces
	"All s #i. Secret(s) @i 
	==> not (Ex #j. K(s)@j)"	
end