PKS for Medical Data Protection

(*** Efficient Design of a Novel ECC-Based Public Key Scheme for Medical Data Protection by Utilization of NanoPi Fire ***)

(* Chael definition *)
(* Note that defining several chaels makes the implementation more readable *)
free RSAP_CH_secure_net : chael [private]. (* private chael between the RSAP and CH *)
free RSAP_CM_secure_net : chael [private]. (* private chael between the RSAP and CM *)
free U_CM_secure_net : chael [private]. (* private chael between the User and CM *)
free pub_net : chael. (* A general public chael *)

(* Private Terms *)
free x : bitstring [private].
free PWu : bitstring [private].
free IDu : bitstring [private].
free IDcm : bitstring [private].
free SK_CM_CH : bitstring [private].

(* Public Terms *)
free IDch : bitstring.
const B : bitstring.

(* Functions or constructors *)
fun Scalar_Mul(bitstring, bitstring) : bitstring.
fun XORFun(bitstring, bitstring) : bitstring.
fun HashFunOne(bitstring) : bitstring.
fun HashFunTwo(bitstring, bitstring) : bitstring.
fun HashFunThree(bitstring, bitstring, bitstring) : bitstring.
fun HashFunFour(bitstring, bitstring, bitstring, bitstring) : bitstring.
fun HashFunFive(bitstring, bitstring, bitstring, bitstring, bitstring) : bitstring.
fun ADD(bitstring, bitstring) : bitstring.
fun Multiply(bitstring, bitstring) : bitstring.
fun Symmetric_Enc(bitstring, bitstring) : bitstring.
fun CONCAT(bitstring, bitstring, bitstring) : bitstring.
fun SEncrypt(bitstring, bitstring): bitstring.

(* Destructors *)
reduc forall m1 : bitstring, key : bitstring; Symmetric_Dec(Symmetric_Enc(m1, key), key) = m1.
reduc forall m1 : bitstring, m2 : bitstring; DXORFun(XORFun(m1, m2), m2) = m1.
reduc forall m1 : bitstring, m2 : bitstring, m3 : bitstring; SeparateFirst(CONCAT(m1, m2, m3)) = m1.
reduc forall m1 : bitstring, m2 : bitstring, m3 : bitstring; SeparateSecond(CONCAT(m1, m2, m3)) = m2.
reduc forall m1 : bitstring, m2 : bitstring, m3 : bitstring; SeparateThird(CONCAT(m1, m2, m3)) = m3.
reduc forall m1 : bitstring, m2 : bitstring; SDecrypt(SEncrypt(m1, m2), m2) = m1.

(* Equations *)
equation forall m1 : bitstring, m2 : bitstring; Scalar_Mul(m1, Scalar_Mul(m2, B)) = Scalar_Mul(m2, Scalar_Mul(m1, B)).

(* queries *)
query attacker (SK_CM_CH). (* this query indicates secrecy of the shared key between reader and ISM *)
query attacker (IDu). (* this query indicates the anonymity of user *)
weaksecret PWu. (* this query indicates the resistance of protocol against the offline password guessing attack *)
query inj-event ( endCM ) ==> inj-event (startCM).
query inj-event ( endCH) ==> inj-event (startCH).

(* Events *)
event startCH.
event endCH.
event startCM.
event endCM.

(*****************************************************************************)
(******************** Root SAP process ************************)
(*****************************************************************************)

let pRSAP=
(* Node registration phase *)
let PKsys = Scalar_Mul(x, B) in
in (RSAP_CH_secure_net, Rch : bitstring);
new rrsap_ch : bitstring;
let Rrsap_ch = Scalar_Mul(rrsap_ch, B) in
let sch = ADD(rrsap_ch, Multiply(HashFunThree(IDch, Rrsap_ch, Rch), x)) in
out (RSAP_CH_secure_net, (sch));
in (RSAP_CM_secure_net, HPWu : bitstring);
out (RSAP_CH_secure_net, (HPWu));
in (RSAP_CH_secure_net, (Xu_2 : bitstring, EIDu_cm : bitstring));
let scm = Multiply(HashFunThree(IDu, IDcm, sch), x) in
out (RSAP_CM_secure_net, (Xu_2, EIDu_cm, scm, PKsys));
0.

(*****************************************************************************)
(******************************** User process *****************************)
(*****************************************************************************)

let pU=

