Appendix A:  Proof System

If a formula q is state-valid, that is valid in all states, then the axiom of tautology defines
	TAU	sdo3(x) q 
That is, if a formula is valid in all states, it is valid in any one state, and can be written as a tautology. 
From the tautology axiom we get the generalisation rule, which states that for a state formula p, if p is valid at a point in the sequence then it is valid over the entire sequence.  For a state formula p,
	GEN	 f(sdo3(x) p, p)
The rule of specification is symmetric to generalisation.  Specification states that a given state formula p that is valid for the sequence is valid at any point in the sequence.  For a state formula p,
	SPEC  f(q,sdo3(x) q)
The rule of instantiation allows us to infer formulae from a given general formula schema by substituting formulae within the schema.  For a formula schema p and a replacement a
	INST  f(p,p[a])
The most frequently used rule is known as modus ponens, used to infer the validity of a formula q given the validity p and p ﬁ q.  Modus ponens is defined as:
	MP 	 f((p, p ﬁ q),q)
These axioms are defined for state formulae instances of p and q, the propositional fragment of the language.  We must therefore expand our deductive system to allow for quantification, using the "-generalisation rule.  For a variable u and formulae p and q(u) such that u has no free occurrences in  p 
	"-GEN	 f(p ﬁ q(u), p ﬁ "u ◊ q(u))
The use of both temporal and quantified formulae allows for instances of the Barcan formulae, 
"w ◊ B ﬁ "w ◊ B
"The Barcan formula is true when each possible world has the same domain of individuals associated with it, i.e. when the range of the quantifier "w is independent of the world (state) in which truth is being evaluated." [Gold92].  This property is satisfied by the models given in this work.

Appendix B:  Necessity of Basic Properties

B.1  Safety 

Safety is violated if a component received unknown or unacceptable input events.  The basic safety properties, if satisfied, ensure that a component will not receive unknown or unacceptable events. 
  
B.1.1  Authenticity
Goal of Authenticity:  No unknown event is produced.  In this section we prove that authenticity, as defined, satisfies this goal.  
Proof:  
Assume that safety is violated by at least one unknown event, that is, there is at least one position in at least one of the output sequences where a component produces an event that is not a defined event.   Prove that authenticity is not satisfied. 
	$x : N ◊ $i : N ◊ " a : Fma{F(i(A)} ◊ s{i}(out)SDO3(x) ÿa 
	= $x : N ◊ $i : N ◊ ÿ$ a : Fma{F(i(A)} ◊ s{i}(out)SDO3(x) a 
	= $x : N ◊ ÿ"i : N ◊ $ a : Fma{F(i(A)} ◊ s{i}(out)SDO3(x) a 
	= ÿ"x : N ◊ "i : N ◊ $ a : Fma{F(i(A)} ◊ s{i}(out)SDO3(x) a 
	= ÿ Authenticity	 								  o

The proof of the violation of the environment assumption of authenticity follows.  Assume that safety is violated by at least one unknown event, that is, there is at least one position in at least one of the sequences where the environment sends an event that is not a defined event.   Prove that authenticity is not satisfied. 
	$x : N ◊ $i : N ◊ " a : Fma{F(i(A)} ◊ s{E}(out)SDO3(x) ÿa 
	= $x : N ◊ $i : N ◊ ÿ$ a : Fma{F(i(A)} ◊ s(E;i)(out)SDO3(x) a 
	= ÿ Authenticity									  o

B.1.2  Integrity
Goal of Integrity:  No unacceptable modificaiton events are received at a component.  
Proof:  
Assume that safety is violated by at least one unacceptable modification event received from either a component or the environment, that is, there is at least one position in at least one of the input sequences containing an unacceptable modficiation event.  Prove that integrity is not satisfied. 
	$x : N ◊ $i : N ◊ " a : Fma{F(A,mod) } ◊  s(NSUP2(+)E;i) SDO3(x) ÿa
	ﬁ ÿ"x : N ◊ "i : N ◊ $ a : Fma{F(A,mod)  F(obs) } ◊  s(NSUP2(+)E;i) SDO3(x) a
= ÿ Integrity									 o

B.1.3  Confidentiality
Goal of Confidentiality:  No unacceptable observation events are received at a component.  
Proof:  
Assume that safety is violated by at least one unacceptable observation event received from either a component or the environment, that is, there is at least one position in at least one of the input sequences containing an unacceptable observation event.  Prove that confidentiality is not satisfied. 
	
	$x : N ◊ $i : N ◊ " a : Fma{F(A,obs) } ◊  s(NSUP2(+)E;i)SDO3(x) ÿa
	ﬁ ÿ"x : N ◊ "i : N ◊ $ a : Fma{F(A,obs) F(mod) } ◊  s(NSUP2(+)E;i)SDO3(x) a
= ÿ Confidentiality								 o

B.1.4  Provenance
Provenance is formally defined as a progress property although it is necessary for the safety of a system.  This is because safety considers the role of the event when it is received yet provenance includes a specification of the temporal behaviour that leads to an event being received. 
Goal of Provenance:  No events are received from an unknown source.  
Proof:  
Assume that safety is violated by at least one event received from an unknown source, that is, there is at least one position in at least one of the input sequences where the event is sent from an unknown source.  Prove that provenance is not satisfied. 
	$x : N ◊ $i : N ◊ "j : N ◊ $ a : Fma{F} ◊ s{i}(in)SDO3(x) ™a Ÿ ÿ s(jSUP3(+)E)(out)SDO3(x) a 
	= ÿ"x : N ◊ "i : N ◊ $j : N ◊ " a : Fma{F} ◊  (s{i}(in)SDO3(x) ™a ﬁ s(jSUP3(+)E)(out)SDO3(x) a )
= ÿ Provenance 						        			 o

B.1.5  Utility
Utility is necessary in that it is the contraposition of provenance.  Viewing a system, by symmetry, we are able to postulate that if no event is received from an unknown source (provenance is satisfied) then so too no event should be sent to an unknown source. 
Goal of Utility:  No events are sent to an unknown source.  
Proof:  
Assume that safety is violated by at least one event sent to an unknown source, that is, there is at least one position in at least one of the input sequences where the event is sent sent unknown source.  Prove that utility is not satisfied. 
	$x : N ◊ $i : N ◊ "j : N ◊ $ a : Fma{F} ◊ s(jSUP3(+)E)(out)SDO3(x) a Ÿ ÿs{i}(in)SDO3(x) ™a  
	= ÿ"x : N ◊ "i : N ◊ $j : N ◊ " a : Fma{F} ◊ (s(jSUP3(+)E)(out)SDO3(x)a ﬁ s{i}(in)SDO3(x)™a)
= ÿ Utility 						        				 o

B.2  Progress

Progress is violated if a component is unable to produce an output in response to a given input. 

B.2.1  Accessibility
Goal of Accessibility:  That every input received at a component will initiate a process at the component.
Proof:  
Assume that an input is received and processing is not initiated.  Prove that accessibility is not satisfied. 
	$x : N ◊ $i : N ◊ $a :Fma{F} ◊ s{i}(in)SDO3(x)a Ÿ s{i}SDO3(x)ÿ(™a) 
	= $x : N ◊ $i : N ◊ $a :Fma{F} ◊ s{i}(in)SDO3(x)a Ÿ ÿ(s{i}SDO3(x)™a) 
	= $x : N ◊ $i : N ◊ $a :Fma{F} ◊ ÿ ( ÿ( s{i}(in)SDO3(x)a) ⁄ s{i}SDO3(x)™a )
= ÿ Accessibility 									 o

B.2.2  Eventual Output
Goal of Eventual Output:  That every process executing at a component will eventually produce an output.

Proof:  
Assume that there is a process that will never produce an output.  Prove that eventual output is not satisfied. 
	$x : N ◊ $i : N ◊ $a :Fma{F} ◊ "b :Fma{F} ◊  s{i}SDO3(x)a Ÿ s{i}(out)SDO3(x)ÿb
	= $x : N ◊ $i : N ◊ $a :Fma{F} ◊ "b :Fma{F} ◊  s{i}SDO3(x)a Ÿ s{i}(out)SDO3(x)ÿ™b
	= $x : N ◊ $i : N ◊ $a :Fma{F} ◊ "b :Fma{F} ◊  ÿ (ÿs{i}SDO3(x)a ⁄ s{i}SDO3(x) ™b )
= ÿ Eventual Output 								 o

B.2.3  Termination
Goal of Termination:  That every process  executing at a component will terminate.
Proof:  
Assume that there is a process that is initiated that does not terminate.  Prove that termination is not satisfied. 
	$x : N ◊ $i : N ◊ $a :Fma{F} ◊ s{i}SDO3(x)a Ÿ s{i}SDO3(x)a 
	= $x : N ◊ $i : N ◊ $a :Fma{F} ◊ ÿ (ÿs{i}SDO3(x)a ⁄ s{i}SDO3(x) (™ÿa) )
= ÿ Termination 									 o

B.2.4  Eventual Progress
Goal of Eventual Progress:  That every process executing at a component will eventually lead to another process executing.
Proof:  
Assume that there is a process that will never lead to another process. Prove that eventual progress is not satisfied. 
	$x : N ◊ $i : N ◊ $a :Fma{F} ◊ "c :Fma{F} ◊  s{i}SDO3(x)™a Ÿ s{i}SDO3(x)ÿc
	= ÿ ("x : N ◊ "i : N ◊ "a :Fma{F} ◊ $c :Fma{F} ◊  (s{i}SDO3(x)™a ﬁ s{i}SDO3(x) ™c ) )
= ÿ Eventual Progress 								 o

B.2.5  Faithfulness
Goal of Faithfulness:  That the component will eventually produce a known, predictable output for every given input.
Proof:  
Assume that there is an input that will not cause an known, predicted output.  Prove that faithfulness is not satisfied. 
	$x : N ◊ $i : N ◊ $ a : F ◊ " b : F ◊ (a;b) Ÿ s{i}(in) SDO3(x) a Ÿ s{i}(out) SDO3(x) ÿb )
	= ÿ "x : N ◊ "i : N ◊ " a : F ◊ $ b : F ◊ ( (a;b) Ÿ s{i}SDO3(x)a ) ﬁ s{i}SDO3(x)™b )
= ÿ Faithfulness 	 								 o

Appendix C:  Proofs of Safety Meta-Properties

In this appendix we include the details of the proofs of the meta-properties of the basic properties.  These meta-properties are proved for each property in the context of the three composite system structures: product, cascade, and feedback.  Where the proof is straightforward or essentially the same as another proof, we omit the details of the proof, indicating only the major steps of the proof.  

Fsup3(isup3(+)j) = Fsup3(i) Fsup3(j) 
Fsup3(isup3(+)j)(i(A),j(A)) = Fsup3(isup3(+)j)(i(A))  Fsup3(isup3(+)j)(j(A)) = Fsup3(i)(A)  Fsup3(j)(A) = Fsup3(isup3(+)j)(A)

C.1  Authenticity

AU ∫ "x : N ◊ "i : N ◊ $ A : Fma{F(i)} ◊ s{i}(out)SDO3(x) A 
AU-E ∫ "x : N ◊ "i : N ◊ $ A : Fma{F(E)} ◊ s{E}(out)SDO3(x) A 

C.1.1  Reflexivity
Examine the reflexivity of authenticity at an arbitrary component.
	sat(Csdo3(i), AU)
	= "x : N ◊ "i,j : N ◊ $ A : Fma{F(i(A,out))} ◊  s(i;E)(out)SDO3(x) A 
Let at least one occurrence of (outsup3(i) Æ environs) be replaced by (outsup3(i) Æ insup3(i))
	= "x : N ◊ "i : N ◊ $ A : Fma{F(i(A,out))} ◊ s(i;Esup3(+)i)(out)SDO3(x) A 
If F(i(A,out) = F(i(A,in,out) then 
	ﬁ "x : N ◊ "i : N ◊ $ A : Fma{F(i(A,in,out))} ◊ s(i;Esup3(+)i)(out)SDO3(x) A 
	ﬁ sat(Cs(R,i), AU)
If F(i(A,out) π F(i(A,in,out) then it is possible that an unacceptable event received as an input from the output of that component will in turn cause an unacceptable, unknown output.
	o(ﬁ,/) sat(Cs(R,i), AU)

The reflexivity of authenticity for the environment is a non-sequiter as it implies that the environment is connected to itself and removed from the components.  The authenticity of the environment is therefore not affected by the reflexive connection of a component with itself.

C.1.2  Transitivity
Product Composition
	sat(&Sup3(P)(Csdo3(i), Csdo3(j)), AU) Ÿ sat(&Sup3(P)(Csdo3(j), Csdo3(k)), AU)
	= "x : N ◊ "i,j,k : N ◊ $ Asdo3(1), Asdo3(2) : Fma{Fsup3(isup3(+)j)(i(A),j(A))} ◊ 
	   $ Bsdo3(1), Bsdo3(2) : Fma{Fsup3(jsup3(+)k)(j(A),k(A))} ◊ s(i;E)(out)SDO3(x)Asdo3(1) Ÿ s(j;E)(out)SDO3(x) Asdo3(2)
	   Ÿ s(j;E)(out)SDO3(x)Bsdo3(1) Ÿ s(k;E)(out)SDO3(x)Bsdo3(2)
If Fsup3(isup3(+)j)(i(A),j(A)) = Fsup3(jsup3(+)k)(j(A),k(A)) = Fsup3(isup3(+)k)(i(A),k(A)) then
	ﬁ "x : N ◊ "i,k : N ◊ $ Csdo3(1), Csdo3(2) : Fma{Fsup3(isup3(+)k)(i(A),k(A))} ◊ 
	   s(i;E)(out)SDO3(x) Csdo3(1) Ÿ s(k;E)(out)SDO3(x) Csdo3(2)
	ﬁ sat(&Sup3(P)(Csdo3(i), Csdo3(k)), AU)
Otherwise
	o(ﬁ,/) sat(&Sup3(P)(Csdo3(i), Csdo3(k)), AU)

Cascade Composition
	sat(&Sup3(C)(Csdo3(i), Csdo3(j)), AU) Ÿ sat(&Sup3(C)(Csdo3(j), Csdo3(k)), AU)
	= "x : N ◊ "i,j,k : N ◊ $ Asdo3(1), Asdo3(2) : Fma{Fsup3(isup3(+)j)(i(A),j(A))} ◊ 
	   $ Bsdo3(1), Bsdo3(2) : Fma{Fsup3(jsup3(+)k)(j(A),k(A))} ◊ s(i;Esup3(+)j)(out)SDO3(x) Asdo3(1) Ÿ s(j;E)(out)SDO3(x) Asdo3(2)  
	   Ÿ s(j;Esup3(+)k)(out)SDO3(x) Bsdo3(1)  Ÿ s(k;E)(out)SDO3(x) Bsdo3(2) 
Let all occurrences of (outsup3(i) Æ insup3(j)) be replaced by (outsup3(i) Æ insup3(k)), and (outsup3(j) Æ insup3(k))  be replaced by (outsup3(j) Æ environs).  	
	= "x : N ◊ "i,j,k : N ◊ $ Asdo3(1), Asdo3(2) : Fma{Fsup3(isup3(+)j)(i(A),j(A))} ◊ 
	   $ Bsdo3(1), Bsdo3(2) : Fma{Fsup3(jsup3(+)k)(j(A),k(A))} ◊  s(i;Esup3(+)k)(out)SDO3(x) Asdo3(1) Ÿ s(j;E)(out)SDO3(x) Asdo3(2)   
	   Ÿ s(j;Esup3())(out)SDO3(x) Bsdo3(1) Ÿ s(k;E)(out)SDO3(x) Bsdo3(2)  
If Fsup3(isup3(+)j)(i(A),j(A)) = Fsup3(jsup3(+)k)(j(A),k(A)) = Fsup3(isup3(+)k)(i(A),k(A)) then
	ﬁ "x : N ◊ "i,j,k : N ◊ $ Csdo3(1), Csdo3(2) : Fma{Fsup3(isup3(+)k)(i(A),k(A))} ◊ 
	   s(i;Esup3(+)k)(out)SDO3(x) Csdo3(1) Ÿ s(k;E)(out)SDO3(x) Csdo3(2)  
	ﬁ sat(&Sup3(C)(Csdo3(i), Csdo3(k)), AU)
Otherwise
	o(ﬁ,/) sat(&Sup3(C)(Csdo3(i), Csdo3(k)), AU)

Feedback Composition
	sat(&Sup3(F)(Csdo3(i), Csdo3(j)), AU) Ÿ sat(&Sup3(F)(Csdo3(j), Csdo3(k)), AU)
	= "x : N ◊ "i,j,k : N ◊ $ Asdo3(1), Asdo3(2) : Fma{Fsup3(isup3(+)j)(i(A),j(A))} ◊ 
	   $ Bsdo3(1), Bsdo3(2) : Fma{Fsup3(jsup3(+)k)(j(A),k(A))} ◊ s(i;Esup3(+)j)(out)SDO3(x) Asdo3(1) Ÿ s(j;Esup3(+)i)(out)SDO3(x) Asdo3(2)  
	   Ÿ s(j;Esup3(+)k)(out)SDO3(x) Bsdo3(1) Ÿ s(k;Esup3(+)j)(out)SDO3(x) Asdo3(2) 
	= "x : N ◊ "i,j,k : N ◊ $ Asdo3(1), Asdo3(2), Asdo3(3), Asdo3(4) : Fma{Fsup3(isup3(+)j)(i(A),j(A))} ◊ 
	   $ Bsdo3(1), Bsdo3(2), Bsdo3(3), Bsdo3(4) : Fma{Fsup3(jsup3(+)k)(j(A),k(A))} ◊ 
	   s(i;Esup3())(out)SDO3(x) Asdo3(1) Ÿ s(i;j)(out)SDO3(x) Asdo3(3) Ÿ s(j;E)(out)SDO3(x) Asdo3(2) Ÿ s(j;i)(out)SDO3(x) Asdo3(4)  
	   Ÿ s(j;E)(out)SDO3(x) Bsdo3(1) Ÿ s(j;k)(out)SDO3(x) Bsdo3(3) 
	   Ÿ s(k;E)(out)SDO3(x) Bsdo3(2) Ÿ s(k;j)(out)SDO3(x) Bsdo3(4) 
Let all occurrences of (outsup3(i) Æ insup3(j)) be replaced by (outsup3(i) Æ insup3(k)), (outsup3(j) Æ insup3(i)) be replaced by (outsup3(k) Æ insup3(i)), (outsup3(j) Æ insup3(k)) be replaced by (outsup3(i) Æ insup3(k)),  (outsup3(k) Æ insup3(j))  be replaced by (outsup3(k) Æ insup3(i))  	
	= "x : N ◊ "i,j,k : N ◊ $ Asdo3(1), Asdo3(2), Asdo3(3), Asdo3(4) : Fma{Fsup3(isup3(+)j)(i(A),j(A))} ◊ 
	   $ Bsdo3(1), Bsdo3(2), Bsdo3(3), Bsdo3(4) : Fma{Fsup3(jsup3(+)k)(j(A),k(A))} ◊ 
	   s(i;Esup3())(out)SDO3(x)Asdo3(1) Ÿ s(i;k)(out)SDO3(x) Asdo3(3) Ÿ s(j;E)(out)SDO3(x)Asdo3(2) Ÿ s(k;i)(out)SDO3(x) Asdo3(4)
	   Ÿ s(j;E)(out)SDO3(x) Bsdo3(1) Ÿ s(i;k)(out)SDO3(x) Bsdo3(3) 
	   Ÿ s(k;E)(out)SDO3(x) Bsdo3(2) Ÿ s(k;i)(out)SDO3(x) Bsdo3(4) 

If Fsup3(isup3(+)j)(i(A),j(A)) = Fsup3(jsup3(+)k)(j(A),k(A)) = Fsup3(isup3(+)k)(i(A),k(A)) then
	ﬁ "x :N ◊ "i,k :N ◊ $ Csdo3(1), Csdo3(2), Csdo3(3), Csdo3(4) :Fma{Fsup3(isup3(+)k)(i(A),k(A))} ◊    
	   s(i;Esup3())(out)SDO3(x) Csdo3(1) Ÿ s(i;k)(out)SDO3(x) Csdo3(3) 
	   Ÿ s(k;E)(out)SDO3(x) Csdo3(2) Ÿ s(k;i)(out)SDO3(x) Csdo3(4) 
	= "x :N ◊ "i,k :N ◊ $ Csdo3(1), Csdo3(2):Fma{Fsup3(isup3(+)k)(i(A),k(A))} ◊    
	   s(i;Esup3(+)k)(out)SDO3(x) Csdo3(1) Ÿ s(k;Esup3(+)i)(out)SDO3(x) Csdo3(2) 
	ﬁ sat(&Sup3(F)(Csdo3(i), Csdo3(k)), AU)
Otherwise
	o(ﬁ,/) sat(&Sup3(F)(Csdo3(i), Csdo3(k)), AU)

C.1.3  Symmetry
Product Composition
	sat(&Sup3(P)(Csdo3(i), Csdo3(j)), AU) 
	= "x :N ◊ "i,j :N ◊ $ Asdo3(1), Asdo3(2) : Fma{Fsup3(isup3(+)j)(i(A),j(A))} ◊ 
	   s(i;E)(out)SDO3(x) Asdo3(1) Ÿ s(j;E)(out)SDO3(x) Asdo3(2) 
	= sat(&Sup3(P)(Csdo3(j), Csdo3(i)), AU)

Cascade Composition
	sat(&Sup3(C)(Csdo3(i), Csdo3(j)), AU) 
	= "x :N ◊ "i,j :N ◊ $ Asdo3(1), Asdo3(2) : Fma{Fsup3(isup3(+)j)(i(A),j(A))} ◊ 
	   s(i;Esup3(+)j)(out)SDO3(x) Asdo3(1) Ÿ s(j;E)(out)SDO3(x) Asdo3(2) 
Let the connections (outsup3(i) Æ insup3(j)) be replaced by (outsup3(i) Æ environs) and at least one occurrence of (outsup3(j) Æ environs) be replaced by (outsup3(j) Æ insup3(i)).  	
	= "x :N ◊ "i,j :N ◊ $ Asdo3(1), Asdo3(2) : Fma{Fsup3(isup3(+)j)(i(A),j(A))} ◊ 
	   s(i;E)(out)SDO3(x) Asdo3(1) Ÿ s(j;Esup3(+)i)(out)SDO3(x) Asdo3(2) 
	ﬁ sat(&Sup3(C)(Csdo3(j), Csdo3(i)), AU)

C.1.4  Closure
	sat(Csdo3(i), AU) Ÿ sat(Csdo3(j), AU)
	= "x :N ◊ "i,j :N ◊ $ A : Fma{Fsup3(i)(i(A))} ◊ $ B : Fma{Fsup3(j)(j(A))} ◊
	   s(i;Nsup3(+)E)(out)SDO3(x) A Ÿ s(j;Nsup3(+)E)(out)SDO3(x) B
Product Composition
	= "x :N ◊ "i,j :N ◊ $ A : Fma{Fsup3(i)(i(A))} ◊ $ B : Fma{Fsup3(j)(j(A))} ◊
	   s(i;E)(out)SDO3(x) A Ÿ s(j;E)(out)SDO3(x) B
If Fsup3(i)(i(A)) = Fsup3(j)(j(A)) then 
	ﬁ "x : N ◊ "i,j : N ◊ $ Csdo3(1), Csdo3(2) : Fma{Fsup3(isup3(+)j)(i(A),j(A))} ◊ 
	   s(i;E)(out)SDO3(x) Csdo3(1) Ÿ s(j;E)(out)SDO3(x) Csdo3(2)
	ﬁ sat(&Sup3(P)(Csdo3(i), Csdo3(j)), AU)
Otherwise 
	o(ﬁ,/) sat(&Sup3(P)(Csdo3(i), Csdo3(j)), AU)

Cascade Composition
	= "x :N ◊ "i,j :N ◊ $ A : Fma{Fsup3(i)(i(A))} ◊ $ B : Fma{Fsup3(j)(j(A))} ◊
	   s(i;E)(out)SDO3(x) A Ÿ s(j;E)(out)SDO3(x) B
Let at least one connection (outsup3(i) Æ environs) be replaced by (outsup3(i) Æ insup3(j)).  	
	= "x :N ◊ "i,j :N ◊ $ A : Fma{Fsup3(i)(i(A))} ◊ $ B : Fma{Fsup3(j)(j(A))} ◊
	   s(i;Esup3(+)j)(out)SDO3(x) Asdo3() Ÿ s(j;E)(out)SDO3(x) B 
If Fsup3(i)(i(A)) = Fsup3(j)(j(A)) then 
	ﬁ "x : N ◊ "i,j : N ◊ $ A,B : Fma{Fsup3(isup3(+)j)(i(A),j(A))} ◊ 
	   s(i;jsup3(+)E)(out)SDO3(x) A Ÿ s(j;E)(out)SDO3(x) B
	ﬁ sat(&Sup3(C)(Csdo3(i), Csdo3(j)), AU)
Otherwise 
	o(ﬁ,/) sat(&Sup3(C)(Csdo3(i), Csdo3(j)), AU)

Feedback Composition
	= "x :N ◊ "i,j :N ◊ $ A : Fma{Fsup3(i)(i(A))} ◊ $ B : Fma{Fsup3(j)(j(A))} ◊
	   s(i;E)(out)SDO3(x) A Ÿ s(j;E)(out)SDO3(x) B
Let at least one connection (outsup3(i) Æ environs) be replaced by (outsup3(i) Æ insup3(j)) and let at least one connection (outsup3(j) Æ environs) be replaced by (outsup3(j) Æ insup3(i)) .  	
	= "x :N ◊ "i,j :N ◊ $ A : Fma{Fsup3(i)(i(A))} ◊ $ B : Fma{Fsup3(j)(j(A))} ◊
	   s(i;Esup3(+)j)(out)SDO3(x) Asdo3() Ÿ s(j;Esup3(+)i)(out)SDO3(x) B 
If Fsup3(i)(i(A)) = Fsup3(j)(j(A)) then 
	ﬁ "x : N ◊ "i,j : N ◊ $ A,B : Fma{Fsup3(isup3(+)j)(i(A),j(A))} ◊ 
	   s(i;jsup3(+)E)(out)SDO3(x) A Ÿ s(j;isup3(+)E)(out)SDO3(x) B 
	ﬁ sat(&Sup3(F)(Csdo3(i), Csdo3(j)), AU)
Otherwise 
	o(ﬁ,/) sat(&Sup3(F)(Csdo3(i), Csdo3(j)), AU)

C.2  Pessimistic Confidentiality and Integrity

PC ∫ "x :N ◊ "i :N ◊ $ A :Fma {F(N(A),obs)  F(N,mod) } ◊  s(Nsup3(+)E;i)(in)SDO3(x) A
PI ∫ "x :N ◊ "i :N ◊ $ A :Fma{F(N,obs)  F(N(A),mod) } ◊  s(Nsup3(+)E;i)(in)SDO3(x) A

C.2.1  Reflexivity 
	sat(Csdo3(i), PC)
	= "x :N ◊ "i : N ◊ $ A :Fma{F(i(A),obs)  F(i,mod) } ◊ s(E;i)(in)SDO3(x) A  
Following the same reasoning as with authenticity, if F(i(A,out),obs) Õ F(i(A),obs) then all outputs of a component are acceptable as inputs to that component.
	ﬁ sat(Csdo3(R,i), PC)
Otherwise,
	o(ﬁ,/)  sat(Csdo3(R,i), PC)
The (ir)reflexivity of pessimistic integrity immediately follows, as the (obs, mod) dual of the reflexivity of pessimistic confidentiality.

C.2.2  Transitivity
Product Composition
	sat(&Sup3(P)(Csdo3(i), Csdo3(j)),PI) Ÿ sat(&Sup3(P)(Csdo3(j), Csdo3(k)),PI)
If Fsup3(isup3(+)j)(i,j,obs) = Fsup3(jsup3(+)k)(j,k,obs) = Fsup3(isup3(+)k)(i,k,obs) and
Fsup3(isup3(+)j)(i(A),j(A),mod) = Fsup3(jsup3(+)k)(j(A),k(A),mod) = Fsup3(isup3(+)k)(i(A),k(A),mod) then
	ﬁ sat(&Sup3(P)(Csdo3(i), Csdo3(k)),PI)
Otherwise
	o(ﬁ,/) sat(&Sup3(P)(Csdo3(i), Csdo3(k)),PI)

Cascade Composition
	sat(&Sup3(C)(Csdo3(i), Csdo3(j)),PI) Ÿ sat(&Sup3(C)(Csdo3(j), Csdo3(k)),PI)
Let all occurrences of (outsup3(i) Æ insup3(j)) be replaced by (outsup3(i) Æ insup3(k)), and (outsup3(j) Æ insup3(k))  be replaced by (outsup3(j) Æ environs).  If Fsup3(isup3(+)j)(i,j,obs) = Fsup3(jsup3(+)k)(j,k,obs) = Fsup3(isup3(+)k)(i,k,obs) and 
Fsup3(isup3(+)j)(i(A),j(A),mod) = Fsup3(jsup3(+)k)(j(A),k(A),mod) = Fsup3(isup3(+)k)(i(A),k(A),mod) then
	ﬁ sat(&Sup3(C)(Csdo3(i), Csdo3(k)),PI)
Otherwise,
	o(ﬁ,/) sat(&Sup3(C)(Csdo3(i), Csdo3(k)),PI)

Feedback Composition
	sat(&Sup3(F)(Csdo3(i), Csdo3(j)),PI) Ÿ sat(&Sup3(F)(Csdo3(j), Csdo3(k)),PI)
Let all occurrences of (outsup3(i) Æ insup3(j)) be replaced by (outsup3(i) Æ insup3(k)), (outsup3(j) Æ insup3(i)) by (outsup3(k) Æ insup3(i)), (outsup3(j) Æ insup3(k)) by (outsup3(i) Æ insup3(k)),  (outsup3(k) Æ insup3(j))  by (outsup3(k) Æ insup3(i)).  If Fsup3(isup3(+)j)(i,j,obs) = Fsup3(jsup3(+)k)(j,k,obs) = Fsup3(isup3(+)k)(i,k,obs) and Fsup3(isup3(+)j)(i(A),j(A),mod) = Fsup3(jsup3(+)k)(j(A),k(A),mod) = Fsup3(isup3(+)k)(i(A),k(A),mod) then
	ﬁ sat(&Sup3(F)(Csdo3(i), Csdo3(k)),PI)
Otherwise
	o(ﬁ,/) sat(&Sup3(F)(Csdo3(i), Csdo3(k)),PI)

The (in)transitivity of pessimistic confidentiality immediately follows, as the (obs, mod) dual of the transitivity of pessimistic integrity.

C.2.3  Symmetry 
Product Composition
	sat(&Sup3(P)(Csdo3(i), Csdo3(j)),PC) 
	= "x :N ◊ "i : {i,j} ◊ $ A,B :Fma{Fsup3(isup3(+)j)(i(A),j(A),obs)  Fsup3(isup3(+)j)(i,j,mod) } ◊  
	   s(E;i)(in) SDO3(x) A Ÿ s(E;j)(in) SDO3(x) B 
	ﬁ sat(&Sup3(P)(Csdo3(j), Csdo3(i)),PC)

Cascade Composition
	sat(&Sup3(P)(Csdo3(i), Csdo3(j)),PI) 
	= "x :N ◊ "i : {i,j} ◊ $ A,B :Fma {Fsup3(isup3(+)j)(i(A),j(A),obs)  Fsup3(isup3(+)j)(i,j,mod) } ◊  
	   s(E;i)(in) SDO3(x) A Ÿ s(isup3(+)E;j)(in) SDO3(x) B 
Let the connections (outsup3(i) Æ insup3(j)) be replaced by (outsup3(i) Æ environs) and at least one occurrence of (outsup3(j) Æ environs) be replaced by (outsup3(j) Æ insup3(i)).  	
	= "x :N ◊ "i : {i,j} ◊ $ A,B :Fma {Fsup3(isup3(+)j)(i(A),j(A),obs)  Fsup3(isup3(+)j)(i,j,mod) } ◊  
	   s(jsup3(+)E;i)(in) SDO3(x) A Ÿ s(E;j)(in) SDO3(x) B 
By definition, the output events produced by component j are defined as Fsup3(isup3(+)j)(j(A,out)). If Fsup3(isup3(+)j)(j(A,out)) Ã {Fsup3(isup3(+)j)(i,j,obs)  Fsup3(isup3(+)j)(i(A),j(A),mod)} then 
	ﬁ sat(&Sup3(P)(Csdo3(j), Csdo3(i)),PC)
Otherwise 
	o(ﬁ,/) sat(&Sup3(P)(Csdo3(j), Csdo3(i)),PC)

The (a)symmetry of pessimistic integrity immediately follows, as the (obs,mod) dual of the symmetry of pessimistic confidentiality.

C.2.4  Closure
sat(Csdo3(i), PI) Ÿ sat(Csdo3(j), PI)
	= "x :N ◊ "i : {i,j} ◊ $ A :Fma {Fsup3(i)(i(A),obs)  Fsup3(i)(i,mod) } ◊  
	   $ B :Fma {Fsup3(j)(j(A),obs)  Fsup3(j)(j,mod) } ◊  
	   s(E;i)(in) SDO3(x) A Ÿ s(E;j)(in) SDO3(x) B 
Product Composition
If Fsup3(i)(i,obs) = Fsup3(j)(j,obs) and Fsup3(i)(i(A),mod) = Fsup3(j)(j(A),mod) then
	ﬁ sat(&Sup3(P)(Csdo3(i), Csdo3(j)), PI)
Otherwise
	o(ﬁ,/) sat(&Sup3(P)(Csdo3(i), Csdo3(j)), PI)

Cascade Composition
If Fsup3(i)(i,obs) = Fsup3(j)(j,obs) and Fsup3(i)(i(A),mod) = Fsup3(j)(j(A),mod) and 
Fsup3(isup3(+)j)(j(A,out)) Ã {Fsup3(isup3(+)j)(i,j,obs)  Fsup3(isup3(+)j)(i(A),j(A),mod) } then
	ﬁ sat(&Sup3(C)(Csdo3(i), Csdo3(j)), PI)
Otherwise
	o(ﬁ,/) sat(&Sup3(C)(Csdo3(i), Csdo3(j)), PI)

Feedback Composition
If Fsup3(i)(i,obs) = Fsup3(j)(j,obs) and Fsup3(i)(i(A),mod) = Fsup3(j)(j(A),mod) and 
Fsup3(isup3(+)j)(j(A,out)) Ã {Fsup3(isup3(+)j)(i,j,obs)  Fsup3(isup3(+)j)(i(A),j(A),mod) } and 
Fsup3(isup3(+)j)(i(A,out)) Ã {Fsup3(isup3(+)j)(i,j,obs)  Fsup3(isup3(+)j)(i(A),j(A),mod) } then
	ﬁ sat(&Sup3(F)(Csdo3(i), Csdo3(j)), PI)
Otherwise
	o(ﬁ,/) sat(&Sup3(F)(Csdo3(i), Csdo3(j)), PI)

The closure properties pessimistic confidentiality immediately follow as the (obs, mod) dual of the transitivity of pessimistic integrity.

C.3  Environment Optimistic Confidentiality and Integrity

EOC ∫ "x : N ◊ "i :  N ◊  
	$ A : Fma{F(N(A),obs)  F(N,mod)} ◊ $ B : Fma{F(i,obs)  F (i,mod)} ◊ 
	A,B Œ Fma{F(i(A),obs)  F(i,mod)} Ÿ s(N;i)(in)SDO3(x) A Ÿ s(E;i)(in) SDO3(x) B
EOI ∫ "x : N ◊ "i :  N ◊ 
	$ A : Fma{F(N,obs)  F(N(A),mod)} ◊ $ B : Fma{F(i,obs)  F (i,mod)} ◊ 
	A,B Œ Fma{F(i,obs)  F(i(A),mod)} Ÿ s(N;i)(in) SDO3(x) A Ÿ s(E;i)(in) SDO3(x) B

C.3.1  Reflexivity 
	sat(Csdo3(i), EOC)
	= "x : N ◊ "i : N ◊ $ B : Fma{F(i,obs)  F(i,mod)} ◊ 
	   B Œ Fma{F(i(A),obs)  F(i,mod)} Ÿ s(E;i)(in) SDO3(x) B  
Followign the same arguement as with pessimistic confidentiality
	o(ﬁ,/)  sat(Csdo3(R,i), PC)

The reflexivity of environment optimistic integrity immediately follows, as the (obs, mod) dual of the reflexivity of environment optimistic confidentiality.

C.3.2  Transitivity
Product Composition
sat(&Sup3(P)(Csdo3(i), Csdo3(j)),EOI) Ÿ sat(&Sup3(P)(Csdo3(j), Csdo3(k)),EOI)
If Fsup3(isup3(+)j)(i,j,obs) = Fsup3(jsup3(+)k)(j,k,obs) = Fsup3(isup3(+)k)(i,k,obs) and Fsup3(isup3(+)j)(i(A),j(A),mod) = Fsup3(jsup3(+)k)(j(A),k(A),mod) = Fsup3(isup3(+)k)(i(A),k(A),mod) and environment trusted not to send unacceptable events to k then  
 	ﬁ "x : N ◊ "i : {i,j} ◊ $ Csdo3(1) :Fma{Fsup3(isup3(+)k)(i,obs)  Fsup3(isup3(+)k)(i,mod)} ◊ 
	   $ Csdo3(2) : Fma{Fsup3(isup3(+)k)(k,obs)  Fsup3(isup3(+)k)(k,mod)} ◊ 
	   Csdo3(1) : Œ Fma{Fsup3(isup3(+)k)(i,obs)  Fsup3(isup3(+)k)(i(A),mod)} Ÿ s(E;i)(in) SDO3(x) Csdo3(1)   
	    Ÿ Csdo3(2)  Œ Fma{Fsup3(isup3(+)k)(k,obs)  Fsup3(isup3(+)k)(k(A),mod)} Ÿ s(E;k)(in) SDO3(x) Csdo3(2)  
	ﬁ sat(&Sup3(P)(Csdo3(i), Csdo3(k)),EOI)
Otherwise
 	o(ﬁ,/) sat(&Sup3(P)(Csdo3(i), Csdo3(k)),EOI)

Cascade Composition
sat(&Sup3(C)(Csdo3(i), Csdo3(j)),EOI) Ÿ sat(&Sup3(C)(Csdo3(j), Csdo3(k)),EOI)
As with product composition, if Fsup3(isup3(+)j)(i,j,obs) = Fsup3(jsup3(+)k)(j,k,obs) = Fsup3(isup3(+)k)(i,k,obs) and Fsup3(isup3(+)j)(i(A),j(A),mod) = Fsup3(jsup3(+)k)(j(A),k(A),mod) = Fsup3(isup3(+)k)(i(A),k(A),mod) and Fsup3(i)(i(A,out)) Ã {Fsup3(isup3(+)k)(i(A),k(A),mod)  Fsup3(isup3(+)k)(i,k,mod) } and environment trusted not to send unacceptable events to k then  
	ﬁ sat(&Sup3(C)(Csdo3(i), Csdo3(k)),EOI)
Otherwise
	o(ﬁ,/) sat(&Sup3(C)(Csdo3(i), Csdo3(k)),EOI)

Feedback Composition
sat(&Sup3(F)(Csdo3(i), Csdo3(j)),EOI) Ÿ sat(&Sup3(F)(Csdo3(j), Csdo3(k)),EOI)
As with product composition, if Fsup3(isup3(+)j)(i,j,obs) = Fsup3(jsup3(+)k)(j,k,obs) = Fsup3(isup3(+)k)(i,k,obs) and Fsup3(isup3(+)j)(i(A),j(A),mod) = Fsup3(jsup3(+)k)(j(A),k(A),mod) = Fsup3(isup3(+)k)(i(A),k(A),mod) and environment trusted not to send unacceptable events to k then  
	ﬁ sat(&Sup3(C)(Csdo3(i), Csdo3(k)),EOI)
Otherwise
	o(ﬁ,/) sat(&Sup3(C)(Csdo3(i), Csdo3(k)),EOI)

The (in)transitivity of pessimistic confidentiality immediately follows, as the (obs, mod) dual of the transitivity of pessimistic integrity.

C.3.3  Symmetry 
Product Composition
	sat(&Sup3(P)(Csdo3(i), Csdo3(j)),EOC) 
As with pessimistic confidentiality
	ﬁ sat(&Sup3(P)(Csdo3(j), Csdo3(i)),EOC)

Cascade Composition
	sat(&Sup3(C)(Csdo3(i), Csdo3(j)),EOC) 
Let the connections (outsup3(i) Æ insup3(j)) be replaced by (outsup3(i) Æ environs) and at least one occurrence of (outsup3(j) Æ environs) be replaced by (outsup3(j) Æ insup3(i)).  If Fsup3(i)(i(A,out)) Ã { Fsup3(isup3(+)k)(i(A),k(A),mod)  Fsup3(isup3(+)k)(i,k,mod) } then  
	ﬁ sat(&Sup3(C)(Csdo3(j), Csdo3(i)),EOC)
Otherwise
	o(ﬁ,/) sat(&Sup3(C)(Csdo3(j), Csdo3(i)),EOC)

The (a)symmetry of pessimistic integrity immediately follows, as the (obs,mod) dual of the symmetry of pessimistic confidentiality.

C.3.4  Closure
sat(Csdo3(i), EOI) Ÿ sat(Csdo3(j), EOI)
	= "x : N ◊ "i : {i} ◊ $ A : Fma{Fsup3(i)(i,obs)  Fsup3(i)(i(A),mod)} ◊  
	   $ B : Fma{Fsup3(i)(obs)  Fsup3(i)(mod)} ◊   
	   B Œ Fma{Fsup3(i)(i,obs)  Fsup3(i)(i(A),,mod)} Ÿ s(N;i)(in)SDO3(x) A Ÿ s(E;i)(in) SDO3(x) B  
	 Ÿ "x : N ◊ "j : {j} ◊ $ C : Fma{Fsup3(j)(j,obs)  Fsup3(j)(j(A),mod)} ◊  
	   $ D : Fma{Fsup3(j)(obs)  Fsup3(j)(mod)} ◊   
	   D Œ Fma{Fsup3(j)(j,obs)  Fsup3(j)(j(A),mod)} Ÿ s(N;i)(in)SDO3(x) C Ÿ s(E;i)(in) SDO3(x) D 

Product Composition
	sat(Csdo3(i), EOI) Ÿ sat(Csdo3(j), EOI)
If Fsup3(i)(i,obs) = Fsup3(j)(j,obs) and Fsup3(i)(i(A),mod) = Fsup3(j)(j(A),mod) and environment trusted not to send unacceptable events to i or j then
	ﬁ sat(&Sup3(P)(Csdo3(i), Csdo3(j)), EOI)

Otherwise
	o(ﬁ,/) sat(&Sup3(P)(Csdo3(i), Csdo3(j)), EOI)

Cascade Composition
	sat(Csdo3(i), EOI) Ÿ sat(Csdo3(j), EOI)
If Fsup3(i)(i,obs) = Fsup3(j)(j,obs) and Fsup3(i)(i(A),mod) = Fsup3(j)(j(A),mod) and Fsup3(isup3(+)j)(j(A,out)) Ã { Fsup3(isup3(+)j)(i,j,obs)  Fsup3(isup3(+)j)(i(A),j(A),mod) } and environment trusted not to send unacceptable events to i or j then
	ﬁ sat(&Sup3(C)(Csdo3(i), Csdo3(j)), EOI)
Otherwise
	o(ﬁ,/) sat(&Sup3(C)(Csdo3(i), Csdo3(j)), EOI)

Feedback Composition
	sat(Csdo3(i), EOI) Ÿ sat(Csdo3(j), EOI)
If Fsup3(i)(i,obs) = Fsup3(j)(j,obs) and Fsup3(i)(i(A),mod) = Fsup3(j)(j(A),mod) and 
Fsup3(isup3(+)j)(i(A,out)) Ã { Fsup3(isup3(+)j)(i,j,obs)  Fsup3(isup3(+)j)(i(A),j(A),mod) } and 
Fsup3(isup3(+)j)(j(A,out)) Ã {Fsup3(isup3(+)j)(i,j,obs)  Fsup3(isup3(+)j)(i(A),j(A),mod) } and environment trusted not to send unacceptable events to i or j then
	ﬁ sat(&Sup3(F)(Csdo3(i), Csdo3(j)), EOI)
Otherwise
	o(ﬁ,/) sat(&Sup3(F)(Csdo3(i), Csdo3(j)), EOI)

The closure properties environment optimistic confidentiality immediately follows, as the (obs, mod) dual of the closure properties of environment optimistic integrity.

C.4  Component Optimistic Confidentiality and Integrity

COC ∫ "x : N ◊ "i : N ◊ $ A : Fma{F(obs)  F(mod)} ◊ 
	$ B : Fma{F(N(A),obs)  F(N,mod)} ◊ 
	A Œ Fma{Fma{F(i(A),obs)  F(mod)} Ÿ s(N;i)(in)SDO3(x) A Ÿ s(E;i)(in) SDO3(x) B
COI ∫ "x : N ◊ "i : N ◊ $ A : Fma{F(obs)  F(mod)} ◊ 
	$ B : Fma{F(N,obs)  F(N(A),mod)} ◊ 
	A Œ Fma{F(obs)  F(i(A),mod)} Ÿ s(N;i)(in)SDO3(x) A Ÿ s(E;i)(in) SDO3(x) B

C.4.1  Reflexivity
	sat(Csdo3(i), COC)
As with pessimistic confidentiality 
 	o(ﬁ,/)  sat(Csdo3(R,i), COC)

The (ir)reflexivity of environment optimistic integrity immediately follows, as the (obs, mod) dual of the reflexivity of environment optimistic confidentiality.

C.4.2  Transitivity
Product Composition
sat(&Sup3(P)(Csdo3(i), Csdo3(j)),COI) Ÿ sat(&Sup3(P)(Csdo3(j), Csdo3(k)),COI)
If Fsup3(isup3(+)j)(i,j,obs) = Fsup3(jsup3(+)k)(j,k,obs) = Fsup3(isup3(+)k)(i,k,obs) and Fsup3(isup3(+)j)(i(A),j(A),mod) = Fsup3(jsup3(+)k)(j(A),k(A),mod) = Fsup3(isup3(+)k)(i(A),k(A),mod) then
 	ﬁ sat(&Sup3(P)(Csdo3(i), Csdo3(k)),COI)
Otherwise
 	o(ﬁ,/) sat(&Sup3(P)(Csdo3(i), Csdo3(k)),COI)

Cascade Composition
sat(&Sup3(C)(Csdo3(i), Csdo3(j)),COI) Ÿ sat(&Sup3(C)(Csdo3(j), Csdo3(k)),COI)
As with product composition, if Fsup3(isup3(+)j)(i,j,obs) = Fsup3(jsup3(+)k)(j,k,obs) = Fsup3(isup3(+)k)(i,k,obs) and
Fsup3(isup3(+)j)(i(A),j(A),mod) = Fsup3(jsup3(+)k)(j(A),k(A),mod) = Fsup3(isup3(+)k)(i(A),k(A),mod) then
	ﬁ sat(&Sup3(C)(Csdo3(i), Csdo3(k)),COI)
Otherwise
	o(ﬁ,/) sat(&Sup3(C)(Csdo3(i), Csdo3(k)),COI)

Feedback Composition
sat(&Sup3(F)(Csdo3(i), Csdo3(j)),COI) Ÿ sat(&Sup3(F)(Csdo3(j), Csdo3(k)),COI)
As with product composition, if Fsup3(isup3(+)j)(i,j,obs) = Fsup3(jsup3(+)k)(j,k,obs) = Fsup3(isup3(+)k)(i,k,obs) and
Fsup3(isup3(+)j)(i(A),j(A),mod) = Fsup3(jsup3(+)k)(j(A),k(A),mod) = Fsup3(isup3(+)k)(i(A),k(A),mod) then
	ﬁ sat(&Sup3(C)(Csdo3(i), Csdo3(k)),COI)
Otherwise
	o(ﬁ,/) sat(&Sup3(C)(Csdo3(i), Csdo3(k)),COI)

The (in)transitivity of pessimistic confidentiality immediately follows, as the (obs, mod) dual of the transitivity of pessimistic integrity.

C.4.3  Symmetry 
Product Composition
	sat(&Sup3(P)(Csdo3(i), Csdo3(j)),COC) 
As with symmetry of previous properties, 
	ﬁ sat(&Sup3(P)(Csdo3(j), Csdo3(i)),COC)

Cascade Composition
	sat(&Sup3(C)(Csdo3(i), Csdo3(j)),COC) 
Let the connections (outsup3(i) Æ insup3(j)) be replaced by (outsup3(i) Æ environs) and at least one occurrence of (outsup3(j) Æ environs) be replaced by (outsup3(j) Æ insup3(i)).  By definition, the output events produced by component j are defined as Fsup3(isup3(+)j)(j(A,out)). 
If Fsup3(isup3(+)j)(j(A,out)) Ã { Fsup3(isup3(+)j)(i,j,obs)  Fsup3(isup3(+)j)(i(A),j(A),mod) } then 
	ﬁ sat(&Sup3(C)(Csdo3(j), Csdo3(i)),COC)
Otherwise
	o(ﬁ,/) sat(&Sup3(C)(Csdo3(j), Csdo3(i)),COC)

The (a)symmetry of pessimistic integrity immediately follows, as the (obs,mod) dual of the symmetry of pessimistic confidentiality.

C.4.4  Closure
sat(Csdo3(i), COI) Ÿ sat(Csdo3(j), COI)
	= "x : N ◊ "i : {i} ◊ $ A : Fma{Fsup3(i)(obs)  Fsup3(i)(mod)} ◊  
	   $ B : Fma{Fsup3(i)(obs)  Fsup3(i)(i(A),mod)} ◊   
	   A,B Œ Fma{Fsup3(i)(iobs)  Fsup3(i)(i(A),mod)} Ÿ s(N;i)(in)SDO3(x) A Ÿ s(E;i)(in) SDO3(x) B  
	 Ÿ "x : N ◊ "j : {j} ◊ $ C : Fma{Fsup3(j)(obs)  Fsup3(j)(mod)} ◊  
	   $ D : Fma{Fsup3(j)(obs)  Fsup3(j)(j(A),mod)} ◊   
	   C,D Œ Fma{Fsup3(j)(j,obs)  Fsup3(j)(j(A),mod)} Ÿ s(N;i)(in)SDO3(x) C Ÿ s(E;i)(in) SDO3(x) D 

Product Composition
	sat(Csdo3(i), COI) Ÿ sat(Csdo3(j), COI)
If Fsup3(i)(i,obs) = Fsup3(j)(j,obs) and Fsup3(i)(i(A),mod) = Fsup3(j)(j(A),mod) then
	ﬁ sat(&Sup3(P)(Csdo3(i), Csdo3(j)), COI)
Otherwise
	o(ﬁ,/) sat(&Sup3(P)(Csdo3(i), Csdo3(j)), COI)

Cascade Composition
	sat(Csdo3(i), COI) Ÿ sat(Csdo3(j), COI)
If Fsup3(i)(i,obs) = Fsup3(j)(j,obs) and Fsup3(i)(i(A),mod) = Fsup3(j)(j(A),mod) and Fsup3(isup3(+)j)(j(A,out)) Ã {Fsup3(isup3(+)j)(i,j,obs)  Fsup3(isup3(+)j)(i(A),j(A),mod) } then
	ﬁ sat(&Sup3(C)(Csdo3(i), Csdo3(j)), COI)
Otherwise
	o(ﬁ,/) sat(&Sup3(C)(Csdo3(i), Csdo3(j)), COI)

Feedback Composition
	sat(Csdo3(i), COI) Ÿ sat(Csdo3(j), COI)
If Fsup3(i)(i,obs) = Fsup3(j)(j,obs) and Fsup3(i)(i(A),mod) = Fsup3(j)(j(A),mod) and Fsup3(isup3(+)j)(i(A,out)) Ã {Fsup3(isup3(+)j)(i,j,obs)  Fsup3(isup3(+)j)(i(A),j(A),mod) } and Fsup3(isup3(+)j)(j(A,out)) Ã { Fsup3(isup3(+)j)(i,j,obs)  Fsup3(isup3(+)j)(i(A),j(A),mod) } then
	ﬁ sat(&Sup3(F)(Csdo3(i), Csdo3(j)), COI)
Otherwise
	o(ﬁ,/) sat(&Sup3(F)(Csdo3(i), Csdo3(j)), COI)

The closure properties environment optimistic confidentiality immediately follows, as the (obs, mod) dual of the closure properties of environment optimistic integrity.

C.5  Strongly Optimistic Confidentiality and Integrity

SOC ∫ "x : N ◊ "i : N ◊ $ A,B : Fma{F(obs)  F(mod)} ◊ 
	$ A,B Œ Fma{F(i(A),obs)  F(mod)} Ÿ s(N;i)(in)SDO3(x) A Ÿ s(E;i)(in) SDO3(x) B
SOI ∫ "x : N ◊ "i : N ◊ $ A,B : Fma{F(obs)  F(mod)} ◊ 
	$ A,B Œ Fma{F(obs)  F(i(A),mod)} Ÿ s(N;i)(in)SDO3(x) A Ÿ s(E;i)(in) SDO3(x) B

C.5.1  Reflexivity 
	sat(Csdo3(i), SOC)
 By the irreflexivity of weakly environment optimistic confidentiality and weakly component optimistic confidentiality.
	o(ﬁ,/)  sat(Csdo3(R,i), COC)

The irreflexivity of strongly optimistic integrity immediately follows, as the (obs, mod) dual of the reflexivity of strongly optimistic confidentiality.

C.5.2  Transitivity
Product Composition
sat(&Sup3(P)(Csdo3(i), Csdo3(j)),SOI) Ÿ sat(&Sup3(P)(Csdo3(j), Csdo3(k)),SOI)
If Fsup3(isup3(+)j)(i,j,obs) = Fsup3(jsup3(+)k)(j,k,obs) = Fsup3(isup3(+)k)(i,k,obs) and Fsup3(isup3(+)j)(i(A),j(A),mod) = Fsup3(jsup3(+)k)(j(A),k(A),mod) = Fsup3(isup3(+)k)(i(A),k(A),mod) then
	ﬁ sat(&Sup3(P)(Csdo3(i), Csdo3(k)),SOI)
Otherwise
 	o(ﬁ,/) sat(&Sup3(P)(Csdo3(i), Csdo3(k)),SOI)

Cascade Composition
sat(&Sup3(C)(Csdo3(i), Csdo3(j)),SOI) Ÿ sat(&Sup3(C)(Csdo3(j), Csdo3(k)),SOI)
As with product composition, if Fsup3(isup3(+)j)(i,j,obs) = Fsup3(jsup3(+)k)(j,k,obs) = Fsup3(isup3(+)k)(i,k,obs) and
Fsup3(isup3(+)j)(i(A),j(A),mod) = Fsup3(jsup3(+)k)(j(A),k(A),mod) = Fsup3(isup3(+)k)(i(A),k(A),mod) then
	ﬁ sat(&Sup3(C)(Csdo3(i), Csdo3(k)),SOI)
Otherwise
	o(ﬁ,/) sat(&Sup3(C)(Csdo3(i), Csdo3(k)),SOI)

Feedback Composition
sat(&Sup3(F)(Csdo3(i), Csdo3(j)),SOI) Ÿ sat(&Sup3(F)(Csdo3(j), Csdo3(k)),SOI)
As with product composition, if Fsup3(isup3(+)j)(i,j,obs) = Fsup3(jsup3(+)k)(j,k,obs) = Fsup3(isup3(+)k)(i,k,obs) and
Fsup3(isup3(+)j)(i(A),j(A),mod) = Fsup3(jsup3(+)k)(j(A),k(A),mod) = Fsup3(isup3(+)k)(i(A),k(A),mod) then
	ﬁ sat(&Sup3(C)(Csdo3(i), Csdo3(k)),SOI)
Otherwise
	o(ﬁ,/) sat(&Sup3(C)(Csdo3(i), Csdo3(k)),S)I)

The (in)transitivity of pessimistic confidentiality immediately follows, as the (obs, mod) dual of the transitivity of pessimistic integrity.

C.5.3  Symmetry 
Product Composition
	sat(&Sup3(P)(Csdo3(i), Csdo3(j)),SOC) 
	ﬁ sat(&Sup3(P)(Csdo3(j), Csdo3(i)),SOC)

Cascade Composition
	sat(&Sup3(C)(Csdo3(i), Csdo3(j)),sOC) 
Let the connections (outsup3(i) Æ insup3(j)) be replaced by (outsup3(i) Æ environs) and at least one occurrence of (outsup3(j) Æ environs) be replaced by (outsup3(j) Æ insup3(i)). 	If Fsup3(isup3(+)j)(j(A)) Ã { Fsup3(isup3(+)j)(i,j,obs)  Fsup3(isup3(+)j)(i(A),j(A),mod) } then 
	ﬁ sat(&Sup3(C)(Csdo3(j), Csdo3(i)),SOC)
Otherwise
	o(ﬁ,/) sat(&Sup3(C)(Csdo3(j), Csdo3(i)),SOC)

The (a)symmetry of pessimistic integrity immediately follows, as the (obs,mod) dual of the symmetry of pessimistic confidentiality.

C.5.4  Closure
sat(Csdo3(i), COI) Ÿ sat(Csdo3(j), COI)
	= "x : N ◊ "i : {i} ◊ $ A, B : Fma{Fsup3(i)(obs)  Fsup3(i)(mod)} ◊  
	   A,B Œ Fma{Fsup3(i)(iobs)  Fsup3(i)(i(A),,mod)} Ÿ s(N;i)(in)SDO3(x) A Ÿ s(E;i)(in) SDO3(x) B  
	 Ÿ "x : N ◊ "j : {j} ◊ $ C,D : Fma{Fsup3(j)(obs)  Fsup3(j)(mod)} ◊  
	   C,D Œ Fma{Fsup3(j)(j,obs)  Fsup3(j)(j(A),mod)} Ÿ s(N;i)(in)SDO3(x) C Ÿ s(E;i)(in) SDO3(x) D 

Product Composition
	sat(Csdo3(i), SOI) Ÿ sat(Csdo3(j), SOI)
If Fsup3(i)(i,obs) = Fsup3(j)(j,obs) and Fsup3(i)(i(A),mod) = Fsup3(j)(j(A),mod) then
	ﬁ sat(&Sup3(P)(Csdo3(i), Csdo3(j)), SOI)
Otherwise
	o(ﬁ,/) sat(&Sup3(P)(Csdo3(i), Csdo3(j)), SOI)

Cascade Composition
	sat(Csdo3(i), SOI) Ÿ sat(Csdo3(j), SOI)
If Fsup3(i)(i,obs) = Fsup3(j)(j,obs) and Fsup3(i)(i(A),mod) = Fsup3(j)(j(A),mod) and Fsup3(isup3(+)j)(j(A,out)) Ã {Fsup3(isup3(+)j)(i,j,obs)  Fsup3(isup3(+)j)(i(A),j(A),mod) } then
	ﬁ sat(&Sup3(C)(Csdo3(i), Csdo3(j)), SOI)
Otherwise
	o(ﬁ,/) sat(&Sup3(C)(Csdo3(i), Csdo3(j)), SOI)

Feedback Composition
	sat(Csdo3(i), SOI) Ÿ sat(Csdo3(j), SOI)
If Fsup3(i)(i,obs) = Fsup3(j)(j,obs) and Fsup3(i)(i(A),mod) = Fsup3(j)(j(A),mod) and Fsup3(isup3(+)j)(i(A,out)) Ã {Fsup3(isup3(+)j)(i,j,obs)  Fsup3(isup3(+)j)(i(A),j(A),mod) } and Fsup3(isup3(+)j)(j(A,out)) Ã {Fsup3(isup3(+)j)(i,j,obs)  Fsup3(isup3(+)j)(i(A),j(A),mod) } then
	ﬁ sat(&Sup3(F)(Csdo3(i), Csdo3(j)), SOI)
Otherwise
	o(ﬁ,/) sat(&Sup3(F)(Csdo3(i), Csdo3(j)), SOI)

The closure properties environment optimistic confidentiality immediately follows, as the (obs, mod) dual of the closure properties of environment optimistic integrity.

Appendix D: Proofs of Progress Meta-Properties

In this appendix we include the details of the proofs of the meta-properties of the basic progress properties.  In cases where the proof is straightforward or essentially the same as another proof, we omit the details of the proof, indicating only the major steps of the proof.  

D.1  Accessibility

AC ∫ "x : N ◊ "i : N ◊ "a : F ◊ s{i}(in)SDO3(x)a  ﬁ s{i}SDO3(x)™a

D.1.1  Reflexivity
The behaviour of the component without self-feedback satisfies accessibility.	
	sat(Csdo3(i), AC) 
	= "x : N ◊ "i : N ◊ "a : F ◊ (s{i}(in)SDO3(x)a  ﬁ s{i}SDO3(x)™a)
Assume that all inputs are received from the environment.
	= "x : N ◊ "i : N ◊ "a : F ◊ (s(E;i)(in)SDO3(x)a  ﬁ s{i}SDO3(x)™a)
Assume that component i has one input channel.  Let the connection (environs Æ insup3(i))  be replaced by (outsup3(i)  Æ insup3(i)).
	= "x : N ◊ "a : F ◊ (s(i;i)(in)SDO3(x)a  ﬁ s{i}SDO3(x)™a)
This implies that the component will continue to satisfy accessbility if the inputs are received from the component via self-feedback.  This is based on the assumption that any input received from the environment will be accepted, regardless of the state of the component.  Therefore since the state of the component does not affect the accessibility of the component, it does not matter that possible environment events may become not possible on self-feedback.  
If the accessibility of the component is dependent on the state of the component, and therefore also on particular inputs and sequences of inputs possible from the environment, we must ensure that these events remain possible when the component has self-feedback.  If the connection of the component with self-feedback does not remove all possible environment input channels, then the environment will continue to be able to ensure accessibility at the component.  If all environment connections are removed then we must ensure that the output of the component will be able to act in a manner similar to the environment to ensure accessibility.
	@ sat(Cs(R,i), AC) 

Assume that component i has more than one input channel.  Let at least one connection (environs Æ insup3(i))  be replaced by (outsup3(i)  Æ insup3(i)).
	= "x : N ◊ F ◊ (s(i;i)(in)SDO3(x)a Ÿ s(E;i)(in)SDO3(x)a  ﬁ s{i}SDO3(x)™a)
	@ sat(Cs(R,i), AC) 
Assume that inputs may be received from the environment or from interconnected components.
	= "x : N ◊ "i : N ◊ "a : F ◊ (s(Nsup3(+)E;i)(in)SDO3(x)a  ﬁ s{i}SDO3(x)™a)
	@ sat(Cs(R,i), AC) 

D.1.2  Transitivity
Product Composition
	sat(&sup3(P)(Csdo3(i),Csdo3(j)), AC) Ÿ sat(&sup3(P)(Csdo3(j),Csdo3(k)), AC)
	= "x : N ◊ "a : F ◊ 
	   (s(E;i)(in)SDO3(x)a  ﬁ s{i}SDO3(x)™a) Ÿ (s(E;j)(in)SDO3(x)a  ﬁ s{j}SDO3(x)™a)
	   Ÿ (s(E;j)(in)SDO3(x)a  ﬁ s{i}SDO3(x)™a) Ÿ (s(E;k)(in)SDO3(x)a  ﬁ s{j}SDO3(x)™a)
If all behaviours are state-independent, then there are no inputs required to ensure accessibility by returning component to an accessible-state.  Thus the transitivity of accessibility follows. 
 	= sat(&sup3(P)(Csdo3(i),Csdo3(k)), AC)
If there are state-dependent behaviours, then there are possible inputs for which the component cannot satisfy accessibility unless a related input is received to restore the state of the component to an accessible-state.  Thus we must ensure that all such access-restoring inputs are still possible from the environment of the composition of i and k.
	@  sat(&sup3(P)(Csdo3(i),Csdo3(k)), AC)

Cascade Composition
	sat(&sup3(C)(Csdo3(i),Csdo3(j)), AC) Ÿ sat(&sup3(C)(Csdo3(j),Csdo3(k)), AC)
	= "x : N ◊ "a : F ◊ 
	   (s(E;i)(in)SDO3(x)a  ﬁ s{i}SDO3(x)™a) Ÿ (s(isup3(+)E;j)(in)SDO3(x)a  ﬁ s{j}SDO3(x)™a)
	   Ÿ (s(E;j)(in)SDO3(x)a  ﬁ s{i}SDO3(x)™a) Ÿ (s(jsup3(+)E;k)(in)SDO3(x)a ﬁ s{j}SDO3(x)™a)
Let all occurrences of (outsup3(i) Æ insup3(j)) be replaced by (outsup3(i) Æ insup3(k)), and (outsup3(j) Æ insup3(k))  be replaced by (outsup3(j) Æ environs).  	
	= "x : N ◊ "a : F ◊ 
	   (s(E;i)(in)SDO3(x)a  ﬁ s{i}SDO3(x)™a) Ÿ (s(E;j)(in)SDO3(x)a  ﬁ s{j}SDO3(x)™a)
	   Ÿ (s(E;j)(in)SDO3(x)a  ﬁ s{i}SDO3(x)™a) Ÿ (s(isup3(+)E;k)(in)SDO3(x)a ﬁ s{j}SDO3(x)™a)
If all behaviours are state-independent, then there are no inputs required from component j to ensure accessibility of component k.  Thus the transitivity of accessibility follows. 
	= "x : N ◊ "a : F ◊ 
	   (s(E;i)(in)SDO3(x)a  ﬁ s{i}SDO3(x)™a) Ÿ (s(isup3(+)E;k)(in)SDO3(x)a ﬁ s{j}SDO3(x)™a)
	ﬁ sat(&sup3(C)(Csdo3(i),Csdo3(k)), AC)
If there are state-dependent behaviours at component k and the required inputs are received from component j, then we must ensure that all such access-restoring inputs are still possible from the environment of the composition of i and k or as outputs from component i.
	@  sat(&sup3(C)(Csdo3(i),Csdo3(k)), AC)

Feedback Composition
	sat(&sup3(F)(Csdo3(i),Csdo3(j)), AC) Ÿ sat(&sup3(F)(Csdo3(j),Csdo3(k)), AC)
	= "x : N ◊ "a : F ◊ 
	   (s(jsup3(+)E;i)(in)SDO3(x)a  ﬁ s{i}SDO3(x)™a) Ÿ (s(isup3(+)E;j)(in)SDO3(x)a  ﬁ s{j}SDO3(x)™a)
	   Ÿ (s(ksup3(+)E;j)(in)SDO3(x)a  ﬁ s{i}SDO3(x)™a) 
	   Ÿ (s(jsup3(+)E;k)(in)SDO3(x)a  ﬁ s{j}SDO3(x)™a)
Let all occurrences of (outsup3(i) Æ insup3(j)) be replaced by (outsup3(i) Æ insup3(k)), (outsup3(j) Æ insup3(k)) be replaced by (outsup3(j) Æ environs), and (outsup3(k) Æ insup3(j)) be replaced by (outsup3(k) Æ insup3(i)), and (outsup3(j) Æ insup3(i)) be replaced by (outsup3(j) Æ environs).	
	= "x : N ◊ "a : F ◊ 
	   (s(ksup3(+)E;i)(in)SDO3(x)a  ﬁ s{i}SDO3(x)™a) Ÿ (s(E;j)(in)SDO3(x)a  ﬁ s{j}SDO3(x)™a)
	   Ÿ (s(E;j)(in)SDO3(x)a  ﬁ s{i}SDO3(x)™a) Ÿ (s(isup3(+)E;k)(in)SDO3(x)a ﬁ s{j}SDO3(x)™a)
If all behaviours are state-independent, then there are no inputs required from component j to ensure accessibility of component i or k.  Thus the transitivity of accessibility follows. 
	= "x : N ◊ "a : F ◊ 
	   (s(ksup3(+)E;i)(in)SDO3(x)a  ﬁ s{i}SDO3(x)™a) Ÿ (s(isup3(+)E;k)(in)SDO3(x)a ﬁ s{j}SDO3(x)™a)
	=  sat(&sup3(F)(Csdo3(i),Csdo3(k)), AC)
If there are state-dependent behaviours at component i or k and the required inputs are received from component j, then we must ensure that all such access-restoring inputs are still possible from the environment of the composition of i and k or as outputs from component k or i.
	@  sat(&sup3(F)(Csdo3(i),Csdo3(k)), AC)

D.1.3  Symmetry
Product Composition
	sat(&sup3(P)(Csdo3(i),Csdo3(j)), AC)
	= "x : N ◊ "a : F ◊ 
	   (s(E;i)(in)SDO3(x)a  ﬁ s{i}SDO3(x)™a) Ÿ (s(E;j)(in)SDO3(x)a  ﬁ s{j}SDO3(x)™a)
	= sat(&sup3(P)(Csdo3(j),Csdo3(i)), AC)

Cascade Composition
	sat(&sup3(C)(Csdo3(i),Csdo3(j)), AC)
	= "x : N ◊ "a : F ◊ 
	   (s(E;i)(in)SDO3(x)a  ﬁ s{i}SDO3(x)™a) Ÿ (s(isup3(+)E;j)(in)SDO3(x)a  ﬁ s{j}SDO3(x)™a)
Let all occurrences of (outsup3(i) Æ insup3(j)) be replaced by (outsup3(i) Æ environs), and at least one occurrence of (outsup3(j) Æ environs) be replaced by (outsup3(j) Æ insup3(i)).  	
	= "x : N ◊ ""a : F ◊ 
	   (s(jsup3(+)E;i)(in)SDO3(x)a  ﬁ s{i}SDO3(x)™a) Ÿ (s(E;j)(in)SDO3(x)a  ﬁ s{j}SDO3(x)™a)
If all behaviours are state-independent, then there are no inputs required from component i or the environment to ensure accessibility of component j, or from the environment to ensure the accessibility of component i.  Thus the transitivity of accessibility follows. 
	ﬁ sat(&sup3(C)(Csdo3(j),Csdo3(i)), AC)
If there are state-dependent behaviours at component j and the required inputs are received from component i, then we must ensure that all such access-restoring inputs are still possible from the environment of the composition of i and j.  We must also ensure that any access-restoring inputs required by component i still be possible inputs, either from the environment or from component j.
	@  sat(&sup3(C)(Csdo3(j),Csdo3(i)), AC)

D.1.4  Closure
	sat(Csdo3(i), AC) Ÿ sat(Csdo3(j), AC)
	= {"x : N ◊ "i : N ◊ "a : F ◊ (s{i}(in)SDO3(x)a ﬁ s{i}SDO3(x)™a) }
	   Ÿ {"x : N ◊ "j : {j} ◊ "a : F ◊ (s{j}(in)SDO3(x)a ﬁ s{j}SDO3(x)™a) }
	= "x : N ◊ "i : N ◊ "a : F ◊ 
	   (s{i}(in)SDO3(x)a  ﬁ s{i}SDO3(x)™a) Ÿ (s{j}(in)SDO3(x)a ﬁ s{j}SDO3(x)™a) 

Product Composition
As long as any access-restoring events from the environment remain possible in the composite environment, then closure follows.
	= sat(&sup3(P)(Csdo3(i),Csdo3(j)), AC)

Cascade Composition
Let at least one occurrence of (outsup3(i) Æ environs) be replaced by (outsup3(i) Æ insup3(j)).
	= "x : N ◊ "a : F ◊ 
	   (s(E;i)(in)SDO3(x)a  ﬁ s{i}SDO3(x)™a) Ÿ (s(isup3(+)E;j)(in)SDO3(x)a ﬁ s{j}SDO3(x)™a)
If all behaviours are state-independent, then there are no inputs required from the environment to ensure accessibility of component i or j.  Thus the closure of accessibility follows. 
	=  sat(&sup3(C)(Csdo3(i),Csdo3(j)), AC)
If there are state-dependent behaviours at component j and the required inputs are received from the environment, then we must ensure that all such access-restoring inputs are still possible from the environment of the composition of i and j or from component i.  We must also ensure that any access-restoring inputs required by component i still be possible inputs, within the composite environment.
	@  sat(&sup3(C)(Csdo3(j),Csdo3(i)), AC)

Feedback Composition
Let at least one occurrence of (outsup3(i) Æ environs) be replaced by (outsup3(i) Æ insup3(j)) and (outsup3(j) Æ environs) be replaced by (outsup3(j) Æ insup3(i)).
	= "x : N ◊ "a : F ◊ 
	   (s(jsup3(+)E;i)(in)SDO3(x)a  ﬁ s{i}SDO3(x)™a) Ÿ (s(isup3(+)E;j)(in)SDO3(x)a ﬁ s{j}SDO3(x)™a)
If all behaviours are state-independent, then there are no inputs required from the environment to ensure accessibility of component i or j.  Thus the closure of accessibility follows. 
	= sat(&sup3(F)(Csdo3(i),Csdo3(j)), AC)
If there are state-dependent behaviours at either component, and the required inputs are received from the environment, then we must ensure that all such access-restoring inputs are still possible from the environment of the composition of i and j or from the interconnected component.  
	@  sat(&sup3(F)(Csdo3(i),Csdo3(j)), AC)

Those behaviours that do not rely on a certain ordering of input events to satisfy accessibility at a component exhibit reflexivity, transitivity, symmetry and closure and will continue to satisfy accessibility on composition with product, cascade and feedback structures.
Those behaviours that do rely on a given order of input events may or may not exhibit reflexivity, transitivity, symmetry and closure.  This will depend on the composite structure and the specific details and dependencies of the component in question. 

D.2  Termination

TR ∫ "x : N ◊ "i : N ◊ "a : F ◊ s{i}SDO3(x)a ﬁ s{i}SDO3(x)™ÿa 

D.2.1  Reflexivity
	sat(Csdo3(i), AC) 
	= "x : N ◊ "i : N ◊ "a : F ◊ (s{i}SDO3(x)a ﬁ s{i}SDO3(x)™ÿa)
Let at least one connection (environs Æ insup3(i)) be replaced by (outsup3(i)  Æ insup3(i)).
	= "x : N ◊ "i : N ◊ "a : F ◊ (s{i}SDO3(x)a ﬁ s{i}SDO3(x)™ÿa)
Every process that is "self-terminating," that is, does not require a certain input to be received in order to terminate, will continue to self-terminate under a self-feedback connection. 
	= sat(Cs(R,i), AC) 
If termination requires a terminating-input, then we cannot guarantee that such an input will be available under self-feedback: termination will depend on required input being sent by another component or environment and will depend on component's ability to receive event (accessibility).
	@ sat(Cs(R,i), AC) 

D.2.2  Transitivity
Product Composition
	sat(&sup3(P)(Csdo3(i),Csdo3(j)), AC) Ÿ sat(&sup3(P)(Csdo3(j),Csdo3(k)), AC)
	= "x : N ◊ "a : F ◊ 
	   (s{i}SDO3(x)a ﬁ s{i}SDO3(x)™ÿa) Ÿ (s{j}SDO3(x)a  ﬁ s{j}SDO3(x)™ÿa)
	    Ÿ (s{j}SDO3(x)a ﬁ s{j}SDO3(x)™ÿa) Ÿ (s{k}SDO3(x)a  ﬁ s{k}SDO3(x)™ÿa)
	ﬁ "x : N ◊ "i : {i,k} ◊ "a : F ◊ 
	   (s{i}SDO3(x)a ﬁ s{i}SDO3(x)™ÿa) Ÿ (s{k}SDO3(x)a  ﬁ s{k}SDO3(x)™ÿa)
If every process is "self-terminating," then termination will exhibit transitivity.  If there are non-self-terminating processes that rely on events that are possible from the composite environment of components i and k, then termination will exhibit transitivity.  
	= sat(&sup3(P)(Csdo3(i),Csdo3(k)), AC) 
If termination requires a terminating-input that may not be possible from the composite environment, then we cannot guarantee that such an input will be available under self-feedback.
	@ sat(&sup3(P)(Csdo3(i),Csdo3(k)), AC)

Cascade Composition
	sat(&sup3(C)(Csdo3(i),Csdo3(j)), AC) Ÿ sat(&sup3(C)(Csdo3(j),Csdo3(k)), AC)
As with product composition, if processes continue to terminate, 
	= sat(&sup3(C)(Csdo3(i),Csdo3(k)), AC) 
If termination requires a terminating-input, then we cannot guarantee that such an input will be available under the cascade composition of components i and k.
	@ sat(&sup3(C)(Csdo3(i),Csdo3(k)), AC)

Feedback Composition
	sat(&sup3(F)(Csdo3(i),Csdo3(j)), AC) Ÿ sat(&sup3(F)(Csdo3(j),Csdo3(k)), AC)
As with product composition, if processes continue to terminate, 
	= sat(&sup3(F)(Csdo3(i),Csdo3(k)), AC) 
If termination requires a terminating-input, then we cannot guarantee that such an input will be available under the cascade composition of components i and k.
	@ sat(&sup3(F)(Csdo3(i),Csdo3(k)), AC)

D.2.3  Symmetry
Product Composition
	sat(&sup3(P)(Csdo3(i),Csdo3(j)), AC)
As with accessibility
	= "x : N ◊ "a : F ◊ (s{i}SDO3(x)a  ﬁ s{i}SDO3(x)™ÿa)) Ÿ (s{j}SDO3(x)a  ﬁ s{j}SDO3(x)™ÿa)
	= sat(&sup3(P)(Csdo3(j),Csdo3(i)), AC)

Cascade Composition
	sat(&sup3(C)(Csdo3(i),Csdo3(j)), AC)
If every process is "self-terminating," then termination will exhibit transitivity.  If there are non-self-terminating processes that rely on events that are possible from the composite environment of components i and j, then termination will exhibit transitivity.  
	= sat(&sup3(C)(Csdo3(i),Csdo3(j)), AC) 
If termination requires a terminating-input that may not be possible from the component's meta-environment, then we cannot guarantee that such an input will be available under the symmetric cascade composition.
	@ sat(&sup3(C)(Csdo3(j),Csdo3(i)), AC)

D.2.4  Closure
	sat(Csdo3(i), AC) Ÿ sat(Csdo3(j), AC)
	= "x : N ◊ "i : N ◊ "a : F ◊ 
	   (s{i}SDO3(x)a  ﬁ s{i}SDO3(x)™ÿa) Ÿ (s{j}SDO3(x)a  ﬁ s{j}SDO3(x)™ÿa) 

Product Composition
If all processes are self-terminating, or all terminating-inputs are possible from composite environment, then product composition is closed.
	= sat(&sup3(P)(Csdo3(i),Csdo3(j)), AC)
Otherwise, 
	@ sat(&sup3(P)(Csdo3(i),Csdo3(j)), AC)

Cascade Composition
If all processes are self-terminating, or all terminating-inputs remain possible events in component'e meta-environment, the cascade composition is closed.
	= sat(&sup3(C)(Csdo3(i),Csdo3(j)), AC)
Otherwise, 
	@ sat(&sup3(C)(Csdo3(i),Csdo3(j)), AC)

Feedback Composition
If all processes are self-terminating, or all terminating-inputs remain posisble events in component's meta-environment, then feedback composition is closed.
	= sat(&sup3(F)(Csdo3(i),Csdo3(j)), AC)
Otherwise, 
	@ sat(&sup3(F)(Csdo3(i),Csdo3(j)), AC)

D.3  Eventual Progress

EP ∫ "x : N ◊ "i : N ◊ "a : F ◊ $c : F ◊ s{i}SDO3(x)™a ﬁ s{i}SDO3(x)™c  

D.3.1  Reflexivity
	sat(Csdo3(i), AC) 
	= "x : N ◊ "i : N ◊ "a : F ◊ $c : F ◊ (s{i}SDO3(x)™a ﬁ s{i}SDO3(x)™c)
Let at least one occurrence of (environs Æ insup3(i)) be replaced by (outsup3(i)  Æ insup3(i)).
	= "x : N ◊ "a : F ◊ $c : F ◊ (s{i}SDO3(x)™a ﬁ s{i}SDO3(x)™c)
As with termination, the reflexivity of eventual progress depends on the possible inputs that remain possible or are rendered impossible by the reflexive connection.  If an input is possible, then eventual progress will be satisfied as long as all possible inputs remain possible.  This requirement ensures that all processes will terminate, allowing eventual progress.  If the reflexive composition is such that no inputs to the component are possible, then it is academic whether eventual progress is satisfied as it has no opportunity to be satisfied.  
	= sat(Cs(R,i), AC) 

D.3.2  Transitivity
Transitivity of eventual progress for product, cascade, and feedback composite system follows using the same arguments as with termination.

Product Composition
	sat(&sup3(P)(Csdo3(i),Csdo3(j)), AC) Ÿ sat(&sup3(P)(Csdo3(j),Csdo3(k)), AC)
	@ sat(&sup3(P)(Csdo3(i),Csdo3(k)), AC)

Cascade Composition
	sat(&sup3(C)(Csdo3(i),Csdo3(j)), AC) Ÿ sat(&sup3(C)(Csdo3(j),Csdo3(k)), AC)
	@  sat(&sup3(C)(Csdo3(i),Csdo3(k)), AC)

Feedback Composition
	sat(&sup3(F)(Csdo3(i),Csdo3(j)), AC) Ÿ sat(&sup3(F)(Csdo3(j),Csdo3(k)), AC)
	@  sat(&sup3(F)(Csdo3(i),Csdo3(k)), AC)

D.3.3  Symmetry
Symmetry of product, cascade, and feedback compositions follows as with termination.

Product Composition
	sat(&sup3(P)(Csdo3(i),Csdo3(j)), AC)
	= sat(&sup3(P)(Csdo3(j),Csdo3(i)), AC)

Cascade Composition
	sat(&sup3(C)(Csdo3(i),Csdo3(j)), AC)
	@  sat(&sup3(C)(Csdo3(j),Csdo3(i)), AC)

D.3.4  Closure
	sat(Csdo3(i), AC) Ÿ sat(Csdo3(j), AC)
	= "x : N ◊ "a : F ◊ $c : F ◊
	   (s{i}SDO3(x)™a ﬁ s{i}SDO3(x)™c) Ÿ (s{j}SDO3(x)™a   ﬁ s{j}SDO3(x)™c) 
Closure of eventual progress follows as with termination.

Product Composition
	@ sat(&sup3(P)(Csdo3(i),Csdo3(j)), AC)

Cascade Composition
	@ sat(&sup3(C)(Csdo3(i),Csdo3(j)), AC)

Feedback Composition
	@ sat(&sup3(F)(Csdo3(i),Csdo3(j)), AC)

D.4  Eventual Output

EO ∫ "x : N ◊ "i : N ◊ "a : F ◊ $b : F ◊ s{i}SDO3(x)a ﬁ s{i}(out)SDO3(x)™b 

D.4.1  Reflexivity
	sat(Csdo3(i), AC) 
	= "x : N ◊ "i : {i,j} ◊ "a : F ◊ $b : F ◊ s{i}SDO3(x)a ﬁ s{i}(out)SDO3(x)™b 
Reflexivity of eventual output follows as with termination and eventual progress.
	@ sat(Cs(R,i), AC) 

D.4.2  Transitivity
Product Composition
	sat(&sup3(P)(Csdo3(i),Csdo3(j)), AC) Ÿ sat(&sup3(P)(Csdo3(j),Csdo3(k)), AC)
	= "x : N ◊ "a : F ◊ $b : F ◊ 
	   (s{i}SDO3(x)a ﬁ s(i;E)(out)SDO3(x)™b) Ÿ (s{j}SDO3(x)a  ﬁ s(j;E)(out)SDO3(x)™b)  
	   Ÿ (s{j}SDO3(x)a ﬁ s(j;E)(out)SDO3(x)™b) Ÿ (s{k}SDO3(x)a  ﬁ s(k;E)(out)SDO3(x)™b) 
As with termination and eventual progress, if all possible inputs remain possible in composite environment, then transitivity of eventual output follows.
	ﬁ "x : N ◊ "a : F ◊ $b : F ◊ 
	   (s{i}SDO3(x)a ﬁ s(i;E)(out)SDO3(x)™b) Ÿ (s{k}SDO3(x)a  ﬁ s(k;E)(out)SDO3(x)™b) 
	ﬁ sat(&sup3(P)(Csdo3(i),Csdo3(k)), AC)
Otherwise, 
	@ sat(&sup3(P)(Csdo3(i),Csdo3(k)), AC)

Cascade Composition
	sat(&sup3(C)(Csdo3(i),Csdo3(j)), AC) Ÿ sat(&sup3(C)(Csdo3(j),Csdo3(k)), AC)
	= "x : N ◊ "a : F ◊ $b : F ◊ 
	   (s{i}SDO3(x)a ﬁ s(i;jsup3(+)E)(out)SDO3(x)™b) Ÿ (s{j}SDO3(x)a ﬁ s(j;E)(out)SDO3(x)™b)  
	   Ÿ (s{j}SDO3(x)a ﬁ s(j;ksup3(+)E)(out)SDO3(x)™b) Ÿ (s{k}SDO3(x)a ﬁ s(k;E)(out)SDO3(x)™b) 
As with termination and eventual progress,
	@ sat(&sup3(C)(Csdo3(i),Csdo3(k)), AC)

Feedback Composition
	sat(&sup3(F)(Csdo3(i),Csdo3(j)), AC) Ÿ sat(&sup3(F)(Csdo3(j),Csdo3(k)), AC)
As with termination and eventual progress,
	@ sat(&sup3(F)(Csdo3(i),Csdo3(k)), AC)

D.4.3  Symmetry
Product Composition
	sat(&sup3(P)(Csdo3(i),Csdo3(j)), AC)
As with termination and eventual progress,
	= sat(&sup3(P)(Csdo3(j),Csdo3(i)), AC)

Cascade Composition
	sat(&sup3(C)(Csdo3(i),Csdo3(j)), AC)
As with termination and eventual progress,
	@ sat(&sup3(C)(Csdo3(j),Csdo3(i)), AC)

D.4.4  Closure
	sat(Csdo3(i), AC) Ÿ sat(Csdo3(j), AC)
	= "x : N ◊ "i : {i} ◊ "j : {j} ◊ "a : F ◊ $b : F ◊ 
	   (s{i}SDO3(x)a ﬁ s{i}(out)SDO3(x)™b) Ÿ (s{j}SDO3(x)a ﬁ s{j}(out)SDO3(x)™b) 

Product Composition
As with termination and eventual progress,
	@ sat(&sup3(P)(Csdo3(i),Csdo3(j)), AC)

Cascade Composition
As with termination and eventual progress,
	@ sat(&sup3(C)(Csdo3(i),Csdo3(j)), AC)

Feedback Composition
As with termination and eventual progress,
	@ sat(&sup3(F)(Csdo3(i),Csdo3(j)), AC)

D.5  Faithfulness

FT ∫ "x:N ◊ "i:N ◊ "a:F(i(in)) ◊ $b:F(i(out)) ◊ 
	(i(a;b) Ÿ s{i}(in)SDO3(x) a) ﬁ s{i}(out)SDO3(x) ™b 

Given that i(a;b) and s{i}(in)SDO3(x) a
"x:N ◊ "i:N ◊ "a:F(i(in)) ◊ $b:F(i(out)) ◊ i(a;b) Ÿ s{i}(in)SDO3(x) a
By Accessibility
= "x:N ◊ "i:N ◊ "a:F(i(in)) ◊ $b:F(i(out)) ◊ i(a;b) Ÿ s{i}(in)SDO3(x) a ﬁ s{i}SDO3(x) ™a
By Eventual Output
= "x:N ◊ "i:N ◊ "a:F(i(in)) ◊ $b:F(i(out)) ◊ 
   i(a;b) Ÿ s{i}(in)SDO3(x) a ﬁ s{i}SDO3(x) ™a ﬁ s{i}(out)SDO3(x) ™™b
= "x:N ◊ "i:N ◊ "a:F(i(in)) ◊ $b:F(i(out)) ◊ i(a;b) Ÿ s{i}(in)SDO3(x) a ﬁ s{i}(out)SDO3(x) ™™b
= Faithfulness

By definition, faithfulness will also imply eventual progress and termination for those behaviours that are input-state independent.  If these properties are not satisfied by all possible behaviours, we cannot guarantee faithfulness because we cannot guarantee that every input a to a component i such that i(a;b) will eventually produce an output b.  Thus if accessibility, eventual output, eventual progress, and termination exhibit a given meta-property, then so will faithfulness.   

D.5.1  Reflexivity
sat(Csdo3(i), FT)
=  "x:N ◊ "i:N ◊ "a:F(i(in)) ◊ $b:F(i(out)) ◊ (i(a;b) Ÿ s{i}(in)SDO3(x) a) ﬁ s{i}(out)SDO3(x) ™b 
If AC, EO, EP and TR exhibit reflexivity
ﬁ sat(Csdo3(R,i), FT)

D.5.2  Transitivity
If AC, EO, EP and TR exhibit transitivity for a given composite structure then so will faithfulness.

D.5.3  Symmetry
If AC, EO, EP and TR exhibit symmetry for a given composite structure then so will faithfulness.

D.5.4  Closure
If AC, EO, EP and TR exhibit closure for a given composite structure then so will faithfulness.

D.6  Provenance

PV ∫ "x : N ◊ "i : N ◊ " A : Fma{F} ◊ s{i}(in)SDO3(x) ™A ﬁ s(NSUP3(+)E;i)(out)SDO3(x) A 

D.6.1  Reflexivity
	sat(Csdo3(i), PV)
	= "x : N ◊ "i : N ◊ " A : Fma{F} ◊ s{i}(in)SDO3(x) ™A ﬁ s(NSUP3(+)E;i)(out)SDO3(x) A  
If connections are correct, then reflexivity of provenance follows,
	= sat(Csdo3(R,i), PV)

D.6.2  Transitivity
If connections are correct, then transivity of provenance for product, cascade and feedback composition follows because the replacement of one known source by another known source does not violate the provenance of the events in the system. 

D.6.3  Symmetry
If connections are correct, then symmetry of provenance for product, cascade and feedback composition follows because the replacement of one known source by another known source does not violate the provenance of the events in the system. 

D.6.4  Closure
If connections are correct, then closure of provenance for product, cascade and feedback composition follows because the replacement of one known source (the environment) by another known source (a known component) does not violate the provenance of the events in the system. 

D.7  Utility

UT ∫ "x : N ◊ "i : N ◊ " A : Fma{F} ◊ s(NSUP3(+)E;i)(out)SDO3(x) A ﬁ s{i}(in)SDO3(x) ™A 

D.7.1  Reflexivity
	sat(Csdo3(i), UT)
	= "x : N ◊ "i : N ◊ " A : Fma{F} ◊ s(NSUP3(+)E;i)(out)SDO3(x) A ﬁ s{i}(in)SDO3(x) ™A  
If connections are correct, then reflexivity of utility follows,
	= sat(Csdo3(R,i), UT)

D.7.2  Transitivity
If connections are correct, then transitivity of utility for product, cascade and feedback composition follows because the replacement of one known source by another known source does not violate the utility the system. 

D.7.3  Symmetry
If connections are correct, then symmetry of utility for product, cascade and feedback composition follows because the replacement of one known source by another known source does not violate the utility of the system. 

D.7.4  Closure
If connections are correct, then closure of utility for product, cascade and feedback composition follows because the replacement of one known source by another known source does not violate the utility of the system. 

Appendix E:  Compatibility of Basic Properties

E.1  Pessimistic Confidentiality and Integrity

PC ∫ "x : N ◊ "i : N ◊ $ A : Fma{F(A,obs)  F(mod) } ◊ s(Nsup3(+)E;i)(in) SDO3(x) A
	= "x : N ◊ "i : N ◊ $ A : Fma{F(A,obs)  F(mod) } ◊ 
	   A Œ Fma{F(A,obs)  F(mod) } Ÿ s(Nsup3(+)E;i)(in) SDO3(x) A
PI ∫ "x : N ◊ "i : N ◊ $ A : Fma{F(obs)  F(A,mod) } ◊ s(Nsup3(+)E;i)(in) SDO3(x) A
	= "x : N ◊ "i : N ◊ $ B : Fma{F(obs)  F(A,mod) } ◊ 
	   B Œ Fma{F(obs)  F(A,mod) } Ÿ s(Nsup3(+)E;i)(in) SDO3(x) B

Compatible Property Domain: 
Qsdo3(PC) * Qsdo3(PI) = A,B : Fma{F(A,obs)  F(mod) )  ( F(A,mod)  F(obs) } 
	= A,B : Fma{(F(A)  F(obs)  F(mod))  ((F(A)  F(mod)  F(obs)) } 
	= A,B : Fma{ (F(A)  F(obs))  (F(A)  F(mod) ) }
	= A,B : Fma{ F(obs)  F(mod) }
If the sets of events for the system, F(obs) and F(mod) are defined such that F(obs) = F(A,obs) and F(mod) = F(A,mod) then the properties of pessimistic confidentiality and integrity will be compatible.  Otherwise, the compatible property domain is incompatible with the individual property domains.
If the compatible property domain is compatible with the individual property domains, or the individual property domains can be made compatible, then the compatibility assessment continues with the compatible property specification.

Required World:
Wsdo3(PC) Ÿ Wsdo3(PI) = (F(A,obs)  F(mod) )  ( F(A,mod)  F(obs) ) }
	= F(A,obs)  F(A,mod) 
Thus the assumptions about the events that are allowable in the composite environment must correspond the to required world.

Compatible Property Specification: 
Rsdo3(PC) Ÿ Rsdo3(PI) = s(Nsup3(+)E;i)(in) SDO3(x) A Ÿ s(Nsup3(+)E;i)(in) SDO3(x) B
	= s(Nsup3(+)E;i)(in) SDO3(x) (A Ÿ B)

Compatible Property:
PC Ÿ PI = "x : N ◊ "i : N ◊ $ A,B : Fma{F(A,obs)  F(A,mod)} ◊
	   A,B Œ Fma{F(A,obs)  F(A,mod) } Ÿ s(Nsup3(+)E;i)(in) SDO3(x) (A Ÿ B)
	= "x : N ◊ "i : N ◊ $ A : Fma{F(A,obs)  F(A,mod) } ◊
	   A Œ Fma{F(A,obs)  F(A,mod) } Ÿ s(Nsup3(+)E;i)(in) SDO3(x) A

E.2  Environment Optimistic Integrity and Pessimistic Integrity

EOI ∫ "x : N ◊ "i :  N ◊ $ A : Fma{F(i,obs)  F(i(A),mod)} ◊ 
	$ B : Fma{F(obs)  F(mod)} ◊ B Œ Fma{F(i,obs)  F(i(A),mod)} 
	Ÿ s(N;i)(in) SDO3(x) A Ÿ s(E;i)(in) SDO3(x) B
Separating into sub-properties:
	EOIsdo3(1) ∫ "x : N ◊ "i :  N ◊ $ A : Fma{F(i,obs)  F(i(A),mod)} ◊ 
		A Œ Fma{F(i,obs)  F(i(A),mod)} Ÿ s(N;i)(in) SDO3(x) A 
	EOIsdo3(2) ∫ "x : N ◊ "i :  N ◊ $ B : Fma{F(obs)  F(mod)} ◊ 
		B Œ Fma{F(i,obs)  F(i(A),mod)} Ÿ s(E;i)(in) SDO3(x) B
PI ∫ "x : N ◊ "i : N ◊ $ A : Fma{F(N,obs)  F(N(A),mod) } ◊  s(Nsup3(+)E;i)(in)SDO3(x) A
Separating into sub-properties and changing event variable names: 	
	PIsdo3(1) ∫ "x : N ◊ "i : N ◊ $ C : Fma{F(N,obs)  F(N(A),mod)} ◊ s(N;i)(in)SDO3(x) C 
	PIsdo3(2) ∫ "x : N ◊ "i : N ◊ $ D : Fma{F(N,obs)  F(N(A),mod)} ◊ s(E;i)(in)SDO3(x) D

Compatible Property Domain:
Qsdo3(EOIsdo3(1)) * Qsdo3(PI) = A,C : Fma{F(N,obs)  F(N(A),mod) } 
Qsdo3(EOIsdo3(2)) * Qsdo3(PI) = B,C : Fma{ F(N,obs)  F(N(A),mod) }

Required World: 
Wsdo3(EOIsdo3(1)) Ÿ Wsdo3(PI) = A F(N,obs)  F(N(A),mod) 
Wsdo3(EOIsdo3(2)) Ÿ Wsdo3(PI) = F(N,obs)  F(N(A),mod)  

Compatible Property Specification:
Rsdo3(EOIsdo3(1)) Ÿ Rsdo3(EOIsdo3(2)) Ÿ Rsdo3(PI) = s(N;i)(in)SDO3(x) (A Ÿ C)  Ÿ s(E;i)(in)SDO3(x) (B Ÿ D) 

Compatible Property: 
EOI Ÿ PI = "x : N ◊ "i : N ◊ $ A,B : Fma{F(N,obs)  F(N(A),mod) } ◊ 
	         Ÿ s(N;i)(in)SDO3(x) A Ÿ s(E;i)(in)SDO3(x) B 
	= PI

E.3  Component Optimistic Confidentiality and Environment Optimistic Confidentiality 

COC ∫ "x : N ◊ "i : N ◊ $ A : Fma{F(obs)  F(mod)} ◊ 
	$ B : Fma{F(i(A),obs)  F(mod)} ◊ 
	A,B Œ Fma{F(i(A),obs)  F(mod)} Ÿ s(N;i)(in)SDO3(x) A Ÿ s(E;i)(in)SDO3(x) B
Separating into sub-properties: 	
	COCsdo3(1) ∫ "x : N ◊ "i : N ◊ $ A : Fma{F(obs)  F(mod)} ◊ 
		A Œ Fma{F(i(A),obs)  F(mod)} Ÿ s(N;i)(in)SDO3(x) A 
	COCsdo3(2) ∫ "x : N ◊ "i : N ◊ $ B : Fma{F(i(A),obs)  F(mod)} ◊ 
		B Œ Fma{F(i(A),obs)  F(mod)} Ÿ s(E;i)(in)SDO3(x) B

EOC ∫ "x : N ◊ "i :  N ◊ $ A : Fma{F(i(A),obs)  F(i,mod)} ◊ 
	$ B : Fma{F(i,obs)  F(mod)} ◊ 
	BŒ Fma{F(i(A),obs)  F(i,mod)} Ÿ s(N;i)(in)SDO3(x) A Ÿ s(E;i)(in) SDO3(x) B
Separating into sub-properties:
	EOCsdo3(1) ∫ "x : N ◊ "i : N ◊ $ C : Fma{F(i(A),obs)  F(mod)} ◊ 
		C Œ Fma{F(i(A),obs)  F(mod)} Ÿ s(N;i)(in)SDO3(x) C 
	EOCsdo3(2) ∫ "x : N ◊ "i : N ◊ $ D : Fma{F(obs)  F(mod)} ◊ 
		D Œ Fma{F(i(A),obs)  F(mod)} Ÿ s(E;i)(in)SDO3(x) D

Compatible Property: 
COC Ÿ EOC = "x : N ◊ "i : N ◊ $ A,B : Fma{F(i(A),obs)  F(mod) } ◊ 
	   A,B Œ Fma{F(i(A),obs)  F(mod) } Ÿ s(N;i)(in)SDO3(x) A Ÿ s(E;i)(in)SDO3(x) B 

E.4  Component Optimistic Confidentiality and Strongly Optimistic Integrity

COC ∫ "x : N ◊ "i : N ◊ $ A : Fma{F(obs)  F(mod)} ◊ 
	$ B : Fma{F(i(A),obs)  F(mod)} ◊ 
	A,B Œ Fma{F(i(A),obs)  F(mod)} Ÿ s(N;i)(in)SDO3(x) A Ÿ s(E;i)(in)SDO3(x) B
Separating into sub-properties: 	
	COCsdo3(1) ∫ "x : N ◊ "i : N ◊ $ A : Fma{F(obs)  F(mod)} ◊ 
		A Œ Fma{F(i(A),obs)  F(mod)} Ÿ s(N;i)(in)SDO3(x) A 
	COCsdo3(2) ∫ "x : N ◊ "i : N ◊ $ B : Fma{F(i(A),obs)  F(mod)} ◊ 
		B Œ Fma{F(i(A),obs)  F(mod)} Ÿ s(E;i)(in)SDO3(x) B
SOI ∫ "x : N ◊ "i : N ◊ $ A,B : Fma{F(obs)  F(mod)} ◊ 
	$ A,B Œ Fma{F(obs)  F(i(A),mod)} Ÿ s(N;i)(in)SDO3(x) A Ÿ s(E;i)(in) SDO3(x) B
Separating into sub-properties and changing event variable names: 	
	SOIsdo3(1) ∫ "x : N ◊ "i : N ◊ $ C : Fma{F(obs)  F(mod)} ◊ 
		$ C Œ Fma{F(obs)  F(i(A),mod)} Ÿ s(N;i)(in)SDO3(x) C 
	SOIsdo3(2) ∫ "x : N ◊ "i : N ◊ $ D : Fma{F(obs)  F(mod)} ◊ 
		$ D Œ Fma{F(obs)  F(i(A),mod)} Ÿ s(E;i)(in) SDO3(x) D

Compatible Property: 
COC Ÿ SOI = "x : N ◊ "i : N ◊ $ A,B : Fma{F(obs)  F(mod) } ◊ 
	A,B Œ Fma{F(i(A),obs)  F(i(A),mod) } 
	Ÿ s(N;i)(in)SDO3(x) A Ÿ s(E;i)(in)SDO3(x) B 

E.5  Authenticity and Component Optimistic Integrity

AU ∫ "x : N ◊ "i : N ◊ $ A : Fma{F(i)} ◊ s{i}(out)SDO3(x) A 
COI ∫ "x : N ◊ "i : N ◊ $ A : Fma{F(obs)  F(mod)} ◊ 
	$ B : Fma{F(i,obs)  F(i(A),mod)} ◊ 
	A Œ Fma{F(i,obs)  F(i(A),mod)} Ÿ s(N;i)(in)SDO3(x) A Ÿ s(E;i)(in) SDO3(x) B
Separating into sub-properties: 
	Qsdo3(COIsdo3(1)) = "x : N ◊ "i : N ◊ $ C : Fma{F(obs)  F(mod)} ◊ 
	   C Œ Fma{F(i,obs)  F(i(A),mod)} Ÿ s(N;i)(in)SDO3(x) C 
	Qsdo3(COIsdo3(2)) = "x : N ◊ "i : N ◊ $ B : Fma{F(i,obs)  F(mod)} ◊ 
	   B Œ Fma{F(i,obs)  F(i(A),mod)} Ÿ s(E;i)(in)SDO3(x) B 

Compatible Property: 
AU Ÿ COI = "x : N ◊ "i : N ◊ $ C : Fma{ F(i,obs)  F(i,mod) }  ◊ 
	$ A,B : Fma{F(i,obs)  F(i(A),mod) }  ◊ 
	A,B,C Œ Fma{F(i,obs)  F(i(A),mod) } 
	 Ÿ s(i;Nsup3(+)E)(out)SDO3(x) A Ÿ s(N;i)(in)SDO3(x) C Ÿ s(E;i)(in)SDO3(x) B 

E.6  Accessibility and Strongly Optimistic Confidentiality

AC ∫ "x : N ◊ "i : N ◊ "a : F ◊ s{i}(in)SDO3(x)a  ﬁ s{i}SDO3(x)™a
SOC ∫ "x : N ◊ "i : N ◊ $ A,B : Fma{F(obs)  F(mod)} ◊ 
	A,B Œ Fma{F(i(A),obs)  F(i,mod)} Ÿ s(N;i)(in)SDO3(x) A Ÿ s(E;i)(in) SDO3(x) B

Compatible Property: 
AC Ÿ SOC 
	= "x : N ◊ "i : N ◊ "a : Fma{F(obs)  F(mod) } ◊ 
	   $b,c : Fma{F(obs)  F(mod) } ◊ a,b,c Œ Fma{F(i(A),obs)F(i,mod) } 
	   Ÿ (s(Nsup3(+)E;i)(in)SDO3(x)a  ﬁ s{i}SDO3(x)™a ) Ÿ s(N;i)(in)SDO3(x) c Ÿ s(E;i)(in)SDO3(x) b 
Fix a = b
	= "x : N ◊ "i : N ◊ "a : Fma{ F(obs)  F(mod) } ◊ 
	   $b,c : Fma{ F(obs)  F(mod) } ◊ a,b,c Œ Fma{F(i(A),obs)F(i,mod) } 
	   Ÿ (s(Nsup3(+)E;i)(in)SDO3(x)a  ﬁ s{i}SDO3(x)™a ) Ÿ s(N;i)(in)SDO3(x) c Ÿ s(E;i)(in)SDO3(x) a 

Fix a = c
	= "x : N ◊ "i : N ◊ "a : Fma{ F(obs)  F(mod) } ◊ 
	   $b,c : Fma{F(obs)  F(mod) } ◊ a,b,c Œ Fma{F(i(A),obs)F(i,mod) } 
	   Ÿ (s(Nsup3(+)E;i)(in)SDO3(x)a  ﬁ s{i}SDO3(x)™a ) Ÿ s(N;i)(in)SDO3(x) a Ÿ s(E;i)(in)SDO3(x) b 

E.7  Eventual Progress and Accessibility

EP ∫ "x : N ◊ "i : N ◊ "a : F ◊ $c : F ◊ s{i}SDO3(x)™a ﬁ s{i}SDO3(x)™c  
AC ∫ "x : N ◊ "i : N ◊ "b : F ◊ s{i}(in)[ksdo3(i)]SDO3(x)b  ﬁ s{i}SDO3(x)™b

Compatible Property: 
EP Ÿ AC 
	= "x : N ◊ "i : N ◊ "a,b : F ◊ $c : F ◊  
	   ( s{i}SDO3(x)™a ﬁ s{i}SDO3(x)™c ) Ÿ ( s{i}(in)SDO3(x)b ﬁ s{i}SDO3(x)™b )
Fix a = b
	= "x : N ◊ "i : N ◊ "a,b : F ◊ $c : F ◊  
	   ( s{i}SDO3(x)™b ﬁ s{i}SDO3(x)™c ) Ÿ ( s{i}(in)SDO3(x)b ﬁ s{i}SDO3(x)™b )
	= "x : N ◊ "i : N ◊ "a,b : F ◊ $c : F ◊  
	   s{i}(in)SDO3(x)b  ﬁ s{i}SDO3(x)™c 
Fix c = b
	= "x : N ◊ "i : N ◊ "a,b : F ◊ $c : F ◊  
	   ( s{i}SDO3(x)™a ﬁ s{i}SDO3(x)™b ) Ÿ ( s{i}(in)SDO3(x)b ﬁ s{i}SDO3(x)™b )

E.8  Environment Optimistic Confidentiality and Faithfulness

EOC ∫ "x : N ◊ "i :  N ◊ $ A : Fma{F(i(A),obs)  F(i,mod)} ◊ 
	$ B : Fma{F(obs)  F(mod)} ◊ 
	BŒ Fma{F(i(A),obs)  F(i,mod)} Ÿ s(N;i)(in)SDO3(x) A Ÿ s(E;i)(in) SDO3(x) B
Separating into sub-properties:
	EOCsdo3(1) ∫ "x : N ◊ "i : N ◊ $ C : Fma{F(i(A),obs)  F(mod)} ◊ 
		C Œ Fma{F(i(A),obs)  F(mod)} Ÿ s(N;i)(in)SDO3(x) C 
	EOCsdo3(2) ∫ "x : N ◊ "i : N ◊ $ D : Fma{F(obs)  F(mod)} ◊ 
		D Œ Fma{F(i(A),obs)  F(mod)} Ÿ s(E;i)(in)SDO3(x) D
FT ∫ "x : N ◊ "i : N ◊ ""a : Fma{F} ◊ $ b : Fma{F} ◊  
	( (a;b) Ÿ s{i}(in)SDO3(x) a ) ﬁ s{i}(out) SDO3(x) ™b 
	= "x : N ◊ "i : N ◊ "a : Fma{F} ◊ $ b : Fma{F} ◊  
	(  (a;b) Ÿ s(Nsup3(+)E;i)(in)SDO3(x) a ) ﬁ s(i;Nsup3(+)E)(out) SDO3(x) ™b  

Compatible Property: 
EOC Ÿ FT 
	= "x : N ◊ "i : N ◊ "a : Fma{F(i(A),obs)  F(mod))} ◊ 
	   $ b : Fma{F(i(A),obs)  F(mod))} ◊ 
	   $ c : Fma{F(i(A),obs)  F(mod)} ◊ $ d : Fma{F(obs)  F(mod)} ◊ 
 	   a,b,c Œ Fma{ (F(i(A),obs)  F(mod)) } 
	   Ÿ D Œ Fma{ (F(i(A),obs)  F(mod)) }
	   Ÿ ( ( (a;b) Ÿ (s(N;i)(in)SDO3(x) a ⁄ s(E;i)(in)SDO3(x) a ) )
	      ﬁ ( s(i;N)(out) SDO3(x) ™b ⁄ s(i;E)(out) SDO3(x) ™b ) )
	   Ÿ s(N;i)(in)SDO3(x) c Ÿ s(E;i)(in)SDO3(x) d 

Fix a = c
	= "x : N ◊ "i : N ◊ "a : Fma{F(i(A),obs)  F(mod))} ◊ 
	   $ b : Fma{F(i(A),obs)  F(mod))} ◊ 
	   $ c : Fma{F(i(A),obs)  F(mod)} ◊ $ d : Fma{F(obs)  F(mod)} ◊ 
 	   a,b,c Œ Fma{ (F(i(A),obs)  F(mod)) } 
	   Ÿ D Œ Fma{ (F(i(A),obs)  F(mod)) }
	   Ÿ ( ( (a;b) Ÿ (s(N;i)(in)[ksdo3(i)] SDO3(x) a ⁄ s(E;i)(in)[ksdo3(i)] SDO3(x) a ) )
	      ﬁ ( s(i;N)(out) SDO3(x) ™b ⁄ s(i;E)(out) SDO3(x) ™b ) )
	   Ÿ s(N;i)(in)SDO3(x) a Ÿ s(E;i)(in)SDO3(x) d 
Fix b = c
	= "x : N ◊ "i : N ◊ "a : Fma{F(i(A),obs)  F(mod))} ◊ 
	   $ b : Fma{F(i(A),obs)  F(mod))} ◊ 
	   $ c : Fma{F(i(A),obs)  F(mod)} ◊ $ d : Fma{F(obs)  F(mod)} ◊ 
 	   a,b,c Œ Fma{(F(i(A),obs)  F(mod)) } 
	   Ÿ D Œ Fma{ (F(i(A),obs)  F(mod)) }
	   Ÿ ( ( (a;b) Ÿ (s(N;i)(in)SDO3(x) a ⁄ s(E;i)(in)SDO3(x) a ) )
	      ﬁ ( s(i;N)(out) SDO3(x) ™b ⁄ s(i;E)(out) SDO3(x) ™b ) )
	   Ÿ s(N;i)(in)SDO3(x) b Ÿ s(E;i)(in)SDO3(x) d 
Fix a = d
	= "x : N ◊ "i : N ◊ "a : Fma{F(i(A),obs)  F(mod))} ◊ 
	   $ b : Fma{F(i(A),obs)  F(mod))} ◊ 
	   $ c : Fma{F(i(A),obs)  F(mod)} ◊ $ d : Fma{F(obs)  F(mod)} ◊ 
 	   a,b,c ŒFma{ (F(i(A),obs) F(mod)) } Ÿ D ŒFma{ F(i(A),obs) F(mod) }
	   Ÿ ( ( (a;b) Ÿ (s(N;i)(in)SDO3(x) a ⁄ s(E;i)(in)SDO3(x) a ) )
	      ﬁ ( s(i;N)(out) SDO3(x) ™b ⁄ s(i;E)(out) SDO3(x) ™b ) )
	   Ÿ s(N;i)(in)SDO3(x) c Ÿ s(E;i)(in)SDO3(x) a 
Fix b = d
	= "x : N ◊ "i : N ◊ "a : Fma{F(i(A),obs)  F(mod))} ◊ 
	   $ b : Fma{F(i(A),obs)  F(mod))} ◊ 
	   $ c : Fma{F(i(A),obs)  F(mod)} ◊ $ d : Fma{F(obs)  F(mod)} ◊ 
 	   a,b,c Œ Fma{ (F(i(A),obs)  F(mod)) } 
	   Ÿ D Œ Fma{ (F(i(A),obs)  F(mod)) }
	   Ÿ ( ( (a;b) Ÿ (s(N;i)(in)SDO3(x) a ⁄ s(E;i)(in)SDO3(x) a ) )
	      ﬁ ( s(i;N)(out) SDO3(x) ™b ⁄ s(i;E)(out) SDO3(x) ™b ) )
	   Ÿ s(N;i)(in)SDO3(x) c Ÿ s(E;i)(in)SDO3(x) b 

Fix a = c, b = d
	= "x : N ◊ "i : N ◊  "a : Fma{F(i(A),obs)  F(mod))} ◊ 
	   $ b : Fma{F(i(A),obs)  F(mod))} ◊ 
	   $ c : Fma{F(i(A),obs)  F(mod)} ◊ $ d : Fma{F(obs)  F(mod)} ◊ 
 	   a,b,c Œ Fma{(F(i(A),obs)  F(mod)) } 
	   Ÿ D Œ Fma{(F(i(A),obs)  F(mod)) }
	   Ÿ ( ( (a;b) Ÿ (s(N;i)(in)SDO3(x) a ⁄ s(E;i)(in)SDO3(x) a ) )
	      ﬁ ( s(i;N)(out) SDO3(x) ™b ⁄ s(i;E)(out) SDO3(x) ™b ) )
	   Ÿ s(N;i)(in)SDO3(x) a Ÿ s(E;i)(in)SDO3(x) b 
Fix a = d, b = c
	= "x : N ◊ "i : N ◊ "a : Fma{F(i(A),obs)  F(mod))} ◊ 
	   $ b : Fma{F(i(A),obs)  F(mod))} ◊ 
	   $ c : Fma{F(i(A),obs)  F(mod)} ◊ $ d : Fma{F(obs)  F(mod)} ◊ 
 	   a,b,c Œ Fma{ (F(i(A),obs)  F(mod)) } 
	   Ÿ D Œ Fma{ (F(i(A),obs)  F(mod)) }
	   Ÿ (a=d) Ÿ (b=c) Ÿ ( ( (a;b) Ÿ ( s(N;i)(in)SDO3(x) d ⁄ s(E;i)(in)SDO3(x) d ) )
	   ﬁ ( s(i;N)(out) SDO3(x) ™b ⁄ s(i;E)(out) SDO3(x) ™b ) )
	   Ÿ s(N;i)(in)SDO3(x) b Ÿ s(E;i)(in)SDO3(x) d 

E.9  Faithfulness and Eventual Output

FT ∫ "x : N ◊ "i : N ◊ "a : F ◊ $ b : F ◊  
	( (a;b) Ÿ s{i}(in) SDO3(x) a ) ﬁ s{i}(out)SDO3(x) ™b 
EO ∫ "x : N ◊ "i : N ◊ "a : F ◊ $b : F ◊ s{i}SDO3(x)a ﬁ s{i}(out)SDO3(x)™b 

Compatible Property:
FT Ÿ EO = " a ◊ $ b : F ◊ ( (a;b) Ÿ s{i}(in) SDO3(x) a ) ﬁ s{i}(out)SDO3(x) ™b  

E.10  Authenticity and Provenance

AU ∫ "x : N ◊ "i : N ◊ $ A : Fma{Fsup3(i)(A)} ◊ s(isup3(+)E;Nsup3(+)E)(out)SDO3(x) A 
PV ∫ "x : N ◊ "i : N ◊ " A : Fma{F} ◊ s{i}(in)SDO3(x) ™A ﬁ s(NSUP3(+)E;i)(out)SDO3(x) A 
	"x : N ◊ "i : N ◊ " B : Fma{F} ◊ s{i}(in)SDO3(x) ™B ﬁ s(NSUP3(+)E;i)(out)SDO3(x) B 

Compatible Property:
AU Ÿ PV = "x : N ◊ "i : N ◊ " B ◊ $ A : Fma{F(i(A))} ◊
	   (s(isup3(+)E;Nsup3(+)E)(out)SDO3(x) A) Ÿ ( s{i}(in)SDO3(x) ™B ﬁ s(NSUP3(+)E;i)(out)SDO3(x) B )

E.11  Provenance and Utility

PV ∫ "x : N ◊ "i : N ◊ " A : Fma{F} ◊ s{i}(in)SDO3(x) ™A ﬁ s(NSUP3(+)E;i)(out)SDO3(x) A 
UT ∫ "x : N ◊ "i : N ◊ " A : Fma{F} ◊ s(NSUP3(+)E;i)(out)SDO3(x) A ﬁ s{i}(in)SDO3(x) ™A

Compatible Property:
PV Ÿ UT = " A : Fma{F(i(A))} ◊ s{i}(in)SDO3(x) ™A Ÿ s(NSUP3(+)E;i)(out)SDO3(x) A

Appendix F:  Examples and Applications

F.1  Compatibility of Properties

If we represent the MAC and DAC policies as formal policies, as given below, we can examine the compatiblity of these properties. 
Predicates: 
own(s,o)  			Subject s owns object o
grant_access(s,s',o)  		Subject s grants access to object o to subject s'
read_access(s,o)  		Subject s has read access to object o
write_access(s,o)		Subject s has write access to object o
dominates(s,o)		Security level of subject s strictly dominates security level 
				of object o
equal(s,o)			Security level of subject s is equal to security level of object o

Properties: 
DAC = "s : Subjects   ◊  "o : Objects  ◊  
	own(s,o) Ÿ grant_access(s,s',o) ﬁ read_access(s',o) Ÿ write_access(s',o)

MAC = "s : Subjects   ◊  "o : Objects  ◊  
	( dominates(s,o) ﬁ read_access(s,o) Ÿ ÿwrite_access(s'o) )
	Ÿ ( ÿdominates(s,o) ﬁ ÿread_access(s,o) Ÿ write_access(s,o) )
	Ÿ ( equal(s,o) ﬁ read_access(s,o) Ÿ write_access(s,o) )

MAC Ÿ DAC 
	= "s : Subjects   ◊  "o : Objects  ◊  
	   ( own(s,o) Ÿ grant_access(s,s',o) ﬁ read_access(s',o) Ÿ write_access(s',o) ) 
	   Ÿ ( dominates(s,o) ﬁ read_access(s',o) Ÿ ÿwrite_access(s',o) )
	   Ÿ ( ÿdominates(s,o) ﬁ ÿread_access(s',o) Ÿ write_access(s',o) )
	   Ÿ ( equal(s,o) ﬁ read_access(s',o) Ÿ write_access(s',o) )
	= "s : Subjects   ◊  "o : Objects  ◊  
	   ( ( own(s,o) Ÿ grant_access(s,s',o) ﬁ read_access(s',o) Ÿ write_access(s',o) )
	   ⁄ ( (dominates(s,o) ﬁ read_access(s',o) Ÿ write_access(s',o) ) 
	        Ÿ (ÿdominates(s,o) ﬁ read_access(s',o) Ÿ write_access(s',o) )
	        Ÿ ( equal(s,o) ) ﬁ read_access(s',o) Ÿ write_access(s',o) ) ) )
	   Ÿ ( dominates(s,o) ﬁ read_access(s',o) Ÿ ÿwrite_access(s',o) )
	   Ÿ ( ÿdominates(s,o) ﬁ ÿread_access(s',o) Ÿ write_access(s',o) )
	   Ÿ ( equal(s,o) ﬁ read_access(s',o) Ÿ write_access(s',o) )
	
	= "s : Subjects   ◊  "o : Objects  ◊  
	   ( ( own(s,o) Ÿ grant_access(s,s',o) ﬁ read_access(s',o) Ÿ write_access(s',o) )
	      Ÿ ( dominates(s,o) ﬁ read_access(s',o) Ÿ ÿwrite_access(s',o) )
	      Ÿ ( ÿdominates(s,o) ﬁ ÿread_access(s',o) Ÿ write_access(s',o) )
	      Ÿ ( equal(s,o) ﬁ read_access(s',o) Ÿ write_access(s',o) ) )
	   ⁄ ( (dominates(s,o) ﬁ read_access(s',o) Ÿ write_access(s',o) ) 
	       Ÿ (ÿdominates(s,o) ﬁ read_access(s',o) Ÿ write_access(s',o) )
	       Ÿ ( equal(s,o) ) ﬁ read_access(s',o) Ÿ write_access(s',o) ) 
	      Ÿ ( dominates(s,o) ﬁ read_access(s',o) Ÿ ÿwrite_access(s',o) )
	      Ÿ ( ÿdominates(s,o) ﬁ ÿread_access(s',o) Ÿ write_access(s',o) )
	      Ÿ ( equal(s,o) ﬁ read_access(s',o) Ÿ write_access(s',o) ) )
	= ^

Assume that a given component Csdo3(i) satisfies DAC
	sat(Csdo3(i), DAC)
	= own(s,o) Ÿ grant_access(s,s',o) ﬁ read_access(s',o) Ÿ write_access(s',o)
	= ( own(s,o) Ÿ grant_access(s,s',o) ﬁ read_access(s',o) Ÿ write_access(s',o) )
	   ⁄ ( (dominates(s,o) ﬁ read_access(s',o) Ÿ write_access(s',o) ) 
	        Ÿ (ÿdominates(s,o) ﬁ read_access(s',o) Ÿ write_access(s',o) )
	        Ÿ ( equal(s,o) ) ﬁ read_access(s',o) Ÿ write_access(s',o) ) )
	O(ﬁ,/)  MAC

Assume that a given component Csdo3(i) satisfies MAC
	sat(Csdo3(i), MAC)
	ﬁ ( dominates(s,o) Ÿ own(s,o) Ÿ grant_access(s,s',o) 
	     ﬁ read_access(s',o) Ÿ ÿwrite_access(s',o) ) )
	   Ÿ ( ÿdominates(s,o) Ÿ own(s,o) Ÿ grant_access(s,s',o) 
	     ﬁ ÿread_access(s',o) Ÿ write_access(s',o) ) )
	   Ÿ ( equal(s,o) Ÿ own(s,o) Ÿ grant_access(s,s',o) 
	     ﬁ read_access(s',o) Ÿ write_access(s',o) ) )
	O(ﬁ,/)  DAC

F.2.  Emergent Properties

This system is made up of two components, a multi-level system, B, (with hi and lo) and a single-level system, A, (hi only).  System A is used to form a feedback loop over system B.  The complete system is illustrated in Figure 11.1.  This system is described in detail in [TLBS88].  

F.2.1  GNI as an Emergent Property
The structure of system B is given in Figure F.1.  The composite system has been shown to be GNI-secure [TLBS88].  B3 is defined as a multi-level security component and therefore system B is also multi-level.  Even though components B2 and B3 are functionally identical, the output of B2 is rated hi, while the output of B3 is rated lo.  Either the output of B2 must be hi, implying that the output of B3 must also be hi, or that the output of B2 must be lo, implying that the connection of B2 and B3 is inadmissible.  Either of these scenaria should be enough to disallow the lo output of B3. 

Figure F.1:  Composition of Multi-Channel, Multi-Level-Security Components 

The desired and actual behaviour of the individual components is defined as follows: 
B1:   	Psdo3(1):  "x : N ◊  $ c :F(hi,out) ◊  s{B1}(out)[hi6] SDO3(x) c
B2:   	Psdo3(2):  "x : N ◊  " a,b : F(hi,in) ◊ $ c :F(hi,out) ◊
	   ( s{B2}(in)[hi1] SDO3(x) a Ÿ s{B2}(in)[hi2] SDO3(x) b ) Ÿ s{B2}(out)[hi3] SDO3(x) f 
   	Psdo3(3):  "x : N ◊  " a,b : F(hi,in) ◊ $ f : F(hi,out) ◊ f = a  b
B3:   	Psdo3(4):  "x : N ◊  " a,b : F(hi,in) ◊  $ d : F(lo,out) ◊  
	    ( s{B3}(in)[hi4] SDO3(x) a Ÿ s{B3}(in)[hi5] SDO3(x) b ) Ÿ ( s{B3}(out)[lo] SDO3(x) d )
   	Psdo3(5):  "x : N ◊  " a,b : F(hi,in) ◊ $ d : F(lo,out) ◊ d = a  b
B3 as described is NOT GNI-secure: any change to the lo-level output can be attributed to a change in one of the two hi-level inputs.  
Given the interconnections of B1, B2, and B3 defined in Figure F.1, the behaviour of the composite system &sup3(P)(&sup3(C)(Bsdo3(1),Bsdo3(3)),&sup3(C)(Bsdo3(2),Bsdo3(3))) = B123 is given as
B(B123):  Bsdo3(6): "x : N ◊  " a,b : F(hi,in) ◊  $ d : F(lo,out) ◊ 
	   ( s{B123}(in)[hi1] SDO3(x) a Ÿ s{B123}(in)[hi2] SDO3(x) b Ÿ s{B123}(out)[hi6] SDO3(x) c ) 
	   	ﬁ ( s{B123}(out)[lo] SDO3(x) d )
	     Bsdo3(7):  "x : N ◊  " a,b,c : F(hi) ◊  $ d : F(lo,out) ◊ d = (a  b  c)
The goal of this system is for two hi-level inputs to be the exclusive-or of the hi-inputs and the hi-output, producing a single lo-level output.  Represented formally, this gives the required properties of the composite system behaviour.
P(B123):   Psdo3(6):  "x : N ◊  " a,b : F(hi,in) ◊  " c : F(hi,out) ◊  $ d : F(lo,out) ◊ 
	   ( s{B123}(in)[hi1] SDO3(x) a Ÿ s{B123}(in)[hi2] SDO3(x) b Ÿ s{B123}(out)[hi6] SDO3(x) c )  
	   	ﬁ ( s{B123}(out)[lo] SDO3(x) d )
	       Psdo3(7):  "x : N ◊  " a,b,c : F(hi) ◊  $ d : F(lo,out) ◊ d = (a  b  c)

The output d does not give any information about the values of the high-level inputs.  We may formalise this goal for system B123 in terms of GNI as follows:
GNI = Psdo3(8):  "x : N ◊  " a,b,l : F(hi,in) ◊  " c,k : F(hi,out) ◊  $ d : F(lo,out) ◊  
	   ( s{B123}(in)[hi1] SDO3(x) (a⁄l) Ÿ s{B123}(in)[hi2] SDO3(x) (b⁄l) 
		Ÿ s{B123}(out)[hi6] SDO3(x) (c⁄k) )  ﬁ ( s{B123}(out)[lo] SDO3(x) d )
The hi-level output c can account for any changes caused by replacing a hi-level input with any other high-level input, including null.  A lo-level user cannot determine if a change in d is due to a change in the hi-level input or the hi-level output c.  
For the composite system, following the algorithms of chapter 10, we prove that GNI acts as an emergent property this (GNI-secure) composite system; GNI is gained on the composition of the individual components of this system. 
"s(C,i=1)P(Csdo3(i)) = P(Bsdo3(1)) " P(Bsdo3(2)) " P(Bsdo3(3)) = { Psdo3(1), Psdo3(2), Psdo3(3), Psdo3(4), Psdo3(5) } 
(s(C,i=1)P(Csdo3(i)) = ∆
PART I: 
"Psdo3(k) : { Psdo3(1), Psdo3(2), Psdo3(3), Psdo3(4), Psdo3(5) }
	P(C) "= Psdo3(1) Ÿ satisfies(Psdo3(1),C)
	ÿrelevant(Psdo3(2),C) 
	ÿrrelevant(Psdo3(3),C) 
	P(C) "= Psdo3(4) Ÿ satisfies(Psdo3(4),C) 
	P(C) "= Psdo3(5) Ÿ satisfies(Psdo3(5),C)
RESULT: P(C) =P(B123) = {Psdo3(1), Psdo3(4), Psdo3(5)}

PART II:
"Psdo3(j) : B(B123) = {Psdo3(6), Psdo3(7), Psdo3(8)}
	Psdo3(6) œ P(C) ⁄ P(similar systems)
		P(C) "= Psdo3(6) Ÿ satisfies(Psdo3(6),C) 
	Psdo3(7) œ P(C)  ⁄ P(similar systems)
		P(C) "= Psdo3(7)Ÿ satisfies(Psdo3(7),C)
	Psdo3(8) œ P(C) ⁄ P(similar systems)
		P(C) "= Psdo3(8)Ÿ satisfies(Psdo3(8),C) 
RESULT: P(C) =P(B123)  = {Psdo3(1), Psdo3(4), Psdo3(5),Psdo3(6), Psdo3(7), Psdo3(8)}

satisfies(Psdo3(8),C) :  
    B(B123) = Psdo3(6) Ÿ Psdo3(7)
= "x : N ◊  " a,b : F(hi,in) ◊  " c : F(hi,out) ◊  $ d : F(lo,out) ◊ 
	   [ ( s{B123}(in)[hi1] SDO3(x) a Ÿ s{B123}(in)[hi2] SDO3(x) b 
	     Ÿ s{B123}(out)[hi6] SDO3(x) c ) ﬁ ( s{B123}(out)[lo] SDO3(x) d ) ] Ÿ d = (a  b  c)
Replace a by (a⁄l), b by (b⁄l) and c by (c⁄k) 
= "x : N ◊  " a,b : F(hi,in) ◊  " c : F(hi,out) ◊  $ d : F(lo,out) ◊ 
	   [ ( s{B123}(in)[hi1] SDO3(x) (a⁄l) Ÿ s{B123}(in)[hi2] SDO3(x) (b⁄l)
	     Ÿ s{B123}(out)[hi6] SDO3(x) (c⁄k) ) ﬁ ( s{B123}(out)[lo] SDO3(x) d ) ]
	   Ÿ d = ( (a⁄l)   (b⁄l)  (c⁄k) )

= "x : N ◊  " a,b : F(hi,in) ◊  " c : F(hi,out) ◊  $ d : F(lo,out) ◊ 
	   [ ( s{B123}(in)[hi1] SDO3(x) (a⁄l) Ÿ s{B123}(in)[hi2] SDO3(x) (b⁄l)
	     Ÿ s{B123}(out)[hi6] SDO3(x) (c⁄k) ) ﬁ ( s{B123}(out)[lo] SDO3(x) d ) ]
	   Ÿ d = ( (a  b  c) ⁄ (a  l  c) ⁄ (a  b  k  ⁄ (a  l  k) 
	   ⁄ (l  b  c) ⁄ (c) ⁄ (l  b  k ) ⁄ (k) )
ﬁ "x : N ◊  " a,b : F(hi,in) ◊  " c : F(hi,out) ◊  $ d : F(lo,out) ◊ 
	   [ ( s{B123}(in)[hi1] SDO3(x) (a⁄l) Ÿ s{B123}(in)[hi2] SDO3(x) (b⁄l)
	     Ÿ s{B123}(out)[hi6] SDO3(x) (c⁄k) ) ﬁ ( s{B123}(out)[lo] SDO3(x) d ) ]
	   Ÿ d = (a  b  c)
ﬁ GNI  

F.2.2  GNI as a De-Emergent Property
In this section we examine the composition of components A and B, both individually generalised non-interference secure (GNI-secure).  The behaviour and properties of system B is described in the previous section (B(B123) = P(B123)).  The behaviour and properties of component A are described by: 
	B(A) = P(A) = "x : N ◊  " a :F(hi) ◊  in(x) = a  € out(x) = a
If we connect the output of system B, out(hi6) with the input of system A, in(hiA), and the output of system A, out(hiA), with one of the high inputs of system B, in(hi1).  The behaviour of the composite system is given as: 
B(&(B123,A)) = B(B123) Ÿ B(A):  
	"x : N ◊  " a,b : F(hi,in) ◊  $ d : F(lo,out) ◊ 
	   [ ( s{B123}(in)[hi1] SDO3(x) a Ÿ s{B123}(in)[hi2] SDO3(x) b  
	   Ÿ  s{B123}(out)[hi6] SDO3(x) c ) ﬁ ( s{B123}(out)[lo] SDO3(x) d ) ] 
	   Ÿ  d = (a  b  c) Ÿ  [ ( s{A}(in)[hiA] SDO3(x) c Ÿ s{A}(out)[hiA] SDO3(x) a  
But, a=c by P(A)
	"x : N ◊  " a,b : F(hi,in) ◊  $ d : F(lo,out) ◊ 
	   [ ( s{B123}(in)[hi1] SDO3(x) a Ÿ s{B123}(in)[hi2] SDO3(x) b  
	   Ÿ  s{B123}(out)[hi6] SDO3(x) a ) ﬁ ( s{B123}(out)[lo] SDO3(x) d ) ] Ÿ  d = b 
	   Ÿ  [ ( s{A}(in)[hiA] SDO3(x) a Ÿ s{A}(out)[hiA] SDO3(x) a  
Writing this as two individual, independent behaviours, 
	Bsdo3(9) = "x : N ◊  " a,b : F(hi,in) ◊  $ d : F(lo,out) ◊ 
 	   s{B123A}(in)[hi2] SDO3(x) b Ÿ s{B123A}(out)[lo] SDO3(x) d 
	Bsdo3(10) = "x : N ◊  " a,b : F(hi,in) ◊  $ d : F(lo,out) ◊ d = b 
The desired behaviour for this component is given by the following properties 
P(&(B123,A)):
	Psdo3(9) = "x : N ◊  " a,b : F(hi,in) ◊  $ d : F(lo,out) ◊ 
 	   s{B123A}(in)[hi2] SDO3(x) b Ÿ s{B123A}(out)[lo] SDO3(x) d 
	Psdo3(10) = "x : N ◊  " a,b : F(hi,in) ◊  $ d : F(lo,out) ◊ d π b
The actual behaviour, B(&(B123,A)) does not entail the desired behaviour, P(&(B123,A)).  This is easily determined by comparing the behaviours:
	Bsdo3(9) ﬁ Psdo3(9) = T
	Bsdo3(10) ﬁ Psdo3(10) = ^
Therefore, the goal of the behaviour of this system (treated as a pedantic property) is not satisfied by the actual behaviour of the system.  
The informally described GNI-property of system B is applicable (relevant) to the composite system and will ideally act as a type 1 emergent property for the composite system.  Assessing GNI for the system given the behaviour B(&(B123,A)), we see that the composite system does not satisfy this property.  
	B(&(B123,A)) 	
	= "x : N ◊  " a,b : F(hi,in) ◊  $ d : F(lo,out) ◊ 
 	   s{B123A}(in)[hi2] SDO3(x)  (b⁄l) Ÿ s{B123A}(out)[lo] SDO3(x) d Ÿ  d =  (b⁄l)
	o(ﬁ,/) GNI
There are no possible changes to the high-level output (there are none) that may account for any changes to the high-level inputs: all such changes are reflected in the low-level outputs.  Thus GNI acts as a de-emergent property.     

F.3  Progress

F.3.1  Specification of Components
Each event is defined as a predicate (for example, gotFSDO3(i)) that may be true or false at any time during execution.  If the predicate gotFSDO3(i) is true for component PSDO3(i), for example, this indicates that the philosopher PSDO3(i) has possession of the component FSDO3(i).  A P-component, PSDO3(i), must gain possession of the F-components FSDO3(i) and FSDO3(i≈1), where i≈1 represents modular addition.  We also use iO(O,SUP1(-))1 to represent modular subtraction.

Allowable Events:
Philosophers: 	inputPSDO3(i ){ eat, gotFSDO3(i), gotFSDO3(i≈1) }
			outputPSDO3(i ){ getFSDO3(i), getFSDO3(i≈1), releaseFSDO3(i),  releaseFSDO3(i≈1), think } 
Forks:		inputFSDO3(i){ getFSDO3(i), releaseFSDO3(i) }
			outputFSDO3(i){ gotFSDO3(i), null }
Input-output behaviour rules: 
Philosophers:  	PSDO3(i)( eat ; getFSDO3(i) )
			PSDO3(i)( gotFSDO3(i ); getFSDO3(i≈1) )
			PSDO3(i)( gotFSDO3(i≈1) ; eating )
			PSDO3(i)( eating ; releaseFSDO3(i) Ÿ releaseFSDO3(i≈1) Ÿ think )
Forks:		FSDO3(i)( getFSDO3(i ); gotFSDO3(i) )
			FSDO3(i)( releaseFSDO3(i ); null )

Component Behaviour Axioms:
Philosophers:
•	A philosopher not possessing any forks and told to try to eat will attempt to obtain the fork to his left.  He is still in the state of having no forks.  
CB1	"PSDO3(i ): {Philosophers} ◊ "x : N ◊  s(E;PSDO3(i))SDO3(x) eat ﬁ s(PSDO3(i);E)SDO3(x) ™getFSDO3(i)  
•	Once the philospher has received his left fork, he is in the state of having that fork and will attempt to get his right-hand fork. 
CB2	"PSDO3(i ): {Philosophers} ◊ "x : N ◊ 
	   s{PSDO3(i)}SDO3(x) ( ÿgotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) ) Ÿ s(E;PSDO3(i))SDO3(x) gotFSDO3(i)  ﬁ  
	   s{PSDO3(i)}SDO3(x) O( gotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) ) Ÿ s(PSDO3(i);E)SDO3(x) ™getFSDO3(i≈1) 

•	Once the philospher has his right fork, he is in the state of having both forks.  He will begin eating.
CB3	"PSDO3(i ): {Philosophers} ◊ "x : N ◊ 
	   s{PSDO3(i)}SDO3(x) ( gotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) ) Ÿ s(E;PSDO3(i))SDO3(x) gotFSDO3(i≈1)  
	   ﬁ  s{PSDO3(i)}SDO3(x) O( gotFSDO3(i) Ÿ gotFSDO3(i≈1) ) Ÿ s(PSDO3(i);PSDO3(i))SDO3(x) ™eating
•	A philosopher that is eating will eventually release both forks and return to thinking.
CB4	"PSDO3(i ): {Philosophers} ◊ "x : N ◊ s{PSDO3(i)}SDO3(x)(gotFSDO3(i) Ÿ gotFSDO3(i≈1) ) Ÿ s(PSDO3(i);PSDO3(i)) SDO3(x)eating
	  ﬁ s{PSDO3(i)}SDO3(x )O(gotFSDO3(i )Ÿ gotFSDO3(i≈1)) 
	      Ÿ s(PSDO3(i);E)SDO3(x)™(releaseFSDO3(i) Ÿ releaseFSDO3(i≈1)Ÿ think)
Forks:
•	A fork that is not granted, and receives a request for ownership will be granted and the fork will eventually acknowledge this granting to the philosopher.
CB5	"FSDO3(j ): {Forks} ◊ "x : N ◊ ( j=i ⁄ j=i≈1 ) Ÿ s{FSDO3(j)}SDO3(x)ÿgranted Ÿ s(E;FSDO3(j))SDO3(x)getFSDO3(j) 
	   ﬁ s{FSDO3(j)}SDO3(x) Ogranted Ÿ s(FSDO3(j);E) SDO3(x) ™gotFSDO3(j) 
•	A fork that is granted and possessed by a component will not be granted and will not be possessed by that component after that component sends a release fork request.
CB6	"PSDO3(i ): {Philosophers} ◊ "x : N ◊ 
	   ( j=i ⁄ j=i≈1 ) Ÿ s{FSDO3(j)}SDO3(x) granted Ÿ s(E;FSDO3(j))SDO3(x) releaseFSDO3(j) 
 	   ﬁ s{FSDO3(j)}SDO3(x) Oÿgranted Ÿ s(FSDO3(j);E)SDO3(x) ™null 

F.3.2  Proofs of Basic Progress Properties of Components
Classification of Behaviours: 
Input- & Output-State Independent: CB1
Input-State Independent: None
Output-State Independent:  CB4
State-Dependent:  CB2, CB3, CB5, CB6

We will examine the satisfiabilty of faithfulness for the component behaviours.  If and when we find behaviours that do not satisfy faithfulness, we will examine the behaviours in detail with respect to the first four basic progress properties. 

Input- & Output-State Independent Behaviours:
	sat(CB1, FT)	
FT	"x : N ◊ "a : F{PSDO3(i)}  ◊ $ b : F{PSDO3(i)}  ◊   
	   ( (a;b) Ÿ s{PSDO3(i)}(in) SDO3(x) a ) ﬁ s{PSDO3(i)}(out) SDO3(x) ™b 
Let (a;b) be the input-output pair (eat ; getFSDO3(i))
	= "x : N ◊ ( (eat ; getFSDO3(i)) Ÿ s{PSDO3(i)}(in) SDO3(x) eat ) ﬁ s{PSDO3(i)}(out) SDO3(x) ™getFSDO3(i) 
	= "x : N ◊ ( (T) Ÿ s{PSDO3(i)}(in) SDO3(x) eat ) ﬁ s{PSDO3(i)}(out) SDO3(x) ™getFSDO3(i) 
	= CB1

Output-State Independent Behaviours:
	sat(CB4, FT)	
FT	= "x : N ◊ "a : F{PSDO3(i)}  ◊ $ b : F{PSDO3(i)}  ◊   
	   ( (a;b) Ÿ s{PSDO3(i)}(in) SDO3(x) a ) ﬁ s{PSDO3(i)}(out) SDO3(x) ™b 

Let (a;b) be the input-output pair (eating ; releaseFSDO3(i) Ÿ releaseFSDO3(i≈1) Ÿ think)
	= "x : N ◊  ( (eating ; releaseFSDO3(i) Ÿ releaseFSDO3(i≈1) Ÿ think) Ÿ s{PSDO3(i)}(in) SDO3(x)eating ) 
	   ﬁ s{PSDO3(i)}(out) SDO3(x) ™(releaseFSDO3(i) Ÿ releaseFSDO3(i≈1) Ÿ think)
	= "x : N ◊   
	   ( (T) Ÿ s{PSDO3(i)}(in) SDO3(x) eating Ÿ s{PSDO3(i)}SDO3(x) (gotFSDO3(i) Ÿ gotFSDO3(i≈1))⁄ÿ(gotFSDO3(i) Ÿ gotFSDO3(i≈1)) ) 
	   ﬁ s{PSDO3(i)}(out) SDO3(x) ™(releaseFSDO3(i) Ÿ releaseFSDO3(i≈1) Ÿ think)
	= "x : N ◊ ( s{PSDO3(i)}(in) SDO3(x) eating Ÿ s{PSDO3(i)}SDO3(x) (gotFSDO3(i) Ÿ gotFSDO3(i≈1)) )
	      ﬁ [ s{PSDO3(i)}(out) SDO3(x) ™(releaseFSDO3(i) Ÿ releaseFSDO3(i≈1) Ÿ think)
		Ÿ s{PSDO3(i)}SDO3(x )O( (gotFSDO3(i )Ÿ gotFSDO3(i≈1))⁄ÿ(gotFSDO3(i )Ÿ gotFSDO3(i≈1)) ) ] 
	   Ÿ ( s{PSDO3(i)}(in) SDO3(x) eating Ÿ s{PSDO3(i)}SDO3(x) ÿ(gotFSDO3(i) Ÿ gotFSDO3(i≈1)) ) 
	      ﬁ [ s{PSDO3(i)}(out) SDO3(x) ™(releaseFSDO3(i) Ÿ releaseFSDO3(i≈1) Ÿ think)
		Ÿ s{PSDO3(i)}SDO3(x )O( (gotFSDO3(i )Ÿ gotFSDO3(i≈1))⁄ÿ(gotFSDO3(i )Ÿ gotFSDO3(i≈1)) ) ] 
	= "x : N ◊ { [ ( s{PSDO3(i)}(in) SDO3(x) eating Ÿ s{PSDO3(i)}SDO3(x) (gotFSDO3(i) Ÿ gotFSDO3(i≈1)) )
	      ﬁ [ s{PSDO3(i)}(out) SDO3(x) ™(releaseFSDO3(i) Ÿ releaseFSDO3(i≈1) Ÿ think) 
		Ÿ s{PSDO3(i)}SDO3(x )O( (gotFSDO3(i )Ÿ gotFSDO3(i≈1)) ] ]
	      ⁄ [ s{PSDO3(i)}(in) SDO3(x) eating Ÿ s{PSDO3(i)}SDO3(x) (gotFSDO3(i) Ÿ gotFSDO3(i≈1)) )
	      ﬁ [ s{PSDO3(i)}(out) SDO3(x) ™(releaseFSDO3(i) Ÿ releaseFSDO3(i≈1) Ÿ think) 
		Ÿ s{PSDO3(i)}SDO3(x )Oÿ(gotFSDO3(i )Ÿ gotFSDO3(i≈1)) ) ] ] }
	   Ÿ { [ ( s{PSDO3(i)}(in) SDO3(x) eating Ÿ s{PSDO3(i)}SDO3(x) ÿ(gotFSDO3(i) Ÿ gotFSDO3(i≈1)) ) 
	      ﬁ [ s{PSDO3(i)}(out) SDO3(x) ™(releaseFSDO3(i) Ÿ releaseFSDO3(i≈1) Ÿ think)
		Ÿ s{PSDO3(i)}SDO3(x )O( (gotFSDO3(i )Ÿ gotFSDO3(i≈1)) ] ]
	      ⁄ [ (s{PSDO3(i)}(in) SDO3(x) eating Ÿ s{PSDO3(i)}SDO3(x) ÿ(gotFSDO3(i) Ÿ gotFSDO3(i≈1)) ) 
	      ﬁ [ s{PSDO3(i)}(out) SDO3(x) ™(releaseFSDO3(i) Ÿ releaseFSDO3(i≈1) Ÿ think)
		Ÿ s{PSDO3(i)}SDO3(x )O( ÿ(gotFSDO3(i )Ÿ gotFSDO3(i≈1)) ) ] ] }
	‹ "x : N ◊ s{PSDO3(i)}SDO3(x) ( gotFSDO3(i) Ÿ gotFSDO3(i≈1) ) Ÿ s(PSDO3(i);PSDO3(i)) SDO3(x) eating
	   ﬁ s{PSDO3(i)}SDO3(x )O( gotFSDO3(i )Ÿ  gotFSDO3(i≈1)) 
	       Ÿ s(PSDO3(i);E)SDO3(x)™(releaseFSDO3(i) Ÿ releaseFSDO3(i≈1) Ÿ think)
	= CB4

	sat(CB2,FT)
Let (a;b) be the input-output pair (gotFSDO3(i) ; getFSDO3(i≈1) )
	= "x : N ◊ ( (gotFSDO3(i) ; getFSDO3(i≈1) ) Ÿ s{PSDO3(i)}(in) SDO3(x) gotFSDO3(i) ) ﬁ s{PSDO3(i)}(out) SDO3(x) ™getFSDO3(i≈1) 
	= "x : N ◊ { [ ( s{PSDO3(i)}(in) SDO3(x) gotFSDO3(i) Ÿ s{PSDO3(i)}SDO3(x) (ÿgotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) ) )
	      ﬁ ( s{PSDO3(i)}(out) SDO3(x) ™getFSDO3(i≈1) Ÿ s{PSDO3(i)}SDO3(x )O( gotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) ) ) ]
	      ⁄ [ ( s{PSDO3(i)}(in) SDO3(x) gotFSDO3(i) Ÿ s{PSDO3(i)}SDO3(x) (ÿgotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) ) )
	      ﬁ ( s{PSDO3(i)}(out) SDO3(x) ™getFSDO3(i≈1) Ÿ s{PSDO3(i)}SDO3(x) Oÿ(ÿgotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) ) ) ] 
	   Ÿ { [ ( s{PSDO3(i)}(in) SDO3(x) gotFSDO3(i) Ÿ s{PSDO3(i)}SDO3(x) ÿ(ÿgotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) ) ) 
	      ﬁ ( s{PSDO3(i)}(out) SDO3(x) ™getFSDO3(i≈1) Ÿ s{PSDO3(i)}SDO3(x) O(ÿgotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) ) ) ]
	      ⁄ [ (s{PSDO3(i)}(in) SDO3(x) gotFSDO3(i) Ÿ s{PSDO3(i)}SDO3(x) ÿ(ÿgotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) ) ) 
	      ﬁ ( s{PSDO3(i)}(out) SDO3(x) ™getFSDO3(i≈1) Ÿ s{PSDO3(i)}SDO3(x) Oÿ(ÿgotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) ) ) ] }
	‹ CB2

We can likewise prove that CB3 ﬁ FT,  CB5 ﬁ FT, and CB6 ﬁ FT.  Thus if the component behaviours are accurately described by the component behaviour axioms, then the component's behaviours will satify progress.  Because these components are not intended to act as stand-alone components, we will not assess their progress for all possible inputs.  Instead, we note those behaviours that are input-state dependent, and the inputs that will not be acted upon in each input-state, for consideration within the context of the composite system. 

Behaviour Axiom	
Input State	
Affected Inputs	
CB4	s{PSDO3(i)}SDO3(x) (gotFSDO3(i) Ÿ gotFSDO3(i≈1) )	gotFSDO3(i) 
gotFSDO3(i≈1) 	
CB2	s{PSDO3(i)}SDO3(x) (ÿgotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) )	gotFSDO3(i≈1) 
eating	
CB3	s{PSDO3(i)}SDO3(x) (gotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) )	gotFSDO3(i) 	
CB5	s{FSDO3(i)}SDO3(x) ÿgranted	releaseFSDO3(i) 	
CB6	s{FSDO3(i)}SDO3(x) granted	getFSDO3(i) 	

Note that the input eat is not included as an affected input.  This is because eat is defined by CB1, an input-state independent behaviour axiom.  Thus the component will always be available to an eat input.

F.3.3  Composite System Specification
The composite system is pictured in Figure F.2.  
Interconnection rules:	
	( outputPSDO3(i)(0) ; inputFSDO3(i)(0) )
	( outputPSDO3(i)(1) ; inputFSDO3(i≈1) (1) )
	( outputPSDO3(i)(2) ; environs )
	( outputFSDO3(i)(0) ; inputPSDO3(i)(0) )
	( outputFSDO3(i≈1) (1) ; inputPSDO3(i)(1) )
	( environs ; inputPSDO3(i)(2) )

Composite System Properties:
The following property is requirement on the behaviour of the composite system: 
	"PSDO3(i ): {Philosophers} ◊ ( s(E;PSDO3(i)) SDO3(x) eat  ﬁ  s{PSDO3(i);E)SDO3(x)™think )
These axioms define the state of the components in the system. 
•	A fork component that is not granted is not held by either possible philosopher component.
"PSDO3(i ): {Philosophers} ◊ 
  ( (s{PSDO3(i)} SDO3(x) ÿgotFSDO3(i) Ÿ s{PSDO3(i≈1)) SDO3(x) ÿgotFSDO3(i)) ‹ s{FSDO3(i)} SDO3(x) ÿgranted )
•	If either philosopher component has possession of a fork component then that fork component is granted.
"PSDO3(i ): {Philosophers} ◊ ( (s{PSDO3(i)} SDO3(x) gotFSDO3(j) O(⁄,SUP5(.)) s{PSDO3(iO(O,SUP1(-))1))SDO3(x) gotFSDO3(j) )ﬁ s{FSDO3(j)}SDO3(x) granted )

•	If a philosopher component has possession of its right-hand fork then it will also have possession of its left-hand fork.
"PSDO3(i ): {Philosophers} ◊ ( s{PSDO3(i)} SDO3(x) gotFSDO3(i≈1) ﬁ ( s{PSDO3(i)} SDO3(x) gotFSDO3(i) Ÿ gotFSDO3(i≈1) ) )
 
System Behaviour Axioms:
•	A philosopher not possessing any forks and told (by an outside source) to try to eat will attempt to obtain the fork to his left.  He is still in the state of having no forks.  
SB1	"PSDO3(i ): {Philosophers} ◊ "FSDO3(i ): {Forks} ◊ "x : N ◊ 
	   s{PSDO3(i)}SDO3(x) ( ÿgotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) ) Ÿ s(E;PSDO3(i))SDO3(x) eat  ﬁ  
	   s{PSDO3(i)}SDO3(x) O( ÿgotFSDO3(i)  Ÿ ÿgotFSDO3(i≈1) ) Ÿ s(PSDO3(i);FSDO3(i))SDO3(x) ™getFSDO3(i)  
•	Once the philospher has received his left fork, he is in the state of having that fork and will attempt to get his right-hand fork. 
SB2	"PSDO3(i ): {Philosophers} ◊ "FSDO3(i ): {Forks} ◊ "x : N ◊ 
	   s{PSDO3(i)}SDO3(x) ( ÿgotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) ) Ÿ s(FSDO3(i);PSDO3(i))SDO3(x) gotFSDO3(i)  ﬁ  
	   s{PSDO3(i)}SDO3(x) O( gotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) ) Ÿ s(PSDO3(i);FSDO3(i≈1))SDO3(x) ™getFSDO3(i≈1) 
•	Once the philospher has his right fork, he is in the state of having both forks.  He will begin eating.
SB3	"PSDO3(i ): {Philosophers} ◊ "FSDO3(i ): {Forks} ◊ "x : N ◊ 
	   s{PSDO3(i)}SDO3(x) ( gotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) ) Ÿ s(FSDO3(i≈1);PSDO3(i))SDO3(x) gotFSDO3(i≈1)  
	   ﬁ  s{PSDO3(i)}SDO3(x) O( gotFSDO3(i) Ÿ gotFSDO3(i≈1) ) Ÿ s(PSDO3(i);PSDO3(i))SDO3(x) ™eating  
•	A philosopher that is eating will eventually release both forks and return to thinking.
SB4	"PSDO3(i ): {Philosophers} ◊ "FSDO3(i ): {Forks} ◊ "x : N ◊ 
	   s{PSDO3(i)}SDO3(x) ( gotFSDO3(i) Ÿ gotFSDO3(i≈1) ) Ÿ s(PSDO3(i);PSDO3(i))SDO3(x) eating
	   ﬁ s{PSDO3(i)}SDO3(x )O( gotFSDO3(i )Ÿ  gotFSDO3(i≈1)) 
	       Ÿ s(PSDO3(i);FSDO3(i)SUP3(+)FSDO3(i≈1)SUP3(+)E)SDO3(x)™(releaseFSDO3(i) Ÿ releaseFSDO3(i≈1) Ÿ think)
•	A fork that is not granted, and receives a request from a philosopher, will be granted and the fork will eventually acknowledge this granting to the philosopher.
SB5	"PSDO3(i ): {Philosophers} ◊ "FSDO3(j ): {Forks} ◊ "x : N ◊ 
	   ( j=i ⁄ j=i≈1 )  Ÿ s{FSDO3(j)}SDO3(x) ÿgranted Ÿ  s(PSDO3(i);FSDO3(j))SDO3(x) getFSDO3(j)  		
	   ﬁ  s{FSDO3(j)} SDO3(x) Ogranted Ÿ s(FSDO3(j);PSDO3(i))SDO3(x) ™gotFSDO3(j) 
•	A fork that is granted and possessed by a component will not be granted and will not be possessed by that component after that component sends a release fork request.
SB6	"PSDO3(i ): {Philosophers} ◊ "FSDO3(j ): {Forks} ◊ "x : N ◊ 
	   ( j=i ⁄ j=i≈1 ) Ÿ s{FSDO3(j)} SDO3(x) granted Ÿ s{PSDO3(i)}SDO3(x) gotFSDO3(j) Ÿ s(PSDO3(i);FSDO3(j))SDO3(x) releaseFSDO3(j)  	  
	 ﬁ  s{FSDO3(j)} SDO3(x) Oÿgranted Ÿ s{PSDO3(i)}SDO3(x) OÿgotFSDO3(j)  Ÿ s(FSDO3(j);E)SDO3(x) ™null 

Repeating the table given above, we add the column "Required Input", where the required input is that will return the component to the input-state required by the affected input.

Behaviour Axiom	
Input State	Affected Inputs	Required 
Input	
CB4	s{PSDO3(i)}SDO3(x) (gotFSDO3(i) Ÿ gotFSDO3(i≈1) )	gotFSDO3(i) 	eating	
	s{PSDO3(i)}SDO3(x) (gotFSDO3(i) Ÿ gotFSDO3(i≈1) )	gotFSDO3(i≈1) 	eating	
CB2	s{PSDO3(i)}SDO3(x) (ÿgotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) )	gotFSDO3(i≈1) 	Not Poss	
	s{PSDO3(i)}SDO3(x) (ÿgotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) )	eating	Not Poss	
CB3	s{PSDO3(i)}SDO3(x) (gotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) )	eating	Not Poss	
CB3	s{PSDO3(i)}SDO3(x) (gotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) )	gotFSDO3(i) 	Not Poss	
CB5	s{FSDO3(i)}SDO3(x) ÿgranted	releaseFSDO3(i) 	Not Poss	
CB6	s{FSDO3(i)}SDO3(x) granted	getFSDO3(i) 	releaseFSDO3(i) 	

CB4 requires the input eating, which follows from the definition of CB4.  The affected inputs of axioms CB2, CB3, and CB5 are not possible for the given input-state within the context of the composite system.  The affected input of CB6, getFSDO3(i) received by a fork component while the fork is granted, however, does require that the input releaseFSDO3(i)  be received by the fork component.  If this input is not received, then the fork will not be able to process the input getFSDO3(i) .  Thus the fork component may not satisfy progress within the composite system if it does not receive the required input releaseFSDO3(i) .  
The next question to be addressed, therefore, is whether it is possible that this required input will never be received.  If the component FSDO3(i) is contained within a circular path or behaviour, then it is possible that the lack of the required input will cause the path and system to exhibit deadlock.  There are two distinct circular paths within the composite system: Psdo3(i), Fsdo3(i), Psdo3(i) and Psdo3(i), FSDO3(i≈1), Psdo3(i).  Each must be examined in detail to determine if it will deadlock. 
Any of the standard deadlock-detection algorithms, applied to those paths that include the components FSDO3(i), can be used to assess the possibility of deadlock.  We did not start with these algorithms because it is instructive to examine these behaviours and pin-point potential problems before examining the system for deadlock.  
To begin with, we list the source and destination of events and the associated state-change between input and output for each behaviour axiom.  We use the Chandy-Misra-Haas algorithm [CMH83], where the path of a probe through the system is the same as the path of a given event through a system.  
	(SB1)	E ; PSDO3(i) ﬁ PSDO3(i) ; FSDO3(i)  
		 No state change 
	(SB5)	(PSDO3(i) ; FSDO3(i) ﬁ FSDO3(i) ; PSDO3(i) ) ⁄  (PSDO3(iO(O,SUP1(-))1); FSDO3(i) ﬁ FSDO3(i) ; PSDO3(iO(O,SUP1(-))1))
		FSDO3(i) SDO3(x) ÿgranted ﬁ FSDO3(i) SDO3(x) Ogranted
	(SB2)	FSDO3(i) ; PSDO3(i) ﬁ PSDO3(i) ; FSDO3(i≈1) 
		PSDO3(i) SDO3(x) ÿgotFSDO3(i) ﬁ PSDO3(i) SDO3(x) OgotFSDO3(i) 
	(SB5)	(PSDO3(i) ; FSDO3(i≈1) ﬁ FSDO3(i≈1) ; PSDO3(i) ) Ÿ (PSDO3(i≈1) ; FSDO3(i≈1) ﬁ FSDO3(i≈1) ; PSDO3(i≈1) )
		FSDO3(i≈1) SDO3(x) ÿgrantedﬁ FSDO3(i≈1) SDO3(x) Ogranted
	(SB3)	FSDO3(i≈1) ; PSDO3(i) ﬁ PSDO3(i) ; PSDO3(i)  
		PSDO3(i) SDO3(x) ÿgotFSDO3(i≈1) ﬁ PSDO3(i) SDO3(x) OgotFSDO3(i≈1) 
	
	(SB4)	PSDO3(i) ; PSDO3(i) ﬁ PSDO3(i) ; FSDO3(i≈1)SUP3(+) FSDO3(i) SUP3(+) E  
		PSDO3(i) SDO3(x) (gotFSDO3(i) Ÿ gotFSDO3(i≈1)) ﬁ PSDO3(i) SDO3(x) ™(ÿgotFSDO3(i) Ÿ ÿgotFSDO3(i≈1)) 
As described by the system behaviour axioms, the output sent from PSDO3(i) is received as an input at FSDO3(i) which may also receive inputs from PSDO3(iO(O,SUP1(-))1).  Because both inputs will have the same effect on the state of FSDO3(i), and because PSDO3(i) cannot continue to execute until it receives a response from FSDO3(i), we must consider the effects of these input events at FSDO3(i).  We will prove that if PSDO3(i) sends an event to component FSDO3(i), which in turn has previously received a similar request from PSDO3(iO(O,SUP1(-))1), that PSDO3(i) will eventually gain possession of component FSDO3(i).  Therefore we must prove the following statement:
	$i . $u . $z>u . s(PSDO3(i);FSDO3(i))SDO3(u) getFSDO3(i) Ÿ s{FSDO3(i)} SDO3(u) granted Ÿ s(FSDO3(i);PSDO3(iO(O,SUP1(-))1))SDO3(u) gotFSDO3(i) 
	ﬁ s{PSDO3(i)}SDO3(z) (gotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) ) 
Proof  $i . $u . s(PSDO3(i);FSDO3(i))SDO3(u) getFSDO3(i) Ÿ s{FSDO3(i)}SDO3(u) granted Ÿ s(FSDO3(i);PSDO3(iO(O,SUP1(-))1))SDO3(u) gotFSDO3(i) 
State	ﬁ $i . $u . s(PSDO3(i);FSDO3(i))SDO3(u) getFSDO3(i) Ÿ s{FSDO3(i)}SDO3(u) granted  
	     Ÿ s{PSDO3(i)}SDO3(z) (ÿgotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) ) Ÿ s(FSDO3(i);PSDO3(iO(O,SUP1(-))1))SDO3(u) gotFSDO3(i) 
SB3	ﬁ $i . $v>u . s(PSDO3(i);FSDO3(i))SDO3(v) getFSDO3(i) Ÿ s{FSDO3(i)}SDO3(v) granted 
	     Ÿ s{PSDO3(i)}SDO3(v) (ÿgotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) ) Ÿ s{PSDO3(iO(O,SUP1(-))1)}SDO3(v) O( gotFSDO3(iO(O,SUP1(-))1) Ÿ gotFSDO3(i) )
	     Ÿ s(PSDO3(iO(O,SUP1(-))1);PSDO3(iO(O,SUP1(-))1)) SDO3(v) ™eating  
SB4	ﬁ $i . $w>v . s(PSDO3(i);FSDO3(i))SDO3(w) getFSDO3(i)  Ÿ s{FSDO3(i)}SDO3(w) granted 
	     Ÿ s{PSDO3(iO(O,SUP1(-))1)}SDO3(w) O( gotFSDO3(iO(O,SUP1(-))1) Ÿ gotFSDO3(i) ) 
	     Ÿ s(PSDO3(iO(O,SUP1(-))1);FSDO3(i)SUP3(+)FSDO3(iO(O,SUP1(-))1)SUP3(+)E) SDO3(w) ™( releaseFSDO3(iO(O,SUP1(-))1) Ÿ releaseFSDO3(i) Ÿ think) 
SB6	ﬁ $i . $x>w . s(PSDO3(i);FSDO3(i))SDO3(x) getFSDO3(i) Ÿ s{FSDO3(i)}SDO3(x) Oÿgranted 
	    Ÿ s{PSDO3(iO(O,SUP1(-))1)}SDO3(x) O( ÿgotFSDO3(iO(O,SUP1(-))1) Ÿ ÿgotFSDO3(i) ) Ÿ s(FSDO3(i);E) SDO3(x) ™null
SB5	ﬁ $i . $y>x .  s(FSDO3(i);PSDO3(i))SDO3(y) ™gotFSDO3(i) Ÿ s{FSDO3(i)}SDO3(y) Ogranted 			
SB2	ﬁ $i . $z>y . s{PSDO3(i)}SDO3(z) (gotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) )  			o
The philosopher will get the fork, and will be able to progress.  If the event received from PSDO3(iO(O,SUP1(-))1) had been a release, the event from PSDO3(i) would have been acted upon and there would not have been a possible impediment to progress.
Given the second instantiation of SB5, what will happen if, according to SB2, PSDO3(i) sends an event to component FSDO3(i≈1), which in turn has previously received a similar request from  PSDO3(i≈1)?  In this case, we are required to prove the following:  
	$i . $w . $ z>w . s(PSDO3(i);FSDO3(i≈1))SDO3(w) getFSDO3(i≈1) Ÿ s{FSDO3(i≈1)}SDO3(w)granted
	   Ÿ s(FSDO3(i≈1);PSDO3(i≈1))SDO3(w) gotFSDO3(i≈1) Ÿ s{PSDO3(i)}SDO3(z)  ( gotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) )
	ﬁ s{PSDO3(i)}SDO3(z)  ( gotFSDO3(i)  Ÿ gotFSDO3(i≈1) ) 
Proof  $i . $w . s(PSDO3(i);FSDO3(i≈1))SDO3(w) getFSDO3(i≈1) Ÿ s{FSDO3(i≈1)}SDO3(w)granted
	   Ÿ s(FSDO3(i≈1);PSDO3(i≈1))SDO3(w) gotFSDO3(i≈1)
State	ﬁ $i . $w .s(PSDO3(i);FSDO3(i≈1)) SDO3(w) getFSDO3(i≈1) Ÿ s{FSDO3(i≈1)}SDO3(w) granted 
	   Ÿ s{PSDO3(i)}SDO3(w)  ( gotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) ) Ÿ sS(FSDO3(i≈1);PSDO3(i≈1))SDO3(w) gotFSDO3(i≈1)

SB2	ﬁ $i . $x>w . s(PSDO3(i);FSDO3(i≈1))SDO3(x) getFSDO3(i≈1) Ÿ s{FSDO3(i≈1)}SDO3(x) granted 
	   Ÿ s{PSDO3(i)}SDO3(z)  ( gotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) )
	   Ÿ s{PSDO3(i≈1)}SDO3(x)  ( gotFSDO3(i≈1) Ÿ ÿgotFSDO3(i≈2) ) Ÿ s(PSDO3(i≈1);FSDO3(i≈2))SDO3(x) ™getFSDO3(i≈2) 
	ﬁ $i . $y>x . s(PSDO3(i);FSDO3(i≈1))SDO3(x) getFSDO3(i≈1) Ÿ s{FSDO3(i≈1)}SDO3(x) granted 
	   Ÿ s{PSDO3(i)}SDO3(z) ( gotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) )
	   Ÿ s{PSDO3(i≈1)}SDO3(x)  ( gotFSDO3(i≈1) Ÿ ÿgotFSDO3(i≈2) ) Ÿ s(PSDO3(i≈1);FSDO3(i≈2))SDO3(x) ™getFSDO3(i≈2)  
	   Ÿ s{FSDO3(i≈2)}SDO3(y)  ( granted ⁄ ÿgranted) 
But we do not know the state of component FSDO3(i≈2).  If the component is not granted, then we can simply follow through with the proof that the component will eventually be able to progress.  If the component is granted, we must continue with the investigation. 
 SB2	ﬁ $i . $y . s(PSDO3(i);FSDO3(i≈1))SDO3(y) getFSDO3(i≈1) Ÿ s{FSDO3(i)}SDO3(y) granted  
	  Ÿ s{PSDO3(i)}SDO3(y)  (gotFSDO3(i)  Ÿ ÿgotFSDO3(i≈1)) Ÿ s(PSDO3(i≈1);FSDO3(i≈2))SDO3(y) getFSDO3(i≈2) Ÿ s{FSDO3(i≈1)}SDO3(y)  granted 
	  Ÿ s{PSDO3(i≈1)} SDO3(y)  (gotFSDO3(i≈1) Ÿ ÿgotFSDO3(i≈2))Ÿ s(PSDO3(i≈2);FSDO3(i≈3))SDO3(y) getFSDO3(i≈3) 
	  Ÿ s{FSDO3(i≈2)}SDO3(y)  granted Ÿ s{PSDO3(i≈2)}SDO3(y)  ( gotFSDO3(i≈2)  Ÿ ÿgotFSDO3(i≈3) ) 
We can see (and easily prove) that if we continue to experience the worst case scenario of the required component always being granted, we will end up with the following specification:
 SB2	ﬁ $i . $y . s(PSDO3(i);FSDO3(i≈1))SDO3(y) getFSDO3(i≈1) Ÿ s{FSDO3(i)}SDO3(y) granted  
	  Ÿ s{PSDO3(i)}SDO3(y)(gotFSDO3(i) ŸÿgotFSDO3(i≈1)) Ÿ s(PSDO3(i≈1);FSDO3(i≈2))SDO3(y) getFSDO3(i≈2)Ÿ s{FSDO3(i≈1)}SDO3(y) granted 
	  Ÿ s{PSDO3(i≈1)}SDO3(y)  (gotFSDO3(i≈1) Ÿ ÿgotFSDO3(i≈2))Ÿ s(PSDO3(i≈2);FSDO3(i≈3))SDO3(y) getFSDO3(i≈3) 
	  Ÿ s{FSDO3(i≈2)}SDO3(y)  granted Ÿ s{PSDO3(i≈2)}SDO3(y)  ( gotFSDO3(i≈2)  Ÿ ÿgotFSDO3(i≈3) ) 
	  Ÿ ... 
	  Ÿ s(PSDO3(iO(O,SUP1(-))1);FSDO3(i))SDO3(z)getFSDO3(i) Ÿ s{FSDO3(iO(O,SUP1(-))1)}SDO3(z)granted Ÿ s{PSDO3(iO(O,SUP1(-))1)}SDO3(z)(gotFSDO3(iO(O,SUP1(-))1) Ÿ ÿgotFSDO3(i) )     o
In this case, every P-component has sent a request to an F-component, which is not able to be granted because the F-component is in turn granted to a different P-component.     
This system cannot progress in this situation;  each P-component is waiting for a specific input which it will not receive and therefore the P-component cannot progress.  Because the P-components cannot progress, they will not be able to produce as an output the input required by the F-components that will allow the F-components to progress, which would in turn allow the P-components to progress.
This situation can be described as follows:
 "i.$x. O(Ÿ,SDO5(i)) {s{FSDO3(i)}SDO3(x) granted Ÿ s(PSDO3(i);FSDO3(i≈1))SDO3(x) getFSDO3(i≈1) Ÿ s{PSDO3(i)}SDO3(x) (gotFSDO3(i) Ÿ ÿgotFSDO3(i≈1)) } 
=  "i.$x. O(Ÿ,SDO5(i)) {s{PSDO3(i≈1)}SDO3(x)  gotFSDO3(i≈1) Ÿ s(PSDO3(i);FSDO3(i≈1))SDO3(x) getFSDO3(i≈1) } 
Therefore, there are behaviours such that the system property 
			"i . sS(E;PSDO3(i)) SDO3(x) eat ﬁ sS(PSDO3(i);E) SDO3(x) ™think 
will never be true.  Using the notation given above, livelock and deadlock occur when:
	Livelock: 	$i.$x. O(Ÿ,SDO5(i)) {s{PSDO3(i≈1)}SDO3(x)  gotFSDO3(i≈1) Ÿ s(PSDO3(i);FSDO3(i≈1))SDO3(x) getFSDO3(i≈1) }  
	Deadlock: 	"i.$x. O(Ÿ,SDO5(i)) {s{PSDO3(i≈1)}SDO3(x)  gotFSDO3(i≈1) Ÿ s(PSDO3(i);FSDO3(i≈1))SDO3(x) getFSDO3(i≈1) }  
There have been many solutions proposed for this particular problem, including round-robin priorities on access to the forks, requiring a philosopher to put down their left fork if they cannot pick up their right fork, and so on.  We will chose to avoid the problem altogether by modifying the behaviour of the system.  This is in keeping with the design of a system: if it doesn't work, try a minor adjustment to see if that helps. 

F.3.4  Solution to Dining Philosophers Livelock
The system as defined requires that each philosopher begin by attempting to pick up their left fork.  The solution that we propose is to require all philosophers sitting in odd-numbered chairs to attempt to pick up their right-hand fork first, while the remaining even-numbered philosophers attempt to pick up their left-hand fork first.  We will prove this solution for an odd number of philosophers in the system.  It can be similarly proven to be true for an even number of philosophers. 
	Input-Output Events
Each philosopher is labelled as even or odd, depending on whether they are sitting in an even-numbered or odd-numbered chair at the table.
Philosophers:  	
	i odd		PSDO3(i)( eat ; getFSDO3(i≈1) )
			PSDO3(i)( gotFSDO3(i≈1) ; getFSDO3(i ))
			PSDO3(i)( gotFSDO3(i ); eating )
			PSDO3(i)( eating ; (releaseFSDO3(i) Ÿ releaseFSDO3(i≈1) Ÿ think) )
	i even 	PSDO3(i)( eat ; getFSDO3(i) )
			PSDO3(i)( gotFSDO3(i ); getFSDO3(i≈1)  )
			PSDO3(i)( gotFSDO3(i≈1) ; eating )
			PSDO3(i)( eating ; (releaseFSDO3(i) Ÿ releaseFSDO3(i≈1) Ÿ think) )
Forks:		FSDO3(i)( getFSDO3(i ); gotFSDO3(i) )
			FSDO3(i)( releaseFSDO3(i ); null )
Environment: 	E( think ; eat )		

	State Axioms
•	If an even-numbered philosopher component has possession of its right-hand fork then it will also have possession of its left-hand fork.
"i . i even . "x . s{PSDO3(i)} SDO3(x) gotFSDO3(i≈1) ﬁ ( s{PSDO3(i)} SDO3(x) gotFSDO3(i) Ÿ gotFSDO3(i≈1) )
•	If an odd-numbered philosopher component has possession of its left-hand fork then it will also have possession of its right-hand fork.
"i . i odd . "x . s{PSDO3(i)} SDO3(x) gotFSDO3(i) ﬁ ( s{PSDO3(i)} SDO3(x) gotFSDO3(i) Ÿ gotFSDO3(i≈1) )
	System Behaviour Axioms
•	An even-numbered philosopher who is thinking will be told (by an outside source) to try to eat and will eventually try to get their left-hand fork.  
SB1	"i . i even . $x . s{PSDO3(i)}SDO3(x) ( ÿgotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) ) Ÿ s(E;PSDO3(i)) SDO3(x) eat  ﬁ  
		s{PSDO3(i)} SDO3(x) O( ÿgotFSDO3(i)  Ÿ ÿgotFSDO3(i≈1)  ) Ÿ s(PSDO3(i);FSDO3(i))SDO3(x) ™getFSDO3(i)  
•	An even-numbered philosopher who has got possession of their left-hand fork will eventually try to get their right-hand fork.  
SB2	"i . i even . $x . s{PSDO3(i)}SDO3(x) ( ÿgotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) ) Ÿ s(FSDO3(i);PSDO3(i))SDO3(x) gotFSDO3(i)  ﬁ  
		s{PSDO3(i)}SDO3(x) O( gotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) ) Ÿ s(PSDO3(i);FSDO3(i≈1))SDO3(x) ™getFSDO3(i≈1) 
•	An even-numbered philosopher who has got possession of their right-hand fork will have possession of both forks and will eventually start eating.  
SB3	"i . i even . $x . s{PSDO3(i)}SDO3(x) ( gotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) ) Ÿ s(FSDO3(i≈1);PSDO3(i))SDO3(x) gotFSDO3(i≈1)  
		ﬁ  s{PSDO3(i)}SDO3(x) O( gotFSDO3(i) Ÿ gotFSDO3(i≈1) ) Ÿ s(PSDO3(i);PSDO3(i))SDO3(x)™eating
•	An odd-numbered philosopher who is thinking will be told (by an outside source) to try to eat and will eventually try to get their right-hand fork.  
SB4	"i . i odd . $x . s{PSDO3(i)}SDO3(x) ( ÿgotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) ) Ÿ sS(E;PSDO3(i)) SDO3(x) eat  ﬁ  
		s{PSDO3(i)}SDO3(x) O( ÿgotFSDO3(i)  Ÿ ÿgotFSDO3(i≈1)  ) Ÿ s(PSDO3(i);FSDO3(i≈1))SDO3(x) ™getFSDO3(i≈1)
•	An odd-numbered philosopher who has got possession of their right-hand fork will eventually try to get their left-hand fork.  
SB5	"i . i odd . $x . s{PSDO3(i)}SDO3(x) ( ÿgotFSDO3(i) Ÿ ÿgotFSDO3(i≈1) ) Ÿ s(FSDO3(i≈1);PSDO3(i))SDO3(x) gotFSDO3(i≈1) ﬁ  
		s{PSDO3(i)}SDO3(x) O( ÿgotFSDO3(i) Ÿ gotFSDO3(i≈1) ) Ÿ s(PSDO3(i);FSDO3(i≈1))SDO3(x) ™getFSDO3(i) 
•	An odd-numbered philosopher who has got possession of their left-hand fork will have possession of both forks and will eventually start eating.  
SB6	"i . i odd . $x . s{PSDO3(i)}SDO3(x) ( ÿgotFSDO3(i) Ÿ gotFSDO3(i≈1) ) Ÿ s(FSDO3(i);PSDO3(i))SDO3(x) gotFSDO3(i)   
		ﬁ  s{PSDO3(i)}SDO3(x) O( gotFSDO3(i) Ÿ gotFSDO3(i≈1) ) Ÿ s(PSDO3(i);PSDO3(i))SDO3(x)™eating
•	A philosopher who has got possession of both forks and is eating will eventually release both forks .  
SB7	"i . $x . s{PSDO3(i)}SDO3(x) ( gotFSDO3(i) Ÿ gotFSDO3(i≈1) ) Ÿ s(PSDO3(i);PSDO3(i))SDO3(x)eating
		ﬁ s{PSDO3(i)}SDO3(x )O ( gotFSDO3(i )Ÿ  gotFSDO3(i≈1)) 
		  Ÿ s(PSDO3(i);FSDO3(i)SUP3(+)FSDO3(i≈1)SUP3(+)E )SDO3(x)™(releaseFSDO3(i) Ÿ releaseFSDO3(i≈1) Ÿ think)
•	A fork that is not granted and is requested by a philosopher will be granted and will eventually be acknowledge as granted to the philosopher by the fork
SB8	"i,j . j=i ⁄ j=i≈1. $x . s{FSDO3(j)}SDO3(x) ÿgranted Ÿ  s(PSDO3(i);FSDO3(j))SDO3(x) getFSDO3(j)  
		ﬁ  s{FSDO3(j)}SDO3(x) Ogranted Ÿ s(FSDO3(j);PSDO3(i))SDO3(x) ™gotFSDO3(j)  
•	A fork that is granted and is possessed by a philosopher will no longer be granted and will not be possessed by that philosopher after that philosopher has produced a release fork event.
SB9	"i,j . j=i ⁄ j=i≈1. $x . s{FSDO3(j)}SDO3(x) granted Ÿ s{PSDO3(i)}SDO3(x) gotFSDO3(j) Ÿ s(PSDO3(i);FSDO3(j))SDO3(x) releaseFSDO3(j)  
		ﬁ  s{FSDO3(j)}SDO3(x) Oÿgranted Ÿ s{PSDO3(i)}SDO3(x) OÿgotFSDO3(j) Ÿ s(FSDO3(j);E)SDO3(x) ™null
  
Interconnection Rules
These are unaffected by this change in the definition of the system.

From the guidelines for assessing progress applied to the original problem, we see that there are two possible instances in which each philosopher may succumb to livelock.  An even-numbered philosopher may first experience livelock while attempting to obtain their left-hand fork, and then while attempting to obtain their right-hand fork.  An odd-numbered philosopher may first experience livelock while attempting to obtain their right-hand fork and then while attempting to obtain their left-hand fork.  Thus there are four cases which which we must examine to ensure that this modified system is free from livelock.   

F.3.4.1  Proof of Freedom from Livelock
Case 1:  Even-numbered philosopher attempting to access their left-hand fork, which is already granted.  We prove that regardless of whether the left-handed fork is granted to another philosopher or not, the even-numbered philosopher will eventually have possession of the fork.  
	$i . i even . $x . $z>x . s{PSDO3(i)}SDO3(x) (ÿgotFSDO3(i) Ÿ ÿgotFSDO3(i≈1)) 
	   Ÿ s(PSDO3(i);FSDO3(i))SDO3(x) ™getFSDO3(i)  Ÿ s{FSDO3(i)}SDO3(x) granted Ÿ s(PSDO3(iO(O,SUP1(-))1))SDO3(x) gotFSDO3(i)  
	ﬁ  s{PSDO3(i)}SDO3(z) (gotFSDO3(i) Ÿ ÿgotFSDO3(i≈1)) 
Case 2:   Even-numbered philosopher attempting to get possession of their right-handed fork, which is granted to another philosopher. 
	$i . i even . $w . $z>w . s{PSDO3(i)}SDO3(w) (gotFSDO3(i) Ÿ ÿgotFSDO3(i≈1))   
	   Ÿ s{PSDO3(i≈1)}SDO3(w) gotFSDO3(i≈1) Ÿ s(PSDO3(i);FSDO3(i≈1))SDO3(w) ™getFSDO3(i≈1)  
	 ﬁ s{PSDO3(i)}SDO3(z) (gotFSDO3(i) Ÿ ÿgotFSDO3(i≈1)) 

Proof  $i . i even . $w . s{PSDO3(i)}SDO3(w) (gotFSDO3(i) Ÿ ÿgotFSDO3(i≈1)) Ÿ s{PSDO3(i≈1)}SDO3(w) gotFSDO3(i≈1)  
	   Ÿ s(PSDO3(i);FSDO3(i≈1))SDO3(w) ™getFSDO3(i≈1)   
State, ﬁ $i . i even . $w . s{PSDO3(i)}SDO3(w) (gotFSDO3(i) Ÿ ÿgotFSDO3(i≈1)) 
 SB6	  Ÿ s{PSDO3(i≈1)}SDO3(w) (gotFSDO3(i≈1) Ÿ gotFSDO3(i≈2) ) Ÿ sS(PSDO3(i≈1);PSDO3(i≈1)) SDO3(w) ™eating
	   Ÿ s(PSDO3(i);FSDO3(i≈1))SDO3(w) ™getFSDO3(i≈1) Ÿ sS(FSDO3(i)) SDO3(w) granted Ÿ sS(FSDO3(i≈1)) SDO3(w) granted 
SB7, SB9, SB8, SB8	
	ﬁ $i . i even . $z>y . s{PSDO3(i)}SDO3(z) (gotFSDO3(i) Ÿ gotFSDO3(i≈1)) 				o
We can similarily prove that the system will not exhibit livelock for an odd-numbered philosopher attempting to access either his left or right-hand fork.  Therefore, all components the system as modified are free from livelock and the system is free from livelock and deadlock.
We can therefore easily prove the system-specific progress property of 
"i . sS(E;PSDO3(i)) SDO3(x) eat ﬁ sS(PSDO3(i);E) SDO3(x) ™think  
This redefined system will not exhibit livelock providing the individual components (the forks and the philosophers) obey the basic progress properties.    

F.4  Network Composition

F.4.1  Composition of Network System
In this section we examine the assessment of the basic safety properties of the network system given in section 11.5.  We begin by listing the properties of the components.
	P(A) = P(B) = { COC, COI, AU-E, AU }
	P(S) = { PC, PI, AU-E, AU }

Using the Composition Principle, we begin with the hypothesis of rule 3 of the principle, that is, that the components satisfy their relevant environment properties (assumptions).  

3.	sat(A, COC) Ÿ sat(A, COI) Ÿ sat(A, AU-E) ﬁ sat(A, AU)
sat(B, COC) Ÿ sat(B, COI) Ÿ sat(B, AU-E) ﬁ sat(B, AU)
sat(S, PC) Ÿ sat(S, PI) Ÿ sat(S, AU-E) ﬁ sat(S, AU)

This follows trivially given that we know that the components have already been evaluated and shown to satisfy all relevant properties. We now use rule 3 to prove rule 1 of the Composition Principle.  

1.	P(A)P(B)P(S) = { PC, PI, COC, COI, AU-E, AU }
	P(A)P(B)P(S) = { AU-E, AU }

AU Œ P(A)P(B)P(S)◊ ÿcomposable(AU) Ÿ relevant(AU) Ÿ AU Œ Msdo3(reqd)
AU-E Œ P(A)P(B)P(S)◊ ÿcomposable(AU-E) Ÿ relevant(AU-E) Ÿ AU-E Œ Msdo3(reqd)
COC Œ P(A) \ P(A)P(B)P(S) ◊ relevant(COC) Ÿ COC Œ Msdo3(reqd)
COI Œ P(A) \ P(A)P(B)P(S) ◊ relevant(COI) Ÿ COI Œ Msdo3(reqd)
PC Œ P(S) \ P(A)P(B)P(S) ◊ ÿrelevant(PC)
PI Œ P(S) \ P(A)P(B)P(S) ◊ ÿrelevant(PI)

Evaluating the properties of Msdo3(reqd) for the composite system, we find that 
sat(C, AU) Ÿ sat(C, AU-E) Ÿ sat(C, COC) Ÿ sat(C, COI) 

The relevant properties of COC and COI are not composable and therefore are not satisfied by the composite system.  Examining the system using the algorithm of Figure 10.2, we see that the only way we will have a usable system that is able to handle all three security levels is to trust the switch component not to send Top Secret events to component A and Confidential events to component B.  Assessing the domain of the system using Figure 10.1 and assuming the trustworthiness of the switch, we see that component optimistic confidentiality and integrity are satisfied.  
Authenticity is not composable because of the effects of changing the domain of the individual systems and the possible effects that would have in rendering previously acceptable events unacceptable.  Because the component optimistic properties are satisfied, however, we find that the domains do not change and that in this situation authenticity is in fact composable.  
Even though the switch satisfies pessimistic confidentiality and integrity, we can show that it also satisfies component optimistic confidentiality and integrity simply because all events that may be sent to it by the two components are acceptable to the switch.  This follows from the authenticity of components A and B, given that they may produce events that are {Confidential, Secret, Top Secret}, all of which are acceptable to the switch.

2.	P(C) = { COC, COI, AU-E, AU }

sat(C, AU-E) Ÿ sat(C, COC) Ÿ sat(C, COI) Ÿ  sat(B, AU) Ÿ sat(S, AU) 
ﬁ sat(A, AU-E) Ÿ sat(A, COC) Ÿ sat(A, COI) 
sat(C, AU-E) Ÿ sat(C, COC) Ÿ sat(C, COI) Ÿ  sat(A, AU) Ÿ sat(S, AU) 
ﬁ sat(B, AU-E) Ÿ sat(B, COC) Ÿ sat(B, COI) 
sat(C, AU-E) Ÿ sat(C, COC) Ÿ sat(C, COI) Ÿ  sat(A, AU) Ÿ sat(B, AU) 
ﬁ sat(S, AU-E) Ÿ sat(S, PC) Ÿ sat(S, PI) 

Thus the Composition Principle simplified the proof of the properties of the composite system given the knowledge of the properties of the components of the system.  The composition principle did not allow us to make any assumptions about properties that were not composable.  Instead, it highlighted where we had to go outside the principle to prove the satisfiability of certain properties.