Thesis

Enforced Privacy: from Practice to Theory

ProVerif Code for AS02

Modelling of the AS02 e-auction protocol
AS02-model.pi

Verifying Verifying strong bidding-price-secrecy for non-winning bidders
AS02-strong-secrecy.pi

ProVerif Code for DLV08

ProVerif model with the original assumptions

Modelling of DLV08 protocol with the original assumptions
Original_Model-Model.pi

Verifying security properties of the original model

Verifying secrecy of patient and doctor information
Original_Model-Secrecy_pt_dr.pi

Verifying authentication of patient and doctor during the patient-doctor sub-protocol
Original_Model-Authentication_pt_dr.pi

Verifying authentication of patient and pharmacist during the patient-pharmacist sub-protocol
Original_Model-Authentication_pt_ph.pi

Verifying classical privacy properties of the original model

Verifying doctor anonymity
Original_Model-Dr_Anonymity.pi

Verifying patient anonymity
Original_Model/Pt_Anonymity.pi

Verifying strong doctor anonymity
Original_Model-Strong_Dr_Anonymity.pi

Verifying strong patient anonymity
Original_Model-Strong_Pt_Anonymity.pi

Verifying doctor untraceability
Original_Model-Dr_untraceability.pi

Verifying patient untraceability
Original_Model-Pt_untraceability.pi

Verifying strong doctor untraceability
Original_Model-Strong_Dr_untraceability.pi

Verifying strong patient untraceability
Original_Model-Strong_Pt_untraceability.pi

Verifying prescribing-privacy
Original_Model-Prescribing-privacy.pi

Showing how to fix the security and privacy problems

Fixing secrecy of patient and doctor information
Fixed_Original_Model-Secrecy_pt_dr.pi

Fixing patient authentication during the patient-doctor sub-protocol
Fixed_Original_Model-Authentication_pt.pi

Fixing patient and pharmacist authentication during the patient-pharmacist sub-protocol
Fixed_Original_Model-Authentication_pt_ph.pi

Fixing doctor anonymity
Fixed_Original_Model-Dr_Anonymity.pi

Fixing strong doctor anonymity
Fixed_Original_Model-Strong_Dr_Anonymity.pi

Fixing patient untraceability
Fixed_Original_Model-Pt_untraceability.pi

Fixing strong doctor untraceability
Fixed_Original_Model-Strong_Dr_untraceability.pi

Fixing strong patient untraceability
Fixed_Original_Model-Strong_Pt_untraceability.pi

Fixing prescribing-privacy
Fixed_Original_Model-Prescribing-privacy.pi

Revised model -- combanation of all the fixes

Revised model
Revised_Model.pi

Verifying properties, which are not satisfied originally, of the revised model

Verifying doctor anonymity
Revised_Model-Dr_Anonymity.pi

Verifying strong doctor anonymity
Revised_Model-Strong_Dr_Anonymity.pi

Verifying doctor untraceability
Revised_Model-Dr_untraceability.pi

Verifying patient untraceability
Revised_Model-Pt_untraceability.pi

Verifying strong doctor untraceability
Revised_Model-Strong_Dr_untraceability.pi

Verifying strong patient untraceability
Revised_Model-Strong_Pt_untraceability.pi

Verifying prescribing-privacy
Revised_Model-Prescribing-privacy.pi

Verifying doctor anonymity
Revised_Model-Dr_Anonymity.pi

Verifying enforced properties of the upadated model -- the model which satisfies prescribing-privacy

Showing the model does not satisfy enforced-prescribing-privacy
Updated_Model-enforced_prescribing_privacy.pi

Verifying pharmacist independent of prescribing-privacy
Updated_Model-Ph_independent_prescribing-privacy.pi

Showing how to fix enforced prescribing-privacy

Fixing enforced prescribing-privacy on the updated model
Fixed_Updated_Model-enforced_ prescribing_privacy.pi

Fixing enforced prescribing-privacy on the original model
Fixed_Original_Model-enforced_ prescribing_privacy.pi

Verifying pharmacist independent of prescribing-privacy
Updated_Model-Ph_independent_prescribing-privacy.pi

Showing the model does not satisfy enforced-prescribing-privacy with chemeleon bit-commitments
Updated_Model-enforced_prescribing-privacy_commitments.pi

Showing the original model does not satisfy pharmacists independent of enforced-prescribing-privacy
Original_Model-pharmacists_independent_of_enforced_prescribing-privacy.pi

Showing the updated model does not satisfy pharmacists independent of enforced-prescribing-privacy with
Updated_Model-pharmacists_independent_of_enforced_prescribing-privacy.pi