Logic Formalization of HIPAA