Verification: open |
Require ModelProperties.
Require AuxiliaryLemmas.
Section openIsSecure.
|
|
Lemma OpenPSS:
(s,t:SFSstate; u:SUBJECT)
(FuncPre5 s)
->(SecureState s)->(TransFunc u s Open t)->(SecureState t).
Intros s t Sub FP5 SS TF; Inversion TF.
Inversion H.
Unfold SecureState DACSecureState SimpleSecurity; Simpl; BreakSS .
Split; Intros.
Elim (OBJeq_dec o o0); Intro EQo.
Rewrite <- EQo.
Elim (SUBeq_dec Sub u0); Intro EQu.
Rewrite <- EQu.
Unfold 1 open_sm PreDACRead PreDACWrite; Simpl.
Cut Cases (fsecmat (secmat s) o) of
(Some y) => (set_In (o,y) (secmat s))
| None => ~(set_In o (DOM OBJeq_dec (secmat s)))
end.
Cut Cases (fsecmat (secmat s) o) of
None => True
| (Some y) => (set_In Sub (ActWriters y))->(PreDACWrite s Sub o)
end.
Elim (fsecmat (secmat s) o).
Intros;
Replace (fsecmat
(set_add SECMATeq_dec
(o,
(mkRW (set_add SUBeq_dec Sub (ActReaders a))
(ActWriters a)))
(set_remove SECMATeq_dec (o,a) (secmat s))) o)
with (Some ReadersWriters
(mkRW (set_add SUBeq_dec Sub (ActReaders a)) (ActWriters a))).
Simpl.
Split; Intros.
Auto.
Unfold PreDACWrite in H9; Apply H9; Auto.
Unfold fsecmat; Apply AddEq1.
Auto.
Intros;
Replace (fsecmat
(set_add SECMATeq_dec
(o,(mkRW (cons Sub (nil SUBJECT)) (empty_set SUBJECT)))
(secmat s)) o)
with (Some ReadersWriters
(mkRW (cons Sub (nil SUBJECT)) (empty_set SUBJECT))).
Simpl.
Split; (Intro H12; Elim H12).
Auto.
Tauto.
Unfold fsecmat; Apply AddEq1; Auto.
Apply ReadWriteImpWrite; Auto.
Unfold fsecmat; Apply DOMFuncRel4.
Cut Cases (fsecmat (open_sm s Sub o READ) o) (fsecmat (secmat s) o) of
(Some y) None =>
(ActReaders y)=(set_add SUBeq_dec Sub (empty_set SUBJECT))
/\(ActWriters y)=(empty_set SUBJECT)
| None _ => False
| (Some y) (Some z) =>
((set_In u0 (ActReaders y))->(set_In u0 (ActReaders z)))
/\((set_In u0 (ActWriters y))->(set_In u0 (ActWriters z)))
end.
Cut Cases (fsecmat (secmat s) o) of
None => True
| (Some y) =>
((set_In u0 (ActReaders y))->(PreDACRead s u0 o))
/\((set_In u0 (ActWriters y))->(PreDACWrite s u0 o))
end.
Unfold PreDACRead PreDACWrite; Simpl; Elim (fsecmat (secmat s) o);
Elim (fsecmat (open_sm s Sub o READ) o).
Tauto.
Auto.
Split; Intros.
Elim H10; Intros.
Absurd Sub=u0; Auto.
Rewrite H12 in H11.
Simpl in H11.
Tauto.
Elim H10; Intros H13 H14; Rewrite H14 in H11; Simpl in H11;
Contradiction.
Auto.
Apply DAC.
Apply Open_smCorr21; Auto.
Replace (fsecmat (open_sm s Sub o READ) o0)
with (fsecmat (secmat s) o0).
Unfold PreDACRead PreDACWrite; Simpl;
Unfold DACSecureState PreDACRead PreDACWrite in DAC; Apply DAC.
Auto.
Elim (OBJeq_dec o o0); Intro EQo.
Rewrite <- EQo.
Elim (SUBeq_dec Sub u0); Intro EQu.
Rewrite <- EQu.
Unfold open_sm; Simpl.
Cut Cases (fsecmat (secmat s) o) of
(Some y) => (set_In (o,y) (secmat s))
| None => ~(set_In o (DOM OBJeq_dec (secmat s)))
end.
Cut Cases (fOSC (objectSC s) o) of
(Some t) =>
Cases (fSSC (subjectSC s) Sub) of
(Some b) => (le_sc t b)
| None => False
end
| None => False
end.
Elim (fsecmat (secmat s) o); Elim (fOSC (objectSC s) o);
Elim (fSSC (subjectSC s) Sub); Contradiction Orelse Auto.
Intros until a1;
Elim (fsecmat
(set_add SECMATeq_dec
(o,
(mkRW (set_add SUBeq_dec Sub (ActReaders a1))
(ActWriters a1)))
(set_remove SECMATeq_dec (o,a1) (secmat s))) o); Auto.
Intros until a0;
Elim (fsecmat
(set_add SECMATeq_dec
(o,(mkRW (cons Sub (nil SUBJECT)) (empty_set SUBJECT)))
(secmat s)) o); Auto.
Auto.
Unfold fsecmat; Apply DOMFuncRel4.
Cut Cases (fsecmat (open_sm s Sub o READ) o) (fsecmat (secmat s) o) of
(Some y) None =>
(ActReaders y)=(set_add SUBeq_dec Sub (empty_set SUBJECT))
/\(ActWriters y)=(empty_set SUBJECT)
| None _ => False
| (Some y) (Some z) =>
((set_In u0 (ActReaders y))->(set_In u0 (ActReaders z)))
/\((set_In u0 (ActWriters y))->(set_In u0 (ActWriters z)))
end.
Cut Cases (fOSC (objectSC s) o) of
(Some t) =>
Cases (fSSC (subjectSC s) Sub) of
(Some b) => (le_sc t b)
| None => False
end
| None => False
end.
Cut Cases
(fsecmat (secmat s) o)
(fOSC (objectSC s) o)
(fSSC (subjectSC s) u0)
of
None _ _ => True
| _ None _ => True
| _ _ None => True
| (Some x) (Some y) (Some z) =>
(set_In u0 (ActReaders x))\/(set_In u0 (ActWriters x))
->(le_sc y z)
end.
Elim (fSSC (subjectSC s) u0); Elim (fsecmat (open_sm s Sub o READ) o);
Elim (fsecmat (secmat s) o); Elim (fOSC (objectSC s) o);
Elim (fSSC (subjectSC s) Sub); Contradiction Orelse Auto.
Tauto.
Intros.
Elim H11; Intros H14 H15; Rewrite H14 in H12; Rewrite H15 in H12;
Simpl in H12; Tauto.
Unfold SimpleSecurity in MAC; Apply MAC; Auto.
Auto.
Apply Open_smCorr21; Auto.
Replace (fsecmat (open_sm s Sub o READ) o0)
with (fsecmat (secmat s) o0).
Unfold SimpleSecurity in MAC; Apply MAC; Auto.
Auto.
Unfold SecureState DACSecureState SimpleSecurity; Simpl; BreakSS .
Split; Intros.
Elim (OBJeq_dec o o0); Intro EQo.
Rewrite <- EQo.
Elim (SUBeq_dec Sub u0); Intro EQu.
Rewrite <- EQu.
Unfold 1 open_sm PreDACRead PreDACWrite; Simpl.
Cut Cases (fsecmat (secmat s) o) of
(Some y) => (set_In (o,y) (secmat s))
| None => ~(set_In o (DOM OBJeq_dec (secmat s)))
end.
Cut Cases (fsecmat (secmat s) o) of
None => True
| (Some y) => (set_In Sub (ActReaders y))->(PreDACRead s Sub o)
end.
Elim (fsecmat (secmat s) o).
Intros;
Replace (fsecmat
(set_add SECMATeq_dec
(o,
(mkRW (ActReaders a)
(set_add SUBeq_dec Sub (ActWriters a))))
(set_remove SECMATeq_dec (o,a) (secmat s))) o)
with (Some ReadersWriters
(mkRW (ActReaders a) (set_add SUBeq_dec Sub (ActWriters a)))).
Simpl.
Split; Intros.
Unfold PreDACRead in H9; Apply H9; Auto.
Auto.
Unfold fsecmat; Apply AddEq1; Auto.
Intros;
Replace (fsecmat
(set_add SECMATeq_dec
(o,(mkRW (empty_set SUBJECT) (cons Sub (nil SUBJECT))))
(secmat s)) o)
with (Some ReadersWriters
(mkRW (empty_set SUBJECT) (cons Sub (nil SUBJECT)))).
Simpl.
Split; (Intro H12; Elim H12).
Auto.
Contradiction.
Unfold fsecmat; Apply AddEq1; Auto.
Apply ReadWriteImpRead; Auto.
Unfold fsecmat; Apply DOMFuncRel4.
Cut Cases (fsecmat (open_sm s Sub o WRITE) o) (fsecmat (secmat s) o) of
(Some y) None =>
(ActWriters y)=(set_add SUBeq_dec Sub (empty_set SUBJECT))
/\(ActReaders y)=(empty_set SUBJECT)
| None _ => False
| (Some y) (Some z) =>
((set_In u0 (ActReaders y))->(set_In u0 (ActReaders z)))
/\((set_In u0 (ActWriters y))->(set_In u0 (ActWriters z)))
end.
Cut Cases (fsecmat (secmat s) o) of
None => True
| (Some y) =>
((set_In u0 (ActReaders y))->(PreDACRead s u0 o))
/\((set_In u0 (ActWriters y))->(PreDACWrite s u0 o))
end.
Unfold PreDACRead PreDACWrite; Simpl; Elim (fsecmat (secmat s) o);
Elim (fsecmat (open_sm s Sub o WRITE) o).
Tauto.
Contradiction.
Split; Intros.
Elim H10; Intros.
Absurd Sub=u0; Auto.
Rewrite H13 in H11.
Simpl in H11.
Tauto.
Elim H10; Intros H13 H14; Rewrite H13 in H11; Simpl in H11;
Tauto.
Auto.
Apply DAC.
Apply Open_smCorr22; Auto.
Replace (fsecmat (open_sm s Sub o WRITE) o0)
with (fsecmat (secmat s) o0).
Unfold PreDACRead PreDACWrite; Simpl;
Unfold DACSecureState PreDACRead PreDACWrite in DAC; Apply DAC.
Auto.
Unfold SimpleSecurity; Intros; Simpl.
Elim (OBJeq_dec o o0); Intro EQo.
Rewrite <- EQo.
Elim (SUBeq_dec Sub u0); Intro EQu.
Rewrite <- EQu.
Unfold open_sm; Simpl.
Cut Cases (fsecmat (secmat s) o) of
(Some y) => (set_In (o,y) (secmat s))
| None => ~(set_In o (DOM OBJeq_dec (secmat s)))
end.
Cut Cases (fOSC (objectSC s) o) of
(Some t) =>
Cases (fSSC (subjectSC s) Sub) of
(Some b) => (le_sc t b)
| None => False
end
| None => False
end.
Elim (fsecmat (secmat s) o); Elim (fOSC (objectSC s) o);
Elim (fSSC (subjectSC s) Sub); Contradiction Orelse Auto.
Intros until a1;
Elim (fsecmat
(set_add SECMATeq_dec
(o,
(mkRW (ActReaders a1)
(set_add SUBeq_dec Sub (ActWriters a1))))
(set_remove SECMATeq_dec (o,a1) (secmat s))) o); Auto.
Intros until a0;
Elim (fsecmat
(set_add SECMATeq_dec
(o,(mkRW (empty_set SUBJECT) (cons Sub (nil SUBJECT))))
(secmat s)) o); Auto.
Auto.
Unfold fsecmat; Apply DOMFuncRel4.
Cut Cases (fsecmat (open_sm s Sub o WRITE) o) (fsecmat (secmat s) o) of
(Some y) None =>
(ActWriters y)=(set_add SUBeq_dec Sub (empty_set SUBJECT))
/\(ActReaders y)=(empty_set SUBJECT)
| None _ => False
| (Some y) (Some z) =>
((set_In u0 (ActReaders y))->(set_In u0 (ActReaders z)))
/\((set_In u0 (ActWriters y))->(set_In u0 (ActWriters z)))
end.
Cut Cases (fOSC (objectSC s) o) of
(Some t) =>
Cases (fSSC (subjectSC s) Sub) of
(Some b) => (le_sc t b)
| None => False
end
| None => False
end.
Cut Cases
(fsecmat (secmat s) o)
(fOSC (objectSC s) o)
(fSSC (subjectSC s) u0)
of
None _ _ => True
| _ None _ => True
| _ _ None => True
| (Some x) (Some y) (Some z) =>
(set_In u0 (ActReaders x))\/(set_In u0 (ActWriters x))
->(le_sc y z)
end.
Elim (fSSC (subjectSC s) u0); Elim (fsecmat (open_sm s Sub o WRITE) o);
Elim (fsecmat (secmat s) o); Elim (fOSC (objectSC s) o);
Elim (fSSC (subjectSC s) Sub); Contradiction Orelse Auto.
Tauto.
Intros.
Elim H11; Intros H14 H15; Rewrite H14 in H12; Rewrite H15 in H12;
Simpl in H12; Tauto.
Unfold SimpleSecurity in MAC; Apply MAC; Auto.
Auto.
Apply Open_smCorr22; Auto.
Replace (fsecmat (open_sm s Sub o WRITE) o0)
with (fsecmat (secmat s) o0).
Unfold SimpleSecurity in MAC; Apply MAC; Auto.
Auto.
Qed.
|
|
Lemma OpenPSP:
(s,t:SFSstate; u:SUBJECT)
(FuncPre5 s)
->(StarProperty s)->(TransFunc u s Open t)->(StarProperty t).
Intros s t Sub FP5 SP TF; Inversion TF.
Inversion H.
Unfold StarProperty; Simpl; Intros.
Cut Cases
(fsecmat (secmat s) o1)
(fsecmat (secmat s) o2)
(fOSC (objectSC s) o2)
(fOSC (objectSC s) o1)
of
None _ _ _ => True
| _ None _ _ => True
| _ _ None _ => True
| _ _ _ None => True
| (Some w) (Some x) (Some y) (Some z) =>
(set_In u0 (ActWriters w))
->(set_In u0 (ActReaders x))
->(le_sc y z)
end.
Elim (OBJeq_dec o o1); Elim (OBJeq_dec o o2); Intros EQ2 EQ1.
Rewrite <- EQ1; Rewrite <- EQ2.
Elim (fsecmat (secmat s) o); Elim (fOSC (objectSC s) o);
Elim (fsecmat (open_sm s Sub o READ) o); Auto.
Rewrite <- EQ1.
Replace (fsecmat (open_sm s Sub o READ) o2)
with (fsecmat (secmat s) o2).
Cut Cases (fsecmat (open_sm s Sub o READ) o) (fsecmat (secmat s) o) of
None _ => False
| (Some y) None =>
(ActReaders y)=(set_add SUBeq_dec Sub (empty_set SUBJECT))
/\(ActWriters y)=(empty_set SUBJECT)
| (Some x) (Some y) =>
(set_In u0 (ActWriters x))->(set_In u0 (ActWriters y))
end.
Elim (fsecmat (secmat s) o); Elim (fOSC (objectSC s) o);
Elim (fsecmat (secmat s) o2);
Elim (fsecmat (open_sm s Sub o READ) o); Elim (fOSC (objectSC s) o2);
Auto.
Intros.
Elim H9; Intros H16 H17; Rewrite H17 in H11; Simpl in H11;
Contradiction.
Apply Open_smCorr31; Auto.
Auto.
Rewrite <- EQ2.
Replace (fsecmat (open_sm s Sub o READ) o1)
with (fsecmat (secmat s) o1).
Elim (SUBeq_dec Sub u0); Intro EQu.
Cut Cases
(fsecmat (secmat s) o1)
(fOSC (objectSC s) o)
(fOSC (objectSC s) o1)
of
None _ _ => False
| _ None _ => False
| _ _ None => False
| (Some x) (Some y) (Some z) =>
(set_In Sub (ActWriters x))->(le_sc y z)
end.
Rewrite <- EQu.
Elim (fsecmat (secmat s) o); Elim (fOSC (objectSC s) o);
Elim (fsecmat (secmat s) o1);
Elim (fsecmat (open_sm s Sub o READ) o); Elim (fOSC (objectSC s) o1);
Auto.
Unfold PreStarPropRead in H6; Apply H6.
Cut Cases (fsecmat (open_sm s Sub o READ) o) (fsecmat (secmat s) o) of
(Some y) None =>
(ActReaders y)=(set_add SUBeq_dec Sub (empty_set SUBJECT))
/\(ActWriters y)=(empty_set SUBJECT)
| None _ => False
| (Some y) (Some z) =>
((set_In u0 (ActReaders y))->(set_In u0 (ActReaders z)))
/\((set_In u0 (ActWriters y))->(set_In u0 (ActWriters z)))
end.
Elim (fsecmat (secmat s) o); Elim (fOSC (objectSC s) o);
Elim (fsecmat (secmat s) o1);
Elim (fsecmat (open_sm s Sub o READ) o); Elim (fOSC (objectSC s) o1);
Auto.
Tauto.
Intros.
Elim H9; Intros H16 H17; Rewrite H16 in H12; Simpl in H12; Elim H12;
Intro; Try Contradiction.
Absurd Sub=u0; Auto.
Apply Open_smCorr21; Auto.
Auto.
Replace (fsecmat (open_sm s Sub o READ) o1)
with (fsecmat (secmat s) o1).
Replace (fsecmat (open_sm s Sub o READ) o2)
with (fsecmat (secmat s) o2).
Auto.
Auto.
Auto.
Unfold StarProperty in SP; Apply SP; Auto.
Unfold StarProperty; Simpl; Intros.
Cut Cases
(fsecmat (secmat s) o1)
(fsecmat (secmat s) o2)
(fOSC (objectSC s) o2)
(fOSC (objectSC s) o1)
of
None _ _ _ => True
| _ None _ _ => True
| _ _ None _ => True
| _ _ _ None => True
| (Some w) (Some x) (Some y) (Some z) =>
(set_In u0 (ActWriters w))
->(set_In u0 (ActReaders x))
->(le_sc y z)
end.
Elim (OBJeq_dec o o1); Elim (OBJeq_dec o o2); Intros EQ2 EQ1.
Rewrite <- EQ1; Rewrite <- EQ2.
Elim (fsecmat (secmat s) o); Elim (fOSC (objectSC s) o);
Elim (fsecmat (open_sm s Sub o WRITE) o); Auto.
Rewrite <- EQ1.
Replace (fsecmat (open_sm s Sub o WRITE) o2)
with (fsecmat (secmat s) o2).
Elim (SUBeq_dec Sub u0); Intro EQu.
Cut Cases
(fsecmat (secmat s) o2)
(fOSC (objectSC s) o)
(fOSC (objectSC s) o2)
of
None _ _ => False
| _ None _ => False
| _ _ None => False
| (Some x) (Some y) (Some z) =>
(set_In Sub (ActReaders x))->(le_sc z y)
end.
Rewrite <- EQu.
Elim (fsecmat (secmat s) o); Elim (fOSC (objectSC s) o);
Elim (fsecmat (secmat s) o2);
Elim (fsecmat (open_sm s Sub o WRITE) o);
Elim (fOSC (objectSC s) o2); Auto.
Unfold PreStarPropWrite in H6; Apply H6.
Cut Cases (fsecmat (open_sm s Sub o WRITE) o) (fsecmat (secmat s) o) of
(Some y) None =>
(ActWriters y)=(set_add SUBeq_dec Sub (empty_set SUBJECT))
/\(ActReaders y)=(empty_set SUBJECT)
| None _ => False
| (Some y) (Some z) =>
((set_In u0 (ActReaders y))->(set_In u0 (ActReaders z)))
/\((set_In u0 (ActWriters y))->(set_In u0 (ActWriters z)))
end.
Elim (fsecmat (secmat s) o); Elim (fOSC (objectSC s) o);
Elim (fsecmat (secmat s) o2);
Elim (fsecmat (open_sm s Sub o WRITE) o);
Elim (fOSC (objectSC s) o2); Auto.
Tauto.
Intros.
Elim H9; Intros H15 H16.
Rewrite H15 in H11; Simpl in H11; Elim H11; Intro; Try Contradiction.
Absurd Sub=u0; Auto.
Apply Open_smCorr22; Auto.
Auto.
Rewrite <- EQ2.
Replace (fsecmat (open_sm s Sub o WRITE) o1)
with (fsecmat (secmat s) o1).
Elim (SUBeq_dec Sub u0); Intro EQu.
Cut Cases (fsecmat (open_sm s Sub o WRITE) o) (fsecmat (secmat s) o) of
(Some y) None =>
(ActWriters y)=(set_add SUBeq_dec Sub (empty_set SUBJECT))
/\(ActReaders y)=(empty_set SUBJECT)
| None _ => False
| (Some y) (Some z) =>
(set_In u0 (ActReaders y))->(set_In u0 (ActReaders z))
end.
Rewrite <- EQu.
Elim (fsecmat (secmat s) o); Elim (fOSC (objectSC s) o);
Elim (fsecmat (secmat s) o1);
Elim (fsecmat (open_sm s Sub o WRITE) o);
Elim (fOSC (objectSC s) o1); Auto.
Intros.
Elim H9; Intros H14 H15; Rewrite H15 in H12; Simpl in H12;
Contradiction.
Apply Open_smCorr32; Auto.
Cut Cases (fsecmat (open_sm s Sub o WRITE) o) (fsecmat (secmat s) o) of
(Some y) None =>
(ActWriters y)=(set_add SUBeq_dec Sub (empty_set SUBJECT))
/\(ActReaders y)=(empty_set SUBJECT)
| None _ => False
| (Some y) (Some z) =>
((set_In u0 (ActReaders y))->(set_In u0 (ActReaders z)))
/\((set_In u0 (ActWriters y))->(set_In u0 (ActWriters z)))
end.
Elim (fsecmat (secmat s) o); Elim (fOSC (objectSC s) o);
Elim (fsecmat (secmat s) o1);
Elim (fsecmat (open_sm s Sub o WRITE) o);
Elim (fOSC (objectSC s) o1); Auto.
Tauto.
Intros.
Elim H9; Intros H14 H15; Rewrite H15 in H12; Simpl in H12;
Contradiction.
Apply Open_smCorr22; Auto.
Auto.
Replace (fsecmat (open_sm s Sub o WRITE) o1)
with (fsecmat (secmat s) o1).
Replace (fsecmat (open_sm s Sub o WRITE) o2)
with (fsecmat (secmat s) o2).
Auto.
Auto.
Auto.
Unfold StarProperty in SP; Apply SP; Auto.
Qed.
|
|
Lemma OpenPCP:
(s,t:SFSstate)(PreservesControlProp s Open t).
Intros; Unfold PreservesControlProp; Intros Sub TF; Inversion TF;
Unfold ControlProperty.
Inversion H.
Split.
Intros.
Split.
Intros;
Absurd (DACCtrlAttrHaveChanged s
(mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s)
(RootGrp s) (SecAdmGrp s) (objectSC s) (acl s)
(open_sm s Sub o READ) (files s) (directories s)) o0);
Auto.
Intros;
Absurd (MACObjCtrlAttrHaveChanged s
(mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s)
(RootGrp s) (SecAdmGrp s) (objectSC s) (acl s)
(open_sm s Sub o READ) (files s) (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)
(open_sm s Sub o READ) (files s) (directories s)) u0);
Auto.
Split.
Intros.
Split.
Intros;
Absurd (DACCtrlAttrHaveChanged s
(mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s)
(RootGrp s) (SecAdmGrp s) (objectSC s) (acl s)
(open_sm s Sub o WRITE) (files s) (directories s)) o0);
Auto.
Intros;
Absurd (MACObjCtrlAttrHaveChanged s
(mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s)
(RootGrp s) (SecAdmGrp s) (objectSC s) (acl s)
(open_sm s Sub o WRITE) (files s) (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)
(open_sm s Sub o WRITE) (files s) (directories s)) u0);
Auto.
Qed.
End openIsSecure.
Hints Resolve OpenPSS OpenPSP OpenPCP.