Verification: write

Require AuxiliaryLemmas.

Section writeIsSecure.



Lemma WritePSS:
 (s,t:SFSstate; u:SUBJECT)
  (SecureState s)->(TransFunc u s Write t)->(SecureState t).
StartPSS .
Inversion H.
Auto.

Qed.



Lemma WritePSP:
 (s,t:SFSstate; u:SUBJECT)
  (StarProperty s)->(TransFunc u s Write t)->(StarProperty t).
StartPSP .
Inversion H.
Auto.

Qed.



Lemma WritePCP:
    (s,t:SFSstate)(PreservesControlProp s Write t).
Intros; Unfold PreservesControlProp; Intros Sub TF; Inversion TF;
  Unfold ControlProperty.
Inversion H.
Split.
Intros.
Split.
Intro;
  Absurd (DACCtrlAttrHaveChanged s
           (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s)
             (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (secmat s)
             (write_files o n buf) (directories s)) o0); Auto.

Intro;
  Absurd (MACObjCtrlAttrHaveChanged s
           (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s)
             (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (secmat s)
             (write_files o n buf) (directories s)) o0); Auto.

Intros;
  Absurd (MACSubCtrlAttrHaveChanged s
           (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s)
             (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (secmat s)
             (write_files o n buf) (directories s)) u0); Auto.

Qed.


End writeIsSecure.

Hints Resolve WritePSS WritePSP WritePCP.