Only Connect, Securely
Chandrika Bhardwaj, Sanjiva Prasad
TL;DR
This paper introduces a formal connection framework based on Lagois connections that enables secure information exchange between autonomous organizations with different security policies, ensuring non-interference and policy independence.
Contribution
It proposes a novel, mathematically rigorous framework for secure information flow across diverse organizational security lattices using Lagois connections.
Findings
Framework preserves non-interference
Ensures secure information exchange
Maintains organizational autonomy
Abstract
The lattice model proposed by Denning in her seminal work provided secure information flow analyses with an intuitive and uniform mathematical foundation. Different organisations, however, may employ quite different security lattices. In this paper, we propose a connection framework that permits different organisations to exchange information while maintaining both security of information flows as well as their autonomy in formulating and maintaining security policy. Our prescriptive framework is based on the rigorous mathematical framework of Lagois connections given by Melton, together with a simple operational model for transferring object data between domains. The merit of this formulation is that it is simple, minimal, adaptable and intuitive, and provides a formal framework for establishing secure information flow across autonomous interacting organisations. We show that our…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSecurity and Verification in Computing · Cloud Data Security Solutions · Network Security and Intrusion Detection
11institutetext: Indian Institute of Technology Delhi, India
11email: {chandrika,sanjiva}@cse.iitd.ac.in
Only Connect, Securely††thanks: Supported by Indo-Japanese project Security in the IoT Space, DST, Govt of India.
Chandrika Bhardwaj
Sanjiva Prasad
Abstract
The lattice model proposed by Denning in her seminal work provided secure information flow analyses with an intuitive and uniform mathematical foundation. Different organisations, however, may employ quite different security lattices. In this paper, we propose a connection framework that permits different organisations to exchange information while maintaining both security of information flows as well as their autonomy in formulating and maintaining security policy. Our prescriptive framework is based on the rigorous mathematical framework of Lagois connections given by Melton, together with a simple operational model for transferring object data between domains. The merit of this formulation is that it is simple, minimal, adaptable and intuitive, and provides a formal framework for establishing secure information flow across autonomous interacting organisations. We show that our framework is semantically sound, by proving that the connections proposed preserve standard correctness notions such as non-interference.
Keywords:
Security class lattice Information flow Lagois connection Atomic operations Non-interference.
1 Introduction
Denning’s seminal work [7] proposed complete lattices as the appropriate mathematical framework for questions regarding secure information flow (SIF). An information flow model (IFM) is characterised as where: Storage objects in are assigned security levels drawn from a (finite) complete lattice . is a set of processes (also assigned security classes as clearances). The partial ordering represents permitted flows between classes; reflexivity and transitivity capture intuitive aspects of information flow; antisymmetry helps avoid redundancies in the framework, and the join operation succinctly captures the combination of information belonging to different security classes in arithmetic, logical and computational operations. This lattice model provides an abstract uniform framework that identifies the commonalities of the variety of analyses for different applications – e.g., confidentiality and trust – whether at the language level or a system level. In the ensuing decades, the vast body of secure information flow analyses has been built on these mathematical foundations, with the development of a plethora of static and dynamic analysis techniques for programming languages [21, 17, 19, 13, 20, 15], operating systems [12, 25, 2, 8, 20], databases [22], and hardware architectures [9, 27], etc. The soundness of this lattice model was expressed in terms of semantic notions of system behaviour, for instance, as properties like non-interference [10] by Volpano et al [23] and others. Alternative semantic notions of security such as safety properties have been proposed as well, e.g., [1], but for brevity we will not explore these further.
The objective of this paper is to propose a simple way in which large-scale distributed secure systems can be built by connecting components in a secure and modular manner. Our work begins with the observation that large information systems are not monolithic: Different organisations define their own information flow policies independently, and subsequently collaborate or federate with one another to exchange information. In general, the security classes and the lattices of any two organisations may be quite different — there is no single universal security class lattice. Moreover, modularity and autonomy are important requirements since each organisation would naturally wish to retain control over its own security policies and the ability to redefine them. Therefore, fusing different lattices by taking their union is an unsatisfactory approach, more so since the security properties of application programs would have to be re-established in this possibly enormous lattice.
When sharing information, most organisations limit the cross-domain communications to a limited set of security classes (which we call transfer classes). In order to ensure that shared data are not improperly divulged, two organisations usually negotiate agreements or memorandums of understanding (MoUs), promising that they will respect the security policies of the other organisation. We argue that a good notion of secure connection should require reasoning only about those flows from only the transfer classes mentioned in a MoU. Usually, cross-domain communication involves downgrading the security class of privileged information to public information using primitives such as encryption, and then upgrading the information to a suitable security class in the other domain. Such approaches, however, do not gel well with correctness notions such as non-interference. Indeed the question of how to translate information between security classes of different lattices is interesting [6].
Contributions of this paper.
In this paper, we propose a simple framework and sufficient conditions under which secure flow guarantees can be enforced without exposing the complexities and details of the component information flow models. The framework consists of (1) a way to connect security classes of one organisation to those in another while satisfying intuitive requirements; (2) a simple language that extends the operations within an organisation with primitives for transferring data between organisations; and (3) a type system and operational model for these constructs, which we use to establish that the framework conserves security.
In §2, we first identify, using intuitive examples, violations in secure flow that may arise when two secure systems are permitted to exchange information in both directions. Based on these lacunae, we formulate security and precision requirements for secure bidirectional flow. We then propose a framework that guarantees the absence of such policy violations, without impinging on the autonomy of the individual systems, without the need for re-verifying the security of the application procedures in either of the domains, and confining the analysis to only the transfer classes involved in potential exchange of data. Our approach is based on monotone functions and an elegant theory of connections [16] between the security lattices. Theorem 2.1 shows that* Lagois connections* between the security lattices satisfy the security and precision requirements.
We present, in §3, a minimal operational language consisting of a small set of atomic primitives to effect the transfer of data between domains. The framework is simple and can be adapted for establishing secure connections between distributed systems at any level of abstraction (language, system, database, …). We assume each domain uses atomic transactional operations for object manipulation and intra-domain computation. The primitives of our model include reliable communication between two systems, transferring object data in designated output variables of one domain to designated input variables of a specified security class in the other domain. We also assume a generic set of operations in each domain for copying data from input variables to domain objects, and from domain objects to output variables. To avoid interference between inter-domain communication and the computations within the domains, we assume that the sets of designated input and output variables are all mutually exclusive of one another, and also with the program/system variables used in the computations within each domain. Thus by design we avoid the usual suspects that cause interference and insecure transfer of data. The operational description of the language consists of the primitives together with their execution rules (§3.1).
The correctness of our framework is demonstrated by expressing soundness (with respect to the operational semantics) of a type system (§3.2), stated in terms of the security lattices and their connecting functions. In particular, Theorem 3.1 shows the standard semantic property of non-interference in both domains holds of all operational behaviours. We adapt and extend the approach taken by Volpano et al [23] to encompass systems coupled using the Lagois connection conditions (and assuming atomicity of the data transfer operations), to show that security is conserved. We believe that our formulation is general enough to be applicable to other behavioural notions of secure information flow as a safety property [1].
In §4, we briefly review some related work. We conclude in §5 with a discussion on our approach and directions for future work.
2 Lagois Connections and All That
Motivating Examples.
Consider a university system in which students study in semi-autonomously administered colleges (one such is {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}C}) that are affiliated to a university ({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}U}). The university also has “university professors” with whom students can take classes. We assume each institution has established the security of its information flow mechanisms and policies.
We first observe that formulating an agreement between the institutions that respects the flow policies within the institutions is not entirely trivial. Consider an arrangement where the college Faculty and University Faculty can share information (say, course material and examinations), and the Dean of Colleges in the University can exchange information (e.g., students’ official grade-sheets) with the college’s Dean of Students. Even such an apparently reasonable arrangement suffers from insecurities, as illustrated in Fig. 2 by the flow depicted using dashed red arrows, where information can flow from the college’s Faculty to the college’s Dean of Students. (Moral: internal structure of the lattices matters.)
As long as information flows unidirectionally from colleges to the University, monotone functions from the security classes of the college lattice {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}C} to university security lattice {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}U} suffice to ensure secure information flow. A function {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}:{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}C}\rightarrow{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}U} is called monotone if whenever {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}sc_{1}}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\sqsubseteq}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}sc_{2}} in {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}C} then {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}sc_{1}})~{}{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\sqsubseteq^{\prime}}~{}{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}sc_{2}}) in {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}U}.111Note that it’s not necessary to make the function {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha} total or onto. Monotonicity also constrains possible flows between classes of the two domains, once certain important flows between certain classes have been identified (see Fig. 2). Moreover, since monotone functions are closed under composition, one can chain them to create secure unidirectional information flow connections through a series of administrative domains. Monotonicity is a basic principle adopted for information flow analyses, e.g. [13].
However, when there is “blowback” of information, mere monotonicity is inadequate for ensuring SIF. Consider the bidirectional flow situation in Fig. 4, where data return to the original domain. Monotonicity of both functions {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}:{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}C}\rightarrow{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}U} and {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}:{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}U}\rightarrow{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}C} does not suffice for security because the composition {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}\circ{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha} may not be non-decreasing. In Fig. 4, both {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha} and {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma} are monotone but their composition can lead to information leaking from a higher class, e.g., College Principal, to a lower class, e.g., Faculty within {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}C} — an outright violation of the college’s security policy. Similarly, composition {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}\circ{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma} may lead to violation of the University’s security policy.
Requirements.
We want to ensure that any “round-trip” flow of information, e.g., from a domain {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L} to {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M} and back to {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L}, is a permitted flow in the lattice {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L}, from where the data originated. Thus we require the following (tersely stated) “security conditions” SC1 and SC2 on {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}:{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L}\rightarrow{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M} and {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}:{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M}\rightarrow{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L}, which preclude any violation of the security policies of both the administrative domains (see Fig. 5):
[TABLE]
We also desire precision, based on a principle of least privilege escalation — if data are exchanged between the two domains without any computation done on them, then the security level should not be needlessly raised. Precision is important for meaningful and useful analyses.
[TABLE]
Further, if the data were to go back and forth between two domains more than once, the security classes to which data belong should not become increasingly restrictive after consecutive bidirectional data sharing (See Fig. 4, which shows monotone functions that keep climbing up to the top). This convergence requirement may be stated informally as conditions CC1 and CC2, requiring fixed points for the compositions {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}\circ{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha} and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}\circ{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}. Since security lattices are finite, CC1 and CC2 necessarily hold – such fixed points exist, though perhaps only at the topmost elements of the lattice. We would therefore desire a stronger requirement, where fixed points are reached as low in the orderings as possible.
Galois connections aren’t the answer.
Any discussion on a pair of partial orders linked by a pair of monotone functions suggests the notion of a Galois connection, an elegant and ubiquitous mathematical structure that finds use in computing, particularly in static analyses. However, Galois connections are not the appropriate structure for bidirectional informational flow control.
Let {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L} and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M} be two complete security class lattices, and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}:{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L}\rightarrow{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M} and {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}:{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M}\rightarrow{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L} be two monotone functions such that ({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha},{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M}) forms a Galois connection. Recall that a Galois connection satisfies the condition
[TABLE]
So in a Galois connection we have {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m_{1}}))~{}{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\sqsubseteq^{\prime}}~{}{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m_{1}}\iff{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m_{1}})~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\sqsubseteq}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m_{1}}). Since {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m_{1}})~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\sqsubseteq}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m_{1}}) holds trivially, we get {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m_{1}}))~{}{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\sqsubseteq^{\prime}}~{}{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m_{1}}. If {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m_{1}}))~{}{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\neq^{\prime}}~{}{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m_{1}} then {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m_{1}}))~{}{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\sqsubset^{\prime}}~{}{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m_{1}} (strictly), which would violate secure flow requirement SC2. Fig. 7 illustrates such a situation.
Why not Galois insertions?
Now suppose {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L} and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M} are two complete security class lattices, and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}:{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L}\rightarrow{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M} and {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}:{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M}\rightarrow{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L} be two monotone functions such that ({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha},{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M}) forms a Galois insertion. Then the flow of information permitted by {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha} and {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma} is guaranteed to be secure. However, Galois insertions mandate conditions on the definitions of functions {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha} and {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma} that are much too strong, i.e.,
- •
{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}:{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M}\rightarrow{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L} is injective, i.e., \forall{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m_{1},m_{2}}\in{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M}:{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m_{1}})~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}=}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m_{2}})\implies{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m_{1}}={\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m_{2}}
- •
{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}:{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L}\rightarrow{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M} is surjective, i.e., \forall{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m_{1}}\in{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M},\exists{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l_{1}}\in{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L}:{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l_{1}})={\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m_{1}}.
Typically data are shared only from a few security classes of any organisation. Organisations rarely make public their entire security class structure and permitted flow policies. Organisations also typically do not want any external influences on some subsets of its security classes. Thus, if not all elements of {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M} are transfer classes, it may be impossible to define a Galois insertion ({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha},{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M}) because we cannot force {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha} to be surjective.
Lagois Connections.
Further, the connection we seek to make between two domains should allow us to transpose them. Fortunately there is an elegant structure, i.e., Lagois Connections [16], which exactly satisfies this as well as the requirements of security and bidirectional sharing (SC1, SC2, PC1, PC2, CC1 and CC2). They also conveniently generalise Galois Insertions.
Definition 1 (Lagois Connection [16])
If L=({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L},{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\sqsubseteq}) and M=({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\sqsubseteq^{\prime}}) are two partially ordered sets, and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}:{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L}\rightarrow{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M} and {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}:{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M}\rightarrow{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L} are order-preserving functions, then we call the quadruple ({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha},{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M}) an increasing Lagois connection, if it satisfies the following properties:
[TABLE]
LC3 ensures that {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}c_{1}})) is the least upper bound of all security classes in {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}C} that are mapped to the same security class, say {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}u_{1}}={\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}c_{1}}) in {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}U}.
The main result of this section is that if the negotiated monotone functions {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha} and {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma} form a Lagois connection between the security lattices {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L} and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M}, then information flows permitted are secure and precise.
Theorem 2.1
Let {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L} and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M} be two complete security class lattices, {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}:{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L}\rightarrow{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M} and {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}:{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M}\rightarrow{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L} be two monotone functions. Then the flow of information permitted by {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}, {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma} satisfies conditions SC1, SC2, PC1, PC2, CC1 and CC2 if ({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha},{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M}) is an increasing Lagois connection.
Proof
Condition SC1 holds because if {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l_{1}})~{}{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\sqsubseteq^{\prime}}~{}{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m_{2}}, by monotonicity of {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}, {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l_{1}}))~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\sqsubseteq}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m_{2}}). But by LC1, {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l_{1}}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\sqsubseteq}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l_{1}})). So {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l_{1}}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\sqsubseteq}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m_{2}}). (A symmetric argument holds for SC2.) Conditions PC1 and PC2 are shown in Proposition 3.7 of [16]. Conditions CC1 and CC2 hold since the compositions {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}\circ{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha} and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}\circ{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma} are closure operators, i.e., idempotent, extensive, order-preserving endo-functions on {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L} and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M}.
In fact, Lagois connections ensure that information in a security class in the original domain remains accessible even after doing a round-trip from the other domain (Proposition 3.8 in [16]):
[TABLE]
We list various propositions about Lagois connections, which illustrate some of their important properties. In particular, the two functions {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma} and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha} uniquely determine each other. Moreover, there are largest members of their pre-images, which act as representatives for the equivalence classes of the equivalence relations {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\thicksim_{M}} and {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\thicksim_{L}} induced by these functions. Further, since our security domains are complete lattices, these distinguished points are closed under meets.
Proposition 1 (Proposition 3.7 in [16])
Let ({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha},{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M}) be a Lagois connection and let {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m}\in{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}[{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L}] and {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l}\in{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}[{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M}]. The {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}^{-1}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m}) has a largest member, which is {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m}), and {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}^{-1}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l}) has a largest member, which is {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l}).
This means that for all {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m}\in{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}[{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L}] and {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l}\in{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}[{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M}], {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m}) and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l}) exist, and are defined by largest members in their pre-image. Also, the images {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}[{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M}] and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}[{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L}] are isomorphic lattices.
{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M^{*}}={\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}[{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}[{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M}]]={\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}[{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L}] defines a system of representatives for {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\thicksim_{M}}. Then, {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m^{\prime}})) is the representative of the equivalence class [{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m^{\prime}}] of {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m^{\prime}} that lies in {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M^{*}}, called budpoint, such that,
[TABLE]
Symmetrically, {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L^{*}}={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}[{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}[{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L}]]={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}[{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M}] defines a system of representatives for {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\thicksim_{L}}.
Proposition 2 (Proposition 3.9 in [16])
If ({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha},{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M}) is a Lagois connection, then the functions {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha} and {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma} uniquely determine each other; in fact
[TABLE]
Proposition 3 (Proposition 3.11 in [16])
If ({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha},{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M}) is a Lagois connection and {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}A}\subseteq{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}[{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M}], then
the meet of {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}A} in {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}[{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M}] exists if and only if the meet of {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}A} in {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L} exists, and whenever either exists, they are equal. 2. 2.
the join {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\hat{a}} of {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}A} in {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}[{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M}] exists if the join {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\check{a}} of {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}A} in {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L} exists, and in this case {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\hat{a}}={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\check{a}}))
3 An Operational Model
3.1 Computational Model.
Let us consider two different organisations {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L} and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M} that want to share data with each other. We start with the assumptions that the two domains comprise storage objects {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}Z} and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}Z^{\prime}} respectively, which are manipulated using their own sets of atomic transactional operations, ranged over by {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}t} and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}t^{\prime}} respectively. We further assume that these transactions within each domain are internally secure with respect to their flow models, and have no insecure or interfering interactions with the environment. Thus, we are agnostic to the level of abstraction of the systems we aim to connect securely, and since our approach treats the application domains as “black boxes”, it is readily adaptable to any level of discourse (language, system, OS, database) found in the security literature.
We extend these operations with a minimal set of operations to transfer data between the two domains. To avoid any concurrency effects, interference or race conditions arising from inter-domain transfer, we augment the storage objects of both domains with a fresh set of export and import variables into/from which the data of the domain objects can be copied atomically. We designate these sets {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}X},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}X^{\prime}} as the respective export variables, and {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}Y},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}Y^{\prime}} as the respective import variables, with the corresponding variable instances written as {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}x_{i}}, {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}x_{i}^{\prime}} and {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}y_{i}}, {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}y_{i}^{\prime}}. These export and import variables form mutually disjoint sets, and are distinct from any extant domain objects manipulated by the applications within a domain. These variables are used exclusively for transfer, and are manipulated atomically. We let {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w_{i}} range over all variables in {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}N}~{}=~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}Z}\cup{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}X}\cup{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}Y} (respectively {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}w_{i}^{\prime}} over {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}N^{\prime}}~{}=~{}{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}Z^{\prime}}\cup{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}X^{\prime}}\cup{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}Y^{\prime}}). Domain objects are copied to export variables and from import variables by special operations {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}rd}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z},{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}y}) and {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}wr}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}x},{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z}) (and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}rd^{\prime}}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}z^{\prime}},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}y^{\prime}}) and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}wr^{\prime}}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}x^{\prime}},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}z^{\prime}}) in the other domain). We assume atomic transfer operations (trusted by both domains) that copy data from the export variables of one domain to the import variables of the other domain as the only mechanism for inter-domain flow of data. Let “phrase” denote a command in either domain or a transfer operation, and let be any (empty or non-empty) sequence of phrases.
[TABLE]
A store (typically {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu},{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\mu^{\prime}},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\nu^{\prime}}) is a finite-domain function from variables to a set of values (not further specified). We write, e.g., {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w}) for the contents of the store {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu} at variable {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w}, and {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu}[{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w}:={\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\mu^{\prime}}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}w^{\prime}})] for the store that is the same as {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu} everywhere except at variable {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w}, where it now takes value {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\mu^{\prime}}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}w^{\prime}}).
The rules specifying execution of commands are given in Fig. 8. Assuming the specification of intradomain transactions of the form {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu}\vdash{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}t}\implies{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu} and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\mu^{\prime}}\vdash{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}t^{\prime}}\implies{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\nu^{\prime}}, our rules allow us to specify judgments of the form \langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\mu^{\prime}}\rangle\vdash p\implies\langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\nu^{\prime}}\rangle for phrases, and (the reflexive-transitive closure) for sequences of phrases. Note that phrase execution occurs atomically, and the intra-domain transactions, as well as copying to and from the export/import variables affect the store in only one domain, whereas the atomic transfer is only between export variables of one domain and the import variables of the other.
3.2 Typing Rules
Let the two domains have the respective different IFMs:
[TABLE]
such that the flow policies in both are defined over different sets of security classes {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}SC} and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}SC^{\prime}}.222Without loss of generality, we assume that {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}SC}\cap{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}SC^{\prime}}=\emptyset, since we can suitably rename security classes.
The (security) types of the core language are as follows.
Metavariables {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l} and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m^{\prime}} range over the sets of security classes, {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}SC} and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}SC^{\prime}} respectively, which are partially ordered by {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\sqsubseteq} and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\sqsubseteq^{\prime}}. A type assignment {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda} is a finite-domain function from variables {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}N} to {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}SC} (respectively, {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\lambda^{\prime}} from {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}N^{\prime}} to {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}SC^{\prime}}). The important restriction we place on {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda} and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\lambda^{\prime}} is that they map export and import variables {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}X},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}X},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}Y^{\prime}},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}Y} only to points in the security lattices {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}SC} and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}SC^{\prime}} respectively which are in the domains of {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma} and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}, i.e., these points participate in the Lagois connection. Intuitively, a variable mapped to security class {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l} can store information of security class {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l} or lower. The type system works with respect to given type assignment. Given the security level, e.g., {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l}, the typing rules track for each command within that domain whether all written-to variables in that domain are of security classes “above” {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l}, and additionally for transactions within a domain, they ensure “simple security”, i.e., that all variables which may have been read belong to security classes “below” {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l}. We assume for the transactions within a domain, e.g., {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L}, we have a type system that will give us judgments of the form {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}\vdash{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}c}:{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l}. The novel extension of our approach is to extend this framework to work over two connected domains, i.e., given implicit security levels of the contexts in the respective domains. Cross-domain transfers will require pairing such judgments, and thus our type systems will have judgments of the form
[TABLE]
We introduce a syntax-directed set of typing rules for the core language, given in Fig. 9. In many of the rules, the type for one of the domains is not constrained by the rule, and so any suitable type may be chosen as determined by the context, e.g., {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m^{\prime}} in the rules Tt, Trd, Twr and {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}TT_{RL}}, and both {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l} and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m^{\prime}} in Com0.
For transactions e.g., {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}t} entirely within domain {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L}, the typing rule Tt constrains the type in the left domain to be at a level {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l} that dominates all variables read in {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}t}, and which is dominated by all variables written to in {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}t}, but places no constraints on the type {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m^{\prime}} in the other domain {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M}. In the rule Trd, since a value in import variable {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}y} is copied to the variable {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z}, we have {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}y})~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\sqsubseteq}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z}), and the type in the domain {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L} is {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z}) with no constraint on the type {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m^{\prime}} in the other domain. Conversely, in the rule Twr, since a value in variable {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z} is copied to the export variable {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}x}, we have {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z})~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\sqsubseteq}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}x}), and the type in the domain {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L} is {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}x}) with no constraint on the type {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m^{\prime}} in the other domain. In the rule {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}TT_{RL}}, since the contents of a variable {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}x^{\prime}} in domain {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M} are copied into a variable {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}y} in domain {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L}, we require {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\lambda^{\prime}}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}x^{\prime}}))~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\sqsubseteq}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}y}), and constrain the type in domain {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L} to {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}y}). The constraint in the other domain is unimportant (but for the sake of convenience, we peg it at {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\lambda^{\prime}}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}x^{\prime}})). Finally, for the types of sequences of phrases, we take the meets of the collected types in each domain respectively, so that we can guarantee that no variable of type lower than these meets has been written into during the sequence. Note that Proposition 3 ensures that these types have the desired properties for participating in the Lagois connection.
3.3 Soundness
We now establish soundness of our scheme by showing a non-interference theorem with respect to operational semantics and the type systems built on the security lattices. This theorem may be viewed as a conservative adaptation (to a minimal secure data transfer framework in a Lagois-connected pair of domains) of the main result of Volpano et al [23].
We assume that underlying base transactional languages in each of the domains have the following simple property (stated for {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L}, but an analogous property is assumed for {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M}): Within each transaction {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}t}, for each assignment of an expression {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}e} to any variable {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z}, the following holds: If {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu}, {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu} are two stores such that for all {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w}\in vars({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}e}), we have {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w})={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w}), then after executing the assignment, we will get {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z})={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z}). That is, if two stores are equal for all variables appearing in the expression {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}e}, then the value assigned to the variable {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z} will be the same. This assumption plays the rôle of “Simple Security” of expressions in [23] in the proof of the main theorem. The type system plays the rôle of “Confinement”. We start with two obvious lemmas about the operational semantics, namely preservation of domains, and a “frame” lemma:
Lemma 1 (Domain preservation)
If \langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\mu^{\prime}}\rangle\vdash s\Rightarrow^{*}\langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu_{1}},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\mu_{1}^{\prime}}\rangle, then dom({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu})=dom({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu_{1}}), and dom({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\mu^{\prime}})=dom({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\mu_{1}^{\prime}}).
Proof
By induction on the length of the derivation of \langle\mu,{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\mu^{\prime}}\rangle\vdash s\Rightarrow^{*}\langle\mu_{1},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\mu_{1}^{\prime}}\rangle.
Lemma 2 (Frame)
If \langle\mu,{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\mu^{\prime}}\rangle\vdash s\Rightarrow^{*}\langle\mu_{1},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\mu_{1}^{\prime}}\rangle,w\in dom(\mu)\cup dom({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\mu^{\prime}}), and is not assigned to in , then {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu}(w)={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu_{1}}(w) and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\mu^{\prime}}(w)={\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\mu_{1}^{\prime}}(w).
Proof
By induction on the length of the derivation of \langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\mu^{\prime}}\rangle\vdash s\Rightarrow^{*}\langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu_{1}},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\mu_{1}^{\prime}}\rangle.
The main result of the paper assumes an “adversary” that operates at a security level {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l} in domain {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L} and at security level {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m^{\prime}} in domain {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M}. Note however, that these two levels are interconnected by the monotone functions {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}:{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L}\rightarrow{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M} and {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}:{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M}\rightarrow{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L}, since these levels are connected by the ability of information at one level in one domain to flow to the other level in the other domain.
Theorem 3.1 (Type Soundness)
Suppose {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m^{\prime}} are the “adversarial” type levels in the respective domains, which satisfy the condition {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l}={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m^{\prime}}) and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m^{\prime}}={\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l}). Let
- (a)
\langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\lambda^{\prime}}\rangle\vdash s:\langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l_{0}},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m_{0}^{\prime}}\rangle; 2. (b)
\langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\mu^{\prime}}\rangle\vdash s\Rightarrow^{*}\langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu_{f}},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\mu_{f}^{\prime}}\rangle; 3. (c)
\langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\nu^{\prime}}\rangle\vdash s\Rightarrow^{*}\langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu_{f}},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\nu_{f}^{\prime}}\rangle; 4. (d)
dom({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu})=dom({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu})=dom({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda})* and dom({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\mu^{\prime}})=dom({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\nu^{\prime}})=dom({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\lambda^{\prime}});* 5. (e)
{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w})={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w})* for all {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w} such that {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w})~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\sqsubseteq}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l}, and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\mu^{\prime}}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}w^{\prime}})={\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\nu^{\prime}}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}w^{\prime}}) for all {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}w^{\prime}} such that {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\lambda^{\prime}}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}w^{\prime}})~{}{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\sqsubseteq^{\prime}}~{}{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m^{\prime}}.*
Then {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu_{f}}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w})={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu_{f}}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w}) for all {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w} such that {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w})~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\sqsubseteq}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l}, and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\mu_{f}^{\prime}}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}w^{\prime}})={\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\nu_{f}^{\prime}}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}w^{\prime}}) for all {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}w^{\prime}} such that {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\lambda^{\prime}}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}w^{\prime}})~{}{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\sqsubseteq^{\prime}}~{}{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m^{\prime}}.
Proof
By induction on the length of sequence . The base case is vacuously true. We now consider a sequence . \langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\mu^{\prime}}\rangle\vdash s_{1}\Rightarrow^{*}\langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu_{1}},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\mu_{1}^{\prime}}\rangle and \langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu_{1}},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\mu_{1}^{\prime}}\rangle\vdash p\Rightarrow\langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu_{f}},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\mu_{f}^{\prime}}\rangle and \langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\nu^{\prime}}\rangle\vdash s_{1}\Rightarrow^{*}\langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu_{1}},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\nu_{1}^{\prime}}\rangle and \langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu_{1}},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\nu_{1}^{\prime}}\rangle\vdash p\Rightarrow\langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu_{f}},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\nu_{f}^{\prime}}\rangle By induction hypothesis applied to , we have {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu_{1}}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w})={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu_{1}}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w}) for all {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w} such that {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w})}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\sqsubseteq}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l}, and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\mu_{1}^{\prime}}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}w^{\prime}})={\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\nu_{1}^{\prime}}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}w^{\prime}}) for all {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}w^{\prime}} such that {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\lambda^{\prime}}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}w^{\prime}})~{}{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\sqsubseteq^{\prime}}~{}{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m^{\prime}}.
Let \langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\lambda^{\prime}}\rangle\vdash s_{1}:\langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l_{s}},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m_{s}^{\prime}}\rangle, and \langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\lambda^{\prime}}\rangle\vdash p:\langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l_{p}},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m_{p}^{\prime}}\rangle. We examine four cases for (the remaining cases are symmetrical).
Case is {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}t}: Consider any {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w} such that {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w})~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\sqsubseteq}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l}. If {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w}\in{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}X}\cup{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}Y} (i.e., it doesn’t appear in {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}t}), or if {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w}\in{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}Z} but is not assigned to in {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}t}, then by Lemma 2 and the induction hypothesis, {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu_{f}}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w})={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu_{1}}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w})={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu_{1}}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w})={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu_{f}}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w}).
Now suppose {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z} is assigned to in {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}t}. From the condition \langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\lambda^{\prime}}\rangle\vdash p:\langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l_{p}},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m_{p}^{\prime}}\rangle, we know that for all {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z_{1}} assigned in {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}t}, {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l_{p}}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\sqsubseteq}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z_{1}}) and for all {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z_{1}} read in {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}t}, {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z_{1}})~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\sqsubseteq}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l_{p}}. Now if {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}~{}\sqsubseteq}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l_{p}}, then since in {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}t} no variables {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z_{2}} such that {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z_{2}})~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\sqsubseteq}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l} are assigned to. Therefore by Lemma 2, {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu_{f}}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w})={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu_{1}}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w})={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu_{1}}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w})={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu_{f}}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w}), for all {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w} such that {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}w})~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\sqsubseteq}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l}.
If {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l_{p}}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}~{}\sqsubseteq}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l}, then for all {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z_{1}} read in {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}t}, {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z_{1}})~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\sqsubseteq}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l_{p}}. Therefore, by assumption on transaction {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}t}, if any variable {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z} is assigned an expression {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}e}, since {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu_{1}}, {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu_{1}} are two stores such that for all {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z_{1}}\in{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}Z_{e}}=vars({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}e}), {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu_{1}}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z_{1}})={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu_{1}}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z_{1}}), the value of {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}e} will be the same. By this simple security argument, after the transaction {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}t}, we have {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu_{f}}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z})={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu_{f}}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z}). Since the transaction happened entirely and atomically in domain {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}L}, we do not have to worry ourselves with changes in the other domain {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}M}, and do not need to concern ourselves with the adversarial level {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m^{\prime}}.
Case is {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}rd}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z},{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}y}): Thus \langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\lambda^{\prime}}\rangle\vdash{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}rd}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z},{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}y}):\langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z}),{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m^{\prime}}\rangle, which means {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}y})~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\sqsubseteq}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z}). If {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\sqsubseteq}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z}), there is nothing to prove (Lemma 2, again). If {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z})~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\sqsubseteq}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l}, then since by I.H., {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu_{1}}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}y})={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu_{1}}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}y}), we have {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu_{f}}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z})={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu_{1}}[{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z}:={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu_{1}}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}y})]({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z})={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu_{1}}[{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z}:={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu_{1}}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}y})]({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z})={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu_{f}}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z}).
Case is {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}wr}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}x},{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z}): Thus \langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\lambda^{\prime}}\rangle\vdash{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}wr}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}x},{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z}):\langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}x}),{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m^{\prime}}\rangle, which means {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z})~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\sqsubseteq}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}x}). If {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\sqsubseteq}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}x}), there is nothing to prove (Lemma 2, again). If {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}x})~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\sqsubseteq}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l}, then since by I.H., {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu_{1}}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z})={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu_{1}}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z}), we have {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu_{f}}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}x})={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu_{1}}[{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}x}:={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu_{1}}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z})]({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}x})={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu_{1}}[{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}x}:={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu_{1}}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}z})]({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}x})={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu_{f}}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}x}).
Case is T_{RL}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}y},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}x^{\prime}}): So \langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\lambda^{\prime}}\rangle\vdash T_{RL}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}y},{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}x^{\prime}}):\langle{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}y}),{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\lambda^{\prime}}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}x^{\prime}})\rangle, and {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\lambda^{\prime}}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}x^{\prime}}))~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\sqsubseteq}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}y}). If {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\sqsubseteq}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}y}), there is nothing to prove (Lemma 2, again). If {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\lambda}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}y})~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\sqsubseteq}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l}, then by transitivity, {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\lambda^{\prime}}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}x^{\prime}}))~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\sqsubseteq}~{}{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l}. By monotonicity of {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}: {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\lambda^{\prime}}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}x^{\prime}})))~{}{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\sqsubseteq^{\prime}}~{}{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l})~{}=~{}{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m^{\prime}} (By our assumption on {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}l} and {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m^{\prime}}). But by LC2, {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\lambda^{\prime}}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}x^{\prime}})~{}{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\sqsubseteq^{\prime}}~{}{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\alpha}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\gamma}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\lambda^{\prime}}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}x^{\prime}}))). So by transitivity, {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\lambda^{\prime}}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}x^{\prime}})~{}{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\sqsubseteq^{\prime}}~{}{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}m^{\prime}}. Now, by I.H., since {\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\mu_{1}^{\prime}}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}x^{\prime}})={\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\nu_{1}^{\prime}}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}x^{\prime}}), we have {\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu_{f}}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}y})={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\mu_{1}}[{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}y}:={\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\mu_{1}^{\prime}}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}x^{\prime}})]({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}y})={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu_{1}}[{\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}y}:={\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}\nu_{1}^{\prime}}({\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}x^{\prime}})]({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}y})={\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}\nu_{f}}({\color[rgb]{0,0.44,0.57}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.44,0.57}\pgfsys@color@cmyk@stroke{0.98}{0.13}{0}{0.43}\pgfsys@color@cmyk@fill{0.98}{0.13}{0}{0.43}y}).
4 Related Work
The notion of Lagois connections [16] has surprisingly not been employed much in computer science. The only cited use of this idea seems to be the work of Huth [11] in establishing the correctness of programming language implementations. To our knowledge, our work is the only one to propose their use in secure information flow control.
Abstract Interpretation and type systems [5] have been used in secure flow analyses, e.g., [4, 3] and [24], where security types are defined using Galois connections employing, for instance, a standard collecting semantics. Their use of two domains, concrete and abstract, with a Galois connection between them, for performing static analyses within a single domain should not be confused with our idea of secure connections between independently-defined security lattices of two organisations.
There has been substantial work on SIF in a distributed setting at the systems level. DStar [26] for example, uses sets of opaque identifiers to define security classes. The DStar framework extends a particular DIFC model [12, 25] for operating systems to a distributed network. The only partial order that is considered in DStar’s security lattice is subset inclusion. So it is not clear if DStar can work on general IFC mechanisms such as FlowCaml [19], which can use any partial ordering. Nor can it express the labels of JiF [17] or Fabric [13] completely. DStar allows bidirectional communication between processes and only if and , i.e., if there is an order-isomorphism between the labels. Our motivating examples indicate such a requirement is far too restrictive for most practical arrangements for data sharing between organisations.
Fabric [14, 13] adds trust relationships directly derived from a principal hierarchy to support federated systems with mutually distrustful nodes and allows dynamic delegation of authority.
Most of the previous DIFC mechanisms [17, 25, 12, 8, 20, 2] including Fabric are susceptible to the vulnerabilities illustrated in our motivating examples, which we will mention in the concluding discussion.
5 Conclusions and Future Work
Our work is similar in spirit to Denning’s motivation for proposing lattices, namely to identify a simple and mathematically elegant structure in which to frame the construction of scalable secure information flow in a modular manner that preserved the autonomy of the individual organisations. From the basic requirements, we identified the elegant theory of Lagois connections as an appropriate structure. Lagois connections provide us a way to connect the security lattices of two (secure) systems in a manner that does not expose their entire internal structure and allows us to reason only in terms of the interfaced security classes. We believe that this framework is also applicable in more intricate information flow control formulations such as decentralised IFC [18] and models with declassification, as well as formulations with data-dependent security classes [15]. We intend to explore these aspects in the future.
In this paper, we also proposed a minimal operational model for the transfer of data between the two domains. This formulation is spare enough to be adaptable at various levels of abstraction (programming language, systems, databases), and is intended to illustrate that the Lagois connection framework can conserve security, using non-interference as the semantic notion of soundness. The choice of non-interference and the use of a type system in the manner of Volpano et al. [23] was to illustrate in familiar terms how those techniques (removed from a particular language formulation) could be readily adapted to work in the context of secure connections between lattices. In this exercise, we made suitable assumptions of atomicity and the use of fresh variables for communication, so as to avoid usual sources of interference. We believe that the Lagois connection framework for secure flows between systems is readily adaptable for notions of semantic correctness other than non-interference, though that is an exercise for the future.
In the future we intend to explore how the theory of Lagois connections constitutes a robust framework that can support the discovery, decomposition, update and maintenance of secure MoUs for exchanging information. In this paper, we concerned ourselves only with two domains and bidirectional information exchange. Compositionality of Lagois connections allows these results to extend to chaining connections across several domains. In the future, we also intend to explore how one may secure more complicated information exchange arrangements than merely chains of bidirectional flow.
We close this discussion with a reminder of why it is important to have a framework in which secure flows should be treated in a modular and autonomous manner. Consider Myer’s DIFC model described in [18], where a principal can delegate to others the capacity to act on its behalf. We believe that this notion does not scale well to large, networked systems since a principal may repose different levels of trust in the various hosts in the network. For this reason, we believe that frameworks such as Fabric [14, 13] may provide more power than mandated by a principle of least privilege. In general, since a principal rarely vests unqualified trust in another in all contexts and situations, one should confine the influence of the principals possessing delegated authority to only specific domains. A mathematical framework that can deal with localising trust and delegation of authority in different domains and controlling the manner in which information flow can be secured deserves a deeper study. We believe that algebraic theories such as Lagois connections can provide the necessary structure for articulating these concepts.
Acknowledgments.
The second author thanks Deepak Garg for insightful discussions on secure information flow. Part of the title is stolen from E.M. Forster.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] Boudol, G.: Secure Information Flow as a Safety Property. In: Formal Aspects in Security and Trust, 5th International Workshop, FAST 2008, Malaga, Spain, October 9-10, 2008, Revised Selected Papers. pp. 20–34 (2008)
- 2[2] Cheng, W., Ports, D.R.K., Schultz, D.A., Popic, V., Blankstein, A., Cowling, J.A., Curtis, D., Shrira, L., Liskov, B.: Abstractions for Usable Information Flow Control in Aeolus. In: 2012 USENIX Annual Technical Conference, Boston, MA, USA, June 13-15, 2012. pp. 139–151 (2012)
- 3[3] Cortesi, A., Ferrara, P., Halder, R., Zanioli, M.: Combining symbolic and numerical domains for information leakage analysis. Trans. Computational Science 31 , 98–135 (2018)
- 4[4] Cortesi, A., Ferrara, P., Pistoia, M., Tripp, O.: Datacentric Semantics for Verification of Privacy Policy Compliance by Mobile Applications. In: Verification, Model Checking, and Abstract Interpretation - 16th International Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015. Proceedings. pp. 61–79 (2015)
- 5[5] Cousot, P.: Types as Abstract Interpretations. In: Conference Record of POPL’97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, Paris, France, 15-17 January 1997. pp. 316–331 (1997)
- 6[6] Deng, S., Gümüsoglu, D., Xiong, W., Gener, Y.S., Demir, O., Szefer, J.: Sec Chisel: Language and Tool for Practical and Scalable Security Verification of Security-Aware Hardware Architectures. IACR Cryptology e Print Archive 2017 , 193 (2017), http://eprint.iacr.org/2017/193
- 7[7] Denning, D.E.: A Lattice Model of Secure Information Flow. Commun. ACM 19 (5), 236–243 (1976)
- 8[8] Efstathopoulos, P., Krohn, M.N., Vandebogart, S., Frey, C., Ziegler, D., Kohler, E., Mazières, D., Kaashoek, M.F., Morris, R.T.: Labels and event processes in the Asbestos operating system. In: Proceedings of the 20th ACM Symposium on Operating Systems Principles 2005, SOSP 2005, Brighton, UK, October 23-26, 2005. pp. 17–30 (2005)