Contextual Integrity and its FormalizationAnupam Datta CMUFall 2007-08What do I do?uResearch Foundations (Modeling and Analysis) of Cryptographic protocols Privacy Secure systems Using methods from programming languages and cryptography Conferences: IEEE CSF, IEEE S andall negative norms are satisfiedHIPAA Healthcare PrivacyHIPAA consists primarily of positive norms: share phi if some rule explicitly allows it (2), (3), (5), (6)Exception: negative norm about psychotherapy notes (4)COPPA Children Online PrivacyCOPPA consists primarily of negative norms children can share their protected info only if parents consent (7) (condition)(8) (obligation future requirements)Sender roleSubject roleAttributeTransmission principleGLBA Financial InstitutionsRecipient roleFinancial institutions must notify consumers if they share their non-public personal information with non- affiliated companies, but the notification may occur either before or after the information sharing occursRelated LanguagesModelSenderRecipientSubjectAttributesPastFutureCombinationRBACRoleIdentityXACMLFlexibleFlexibleFlexibleooEPALFixedRoleFixedoP3PFixedRoleFixedooLPURoleRoleRoleLegend: unsupported opartially supported fully supported LPU fully supports attributes, combination, temporal conditionsWhy Not Use P3P?uDifferent application P3P understood by web browsers LPU intended for internal policy enforcementuNot expressive enough P3P cannot express HIPAA, GLBA, COPPA Each policy only has one sender and one subject Missing temporal conditions; only has simple opt-in / opt-outOutlineuMotivating Example uFramework uModel uLogic of Privacy and Utility uWorkflows and Responsibility uAlgorithmic Results uWorkflow Design assuming agents responsible uAuditing logs when agents irresponsible uConclusionsNurseSecretaryMyHealthVanderbilt ImprovedPatientDoctorHealth AnswerHealth AnswerHealth QuestionAppointment RequestHealth QuestionNow that I have cancer, Should I eat more vegetables?Health QuestionYes! except broccoliHealth AnswerAssign responsibilities to roles & workflow engineDoctor should answer health questionsGraph-based WorkflowuGraph (R, R x R), where R is the set of roles uEdge-labeling functionpermit: R x R 2T, where T is the set of attributes uResponsibility of workflow engine Allow msg from role r1 to role r2 iff tags(msg) permit(r1, r2) uResponsibility of human agents in roles Tagging responsibilities ensure messages are correctly tagged Progress responsibilities ensure messages proceed through workflowMyHealth ResponsibilitiesuTagging Nurses should tag health questions G p, q, s, m. inrole(p, nurse) send(p, q, m) contains(m, s, health-question) tagged(m, s, health-question) uProgress Doctors should answer health questions G p, q, s, m. inrole(p, doctor) send(q, p, m) contains(m, s, health- question) F m. send(p, s, m) contains(m, s, health-answer)Abstract WorkflowuResponsibility of workflow engine LTL formula Feasible (enforceable) if is a safety formula without the contains() predicateuResponsibility of each role r LTL formula r Feasible if agents have a strategy to discharge their responsibilities p. inrole(p, r) rGraph-based workflows are a special caseOutlineuMotivating Example uFramework uModel uLogic of Privacy and Utility uWorkflows and Responsibility uAlgorithmic Results uWorkflow Design assuming agents responsible uAbstract workflows uAuditing logs when agents irresponsible uOnly graph-based workflows uConclusionsNurseSecretaryMyHealthVanderbilt ImprovedPatientDoctorHealth AnswerHealth AnswerHealth QuestionAppointment RequestHealth QuestionNow that I have cancer, Should I eat more vegetables?Health QuestionYes! except broccoliHealth AnswerMinimal disclosurePrivacy: HIPAA compliance+Utility: Schedule appointments, obtain health answersResponsibility: Doctor should answer health questionsWorkflow Design ResultsuTheorems: Assuming all agents act responsibly, checking whether workflow achieves Privacy is in PSPACE (in the size of the formula describing the workflow) Utility is decidable uDefinition and construction of minimal disclosure workflowAlgorithms implemented in model-checkers, e.g. SPIN, MOCHADeciding PrivacyuPLTL model-checking problem is PSPACE decidableG |= tags-correct U agents-responsible privacy-policyG: concurrent game structureResult applies to finite models (#agents, msgs,) MyHealth PrivacyuMyHealthVanderbilt workflow satisfies this privacy conditionIn all states, only nurses and doctors receive health questionsG p1, p2, q, m send(p1, p2, m) contains(m, q, health-question) inrole(p2, nurse) inrole(p2, doctor) uRun LTL model-checker, e.g. SPINDeciding UtilityuATL* model-checking of concurrent game structures is Decidable with perfect information Undecidable with imperfect information uTheorem: There is a sound decision procedure for de