(* Secure session phase *)
out (U_CM_secure_net, (IDu, PWu));
0.

(*****************************************************************************)
(***************************** CM process ********************************)
(*****************************************************************************)

let pCM=
(* Node registration phase *)
new rcm_u : bitstring;
let HPWu = HashFunThree(IDu, PWu, rcm_u) in
out (RSAP_CM_secure_net, (HPWu));
in (RSAP_CM_secure_net, (Xu_2 : bitstring, EIDu_cm : bitstring, scm : bitstring, PKsys : bitstring));
new rcm : bitstring;
let SKcm = Multiply(rcm, scm) in
let PKcm = Scalar_Mul(rcm, PKsys) in

(* Secure session phase *)
new CTcm : bitstring;
in (U_CM_secure_net, (xIDu : bitstring, xPWu : bitstring));
let xHPWu = HashFunThree(xIDu, xPWu, rcm_u) in
let Xu_1 = DXORFun(Xu_2, xHPWu) in
new SNcm : bitstring;
let STcm = Scalar_Mul(SNcm, PKcm) in
let Vcm = HashFunFive(IDu, IDcm, Xu_1, STcm, CTcm) in
event startCH;
out (pub_net, (EIDu_cm, STcm, Vcm, CTcm));
in (pub_net, (xXEIDu_cm_new : bitstring, xSTch : bitstring, xVch : bitstring, xCTch : bitstring));
let SSKcm = HashFunTwo(IDch, Scalar_Mul(Multiply(SNcm, SKcm), xSTch)) in
let xEIDu_cm_new = DXORFun(xXEIDu_cm_new, HashFunOne(SSKcm)) in
let xxVch = HashFunThree(xEIDu_cm_new, SSKcm, xCTch) in
if (xVch = xxVch) then
out (pub_net, SEncrypt(SK_CM_CH, SSKcm));
event endCM;
0.

(*****************************************************************************)
(***************************** CH process ***********************************)
(*****************************************************************************)

let pCH=

(* Node registration phase *)
new rch : bitstring;
let Rch = Scalar_Mul(HashFunOne(XORFun(rch, IDch)), B) in
out (RSAP_CH_secure_net, (Rch));
in (RSAP_CH_secure_net, sch : bitstring);
let PKch = Scalar_Mul(rch, B) in
in (RSAP_CH_secure_net, HPWu : bitstring);
let Xu_1 = HashFunFour(IDu, IDcm, rch, sch) in
let Xu_2 = XORFun(Xu_1, HPWu) in
new rch_u : bitstring;
let EIDu_cm = Symmetric_Enc(CONCAT(IDu, IDcm, rch_u), rch) in
out (RSAP_CH_secure_net, (Xu_2, EIDu_cm));

(* Secure session phase *)
new CTch : bitstring;
in (pub_net, (xEIDu_cm : bitstring, xSTcm : bitstring, xVcm : bitstring, xCTcm : bitstring));
let temp1 = Symmetric_Dec(xEIDu_cm, rch) in
let xIDu = SeparateFirst(temp1) in
let xIDcm = SeparateSecond(temp1) in
let xrch_u = SeparateThird(temp1) in
let xXu_1 = HashFunFour(xIDu, xIDcm, rch, sch) in
let xxVcm = HashFunFive(xIDu, xIDcm, xXu_1, xSTcm, xCTcm) in
if (xVcm = xxVcm) then
new SNch : bitstring;
let STch = Scalar_Mul(SNch, PKch) in
let SSKch = HashFunTwo(IDch, Scalar_Mul(Multiply(SNch, Multiply(rch, HashFunThree(xIDu, xIDcm, sch))), xSTcm)) in
out (pub_net, SEncrypt(SK_CM_CH, SSKch));
new rch_u_new : bitstring;
let EIDu_cm_new = Symmetric_Enc(CONCAT(xIDu, xIDcm, rch_u_new), rch) in
let XEIDu_cm_new = XORFun(EIDu_cm_new, HashFunOne(SSKch)) in
let Vch = HashFunThree(EIDu_cm_new, SSKch, CTch) in
event startCM;
out (pub_net, (XEIDu_cm_new, STch, Vch, CTch));
event endCH;
0.

process
( (!pRSAP) | (!pCM) | (!pCH) | (!pU) )


Output:
Completing equations...
Completing equations...
-- Query inj-event(endCH) ==> inj-event(startCH)
nounif mess(RSAP_CH_secure_net[],Rch_347)/-5000
Completing...
200 rules inserted. The rule base contains 187 rules. 19 rules in the queue.
Starting query inj-event(endCH) ==> inj-event(startCH)
goal reachable: begin(startCH, xPWu = PWu[], xIDu = IDu[], PKsys_104 = Scalar_Mul(x[],B), scm_103 = Multiply(HashFunThree(IDu[],IDcm[],ADD(rrsap_ch[Rch = Rch_8190,!1 = @sid_8191],Multiply(HashFunThree(IDch[],Scalar_Mul(rrsap_ch[Rch = Rch_8190,!1 = @sid_8191],B),Rch_8190),x[]))),x[]), EIDu_cm_102 = Symmetric_Enc(CONCAT(IDu[],IDcm[],rch_u[HPWu_108 = HashFunThree(IDu[],PWu[],rcm_u[!1 = @sid_8192]),sch_107 = sch_8193,!1 = endsid_8194]),rch[!1 = endsid_8194]), Xu_2_101 = XORFun(HashFunFour(IDu[],IDcm[],rch[!1 = endsid_8194],sch_8193),HashFunThree(IDu[],PWu[],rcm_u[!1 = @sid_8192])), @sid_444 = @sid_8192, @occ28 = @occ_cst) && mess(RSAP_CH_secure_net[],Rch_8190) && mess(RSAP_CH_secure_net[],sch_8193) -> end(endsid_8194,endCH)
RESULT inj-event(endCH) ==> inj-event(startCH) is true.
-- Query inj-event(endCM) ==> inj-event(startCM)
nounif mess(RSAP_CH_secure_net[],Rch_8416)/-5000
Completing...
200 rules inserted. The rule base contains 187 rules. 30 rules in the queue.
Starting query inj-event(endCM) ==> inj-event(startCM)
RESULT inj-event(endCM) ==> inj-event(startCM) is true.
-- Query not attacker(IDu[])
nounif mess(RSAP_CH_secure_net[],Rch_16177)/-5000
Completing...
200 rules inserted. The rule base contains 188 rules. 22 rules in the queue.
400 rules inserted. The rule base contains 388 rules. 4 rules in the queue.
Starting query not attacker(IDu[])
RESULT not attacker(IDu[]) is true.
-- Query not attacker(SK_CM_CH[])
nounif mess(RSAP_CH_secure_net[],Rch_22239)/-5000
Completing...
200 rules inserted. The rule base contains 188 rules. 22 rules in the queue.
400 rules inserted. The rule base contains 388 rules. 4 rules in the queue.
Starting query not attacker(SK_CM_CH[])
RESULT not attacker(SK_CM_CH[]) is true.
-- Weak secret PWu
Termination warning: v_28809 <> v_28810 && attacker_guess(v_28808,v_28809) && attacker_guess(v_28808,v_28810) -> bad
Selecting 0
Termination warning: v_28812 <> v_28813 && attacker_guess(v_28812,v_28811) && attacker_guess(v_28813,v_28811) -> bad
Selecting 0
nounif mess(RSAP_CH_secure_net[],Rch_29205)/-5000
Completing...
Termination warning: v_28809 <> v_28810 && attacker_guess(v_28808,v_28809) && attacker_guess(v_28808,v_28810) -> bad
Selecting 0
Termination warning: v_28812 <> v_28813 && attacker_guess(v_28812,v_28811) && attacker_guess(v_28813,v_28811) -> bad
Selecting 0
Termination warning: v_32209 <> v_32210 && attacker(v_32209) && attacker_guess(v_32209,v_32210) -> bad
Selecting 1
Termination warning: v_32304 <> v_32305 && attacker(v_32304) && attacker_guess(v_32305,v_32304) -> bad
Selecting 1
200 rules inserted. The rule base contains 192 rules. 58 rules in the queue.
400 rules inserted. The rule base contains 378 rules. 49 rules in the queue.
600 rules inserted. The rule base contains 578 rules. 63 rules in the queue.
800 rules inserted. The rule base contains 778 rules. 58 rules in the queue.
1000 rules inserted. The rule base contains 978 rules. 73 rules in the queue.
1200 rules inserted. The rule base contains 1178 rules. 44 rules in the queue.
RESULT Weak secret PWu is true (bad not derivable).