(*** Efficient Design of a Novel ECC-Based Public Key Scheme for Medical Data Protection by Utilization of NanoPi Fire ***) (* Cha el definition *)(* Note that defining several cha els makes the imp

(*** AKE Scheme ***)(* Data types *)type Key.type Point.type Random.type ID.type Time.(* Cha el Definition *)free net : cha el. (* Private Terms *)free SKij : bitstring [private].free ai : Random [private].free aj : Random [private].free ki : Key [

(*** ISM Key Agreement Scheme ***)(* Cha el Definition *)free net : cha el. (* Private Terms *)free SK_esp_r : bitstring [private].free SK_r_i : bitstring [private].free IDw : bitstring [private].free PWw : bitstring [private].free IDr : bitstring

(********************** Key Establishment Protocol *************************)(* Data types *)type Key.type Point.type Random.type ID.(* Cha el Definition *)free net : cha el. (* Private Terms *)free SSKnm : Key [private].const skm : Key [private].c