pith. sign in

arxiv: 2606.27059 · v1 · pith:57TTOE66new · submitted 2026-06-25 · 💻 cs.CR

Type-based information flow analysis for π-calculus with a dynamically extensible security lattice

Yukihiro Oda , Eijiro Sumii This is my paper

Pith reviewed 2026-06-26 03:47 UTC · model grok-4.3

classification 💻 cs.CR
keywords type systeminformation flowpi-calculussecurity latticedynamic extensionnon-interferencebisimulation
0
0 comments X

The pith

The type system for pi-calculus allows new security levels to be created and added to the lattice during program execution.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper presents an extension to Kobayashi's type-based information flow analysis for the pi-calculus. The extension supports dynamic creation of security levels that can be inserted into the security lattice at runtime. A reader would care because this enables modeling more realistic systems where security classifications can change or be introduced as the system runs. The key is maintaining the non-interference guarantee expressed as bisimulation equivalence despite these changes.

Core claim

We develop a type system for secure information flow where new security levels can be created and inserted into the security lattice dynamically, i.e., even in the middle of an execution of a system. Our system is formalized by extending Kobayashi's type-based secure information flow analysis for Milner's pi-calculus, which is one of the most expressive models supporting both sequential and concurrent computations, with concise syntax, reduction-based semantics, and bisimulation equivalence as a robust formalization of secrecy as non-interference. The development required careful treatment of extensions of lattices themselves as well as deliberate generalization from the simple 2-element lat

What carries the argument

The extended type system that tracks information flow while handling dynamic lattice insertions and preserving bisimulation-based non-interference.

If this is right

  • New security levels can be created and inserted into the lattice mid-execution.
  • Non-interference defined as bisimulation continues to hold after lattice extensions.
  • The type system applies to pi-calculus processes with evolving security policies.
  • Generalization beyond the fixed High-Low lattice is achieved while retaining the original guarantees.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The method could be tested on examples involving repeated dynamic level creations to check scalability of the extension rules.
  • Similar dynamic lattice handling might transfer to other process calculi that use bisimulation for secrecy.
  • This opens the possibility of verifying systems where security domains are allocated at runtime rather than fixed in advance.

Load-bearing premise

The careful treatment of lattice extensions and generalization from the 2-element lattice preserves the non-interference property from the original Kobayashi system.

What would settle it

A concrete execution in which a new security level is created, high information flows through it, and a low observer can distinguish the resulting behaviors via bisimulation.

Figures

Figures reproduced from arXiv: 2606.27059 by Eijiro Sumii, Yukihiro Oda.

Figure 1
Figure 1. Figure 1: Typing rules The typing rules other than (T-NewSec) are similar to previous ones [6] except that they are all parame￾terized by the general lattice of secrecy levels L. The second premise L v  ˜l1 < νl0 < ˜l2  L in (T-NewSec) ensures safe extension thanks to our previous definitions on lattices (Definition 2.3 and Definition 2.5). The “side” condition m ≤L ˜l1, ˜l2, which is more subtle, guarantees that … view at source ↗
Figure 2
Figure 2. Figure 2: An example of typing (rule names and trailing 0 are omitted), where L′ = ((⊥) < νl < (⊤))L Lemma 4.2 (Structural preorder preserves typing). If Γ k L ▷m P is l-securely derivable and P  P 0 , then Γ k L ▷m P 0 is also l-securely derivable. Proof. See Appendix D.2. Definition 4.3 (Substitution on type environment). For a type environment Γ, variables x˜, and values v˜ with {x˜} ∩ {v˜} = ∅, we define a type… view at source ↗
Figure 3
Figure 3. Figure 3: Substitution on type environment depth [ ](1) = depth [ ](2) = 0 depth(P) = 0 if [ ](1) and [ ](2) do not occur in P depth(C0 | C1) = depth(C0) + depth(C1) depth(x!˜v.C0) = depth(C0) + 1 depth(x?˜y.C0) = depth(C0) + 1 depth(∗C0) = depth(C0) depth((νx : ξ)C0) = depth(C0) depth˜l0 < νl < ˜l1  C0  = depth(C0) + 1 depth(if v then C0 else C1) = depth(C0) + depth(C1) [PITH_FULL_IMAGE:figures/full_fig_p0… view at source ↗
Figure 4
Figure 4. Figure 4: Depth of context A context with two holes is defined as an expression obtained from a process by replacing just two sub￾processes with [ ](1) and [ ](2). We write C [P0] (1)[P1] (2) for the process obtained by replacing [ ](1) and [ ](2) in C with P0 and P1, respectively. Definition 4.10 (Depth of context). For a context with two holes C, we inductively define the depth of C, written depth(C), as in [PITH… view at source ↗
read the original abstract

We develop a type system for secure information flow where new security levels can be created and inserted into the security lattice dynamically, i.e., even in the middle of an execution of a system. Our system is formalized by extending Kobayashi's type-based secure information flow analysis for Milner's pi-calculus, which is one of the most expressive models (or "languages") supporting both sequential and concurrent computations, with concise syntax, reduction-based semantics, and bisimulation equivalence as a robust formalization of secrecy as non-interference. The development required careful treatment of extensions of lattices themselves as well as deliberate generalization from the simple 2-element lattice (consisting of only High and Low) in the original system.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 0 minor

Summary. The paper develops a type system for secure information flow in Milner's π-calculus that supports dynamic creation and insertion of new security levels into the lattice during execution. It extends Kobayashi's prior type-based analysis (which encodes secrecy as bisimulation-based non-interference) by generalizing from a static 2-element (High/Low) lattice to handle runtime lattice extensions.

Significance. If the extension preserves the original non-interference property, the result would be a useful step toward type-based IFC for concurrent systems with evolving security policies. The explicit grounding in an existing, expressive calculus and bisimulation semantics is a strength.

major comments (1)
  1. [Abstract] Abstract: the claim that the system supports dynamic lattice extensions while preserving secrecy as bisimulation rests on 'careful treatment' of lattice operations, but no type rules, reduction semantics for lattice insertion, or proof outline are visible, preventing verification that the generalization from the 2-element lattice avoids introducing new flows.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their review. The major comment focuses on the abstract's level of detail. We respond below and note that the full manuscript contains the requested elements.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the claim that the system supports dynamic lattice extensions while preserving secrecy as bisimulation rests on 'careful treatment' of lattice operations, but no type rules, reduction semantics for lattice insertion, or proof outline are visible, preventing verification that the generalization from the 2-element lattice avoids introducing new flows.

    Authors: The abstract is a concise summary and does not include technical details such as rules or proofs, which is standard. The full manuscript defines the type rules for dynamic lattice extensions in Section 3 (generalizing Kobayashi's system), the reduction semantics for lattice insertion operations in Section 2.3, and provides a proof outline plus full non-interference argument (via bisimulation) in Section 5. The lattice operations are treated to ensure no new flows are introduced during extension. If desired, we can add one sentence to the abstract referencing these sections. revision: partial

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper presents an extension of Kobayashi's independent prior type system for pi-calculus information flow to handle dynamic lattice creation. The abstract and description frame this as a deliberate generalization from the original 2-element lattice with careful treatment of extensions, without any self-definitional equations, fitted inputs renamed as predictions, load-bearing self-citations from overlapping authors, or ansatz smuggling. The derivation chain relies on external prior work by a different author and standard bisimulation-based non-interference, making the result self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Based on abstract only; no free parameters, invented entities, or ad-hoc axioms are identifiable from the provided text.

axioms (1)
  • standard math Pi-calculus reduction semantics and bisimulation equivalence as formalization of secrecy
    The paper extends Kobayashi's system which relies on Milner's pi-calculus model.

pith-pipeline@v0.9.1-grok · 5644 in / 1123 out tokens · 60301 ms · 2026-06-26T03:47:40.811120+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

93 extracted references · 14 canonical work pages

  1. [1]

    Communications of the ACM , volume =

    D. E. Denning, “A lattice model of secure information flow,” Commun. ACM , vol. 19, no. 5, pp. 236–243, 1976. [Online]. A vailable:https://doi.org/10.1145/360051.360056

    work page doi:10.1145/360051.360056 1976

  2. [2]

    In: 1982 IEEE Symposium on Security and Privacy, 1982, pp

    J. A. Goguen and J. Meseguer, “Security policies and security models,” in 1982 IEEE Symposium on Security and Privacy, Oakland, CA, USA, April 26-28, 1982 . IEEE Computer Society, 1982, pp. 11–20. [Online]. A vailable: https://doi.org/10.1109/SP.1982.10014

    work page doi:10.1109/sp.1982.10014 1982

  3. [3]

    A sound type system for secure flow analysis,

    D. M. Volpano, C. E. Irvine, and G. Smith, “A sound type system for secure flow analysis,” J. Comput. Secur. , vol. 4, no. 2/3, pp. 167–188, 1996. [Online]. A vailable: https://doi.org/10.3233/JCS-1996-42-304

    work page doi:10.3233/jcs-1996-42-304 1996

  4. [4]

    Language-based information- flow security,

    A. Sabelfeld and A. C. Myers, “Language-based information- flow security,” IEEE J. Sel. Areas Commun. , vol. 21, no. 1, pp. 5–19, 2003. [Online]. A vailable: https://doi.org/10.1109/ JSAC.2002.806121

    arXiv 2003

  5. [5]

    The slam calculus: Programming with secrecy and integrity,

    N. Heintze and J. G. Riecke, “The slam calculus: Programming with secrecy and integrity,” in POPL ’98, Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, CA, USA, January 19-21, 1998 , D. B. MacQueen and L. Cardelli, Eds. ACM, 1998, pp. 365–377. [Online]. A vailable:https://doi.org/10.1145/268946.268976

    work page doi:10.1145/268946.268976 1998

  6. [6]

    Type-based information flow analysis for the pi-calculus,

    N. Kobayashi, “Type-based information flow analysis for the pi-calculus,” Acta Informatica , vol. 42, no. 4-5, pp. 291–347, 2005. [Online]. A vailable: https://doi.org/10.1007/ s00236-005-0179-x

    2005

  7. [7]

    A type system for lock-free processes,

    ——, “A type system for lock-free processes,” Inf. Comput. , vol. 177, no. 2, pp. 122–159, 2002. [Online]. A vailable: https://doi.org/10.1006/inco.2002.3171

    work page doi:10.1006/inco.2002.3171 2002

  8. [8]

    Milner, Communicating and mobile systems - the Pi- calculus

    R. Milner, Communicating and mobile systems - the Pi- calculus. Cambridge University Press, 1999

    1999

  9. [9]

    A calculus of mobile processes, I,

    R. Milner, J. Parrow, and D. Walker, “A calculus of mobile processes, I,” Inf. Comput. , vol. 100, no. 1, pp. 1–40, 1992. [Online]. A vailable: https://doi.org/10.1016/0890-5401(92) 90008-4

    work page doi:10.1016/0890-5401(92 1992

  10. [10]

    A calculus of mobile processes, II,

    ——, “A calculus of mobile processes, II,” Inf. Comput. , vol. 100, no. 1, pp. 41–77, 1992. [Online]. A vailable: https://doi.org/10.1016/0890-5401(92)90009-5

    work page doi:10.1016/0890-5401(92)90009-5 1992

  11. [11]

    Barbed bisimulation,

    R. Milner and D. Sangiorgi, “Barbed bisimulation,” in Automata, Languages and Programming, 19th International Colloquium, ICALP92, Vienna, Austria, July 13-17, 1992, Proceedings, ser. Lecture Notes in Computer Science, W. Kuich, Ed., vol. 623. Springer, 1992, pp. 685–695. [Online]. A vailable: https://doi.org/10.1007/3-540-55719-9_ 114

    work page doi:10.1007/3-540-55719-9_ 1992

  12. [12]

    Bisimulation through probabilistic testing,

    K. G. Larsen and A. Skou, “Bisimulation through probabilistic testing,” Inf. Comput. , vol. 94, no. 1, pp. 1–28, 1991. [Online]. A vailable: https://doi.org/10.1016/ 0890-5401(91)90030-6

    1991

  13. [13]

    Probabilistic noninterference through weak probabilistic bisimulation,

    G. Smith, “Probabilistic noninterference through weak probabilistic bisimulation,” in 16th IEEE Computer Security Foundations Workshop (CSFW-16 2003), 30 June - 2 July 2003, Pacific Grove, CA, USA . IEEE Computer Society, 2003, pp. 3–13. [Online]. A vailable: https://doi.org/10.1109/ CSFW.2003.1212701

    arXiv 2003

  14. [14]

    Back to the format: A survey on SOS for probabilistic processes,

    V. Castiglioni, R. Lanotte, and S. Tini, “Back to the format: A survey on SOS for probabilistic processes,” J. Log. Algebraic Methods Program. , vol. 137, p. 100929,

  15. [15]

    A vailable: https://doi.org/10.1016/j.jlamp

    [Online]. A vailable: https://doi.org/10.1016/j.jlamp. 2023.100929

    work page doi:10.1016/j.jlamp 2023

  16. [16]

    A spectrum of approximate probabilistic bisimulations,

    T. Spork, C. Baier, J. Katoen, J. Piribauer, and T. Quatmann, “A spectrum of approximate probabilistic bisimulations,” in 35th International Conference on Concurrency Theory, CONCUR 2024, September 9-13, 2024, Calgary, Canada , ser. LIPIcs, R. Majumdar and A. Silva, Eds., vol. 311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, pp. 37:1–37:19. [...

    work page doi:10.4230/lipics.concur.2024.37 2024

  17. [17]

    van Glabbeek (2001):The Linear Time–Branching Time Spectrum I

    R. J. van Glabbeek, “The linear time - branching time spectrum I,” in Handbook of Process Algebra , J. A. Bergstra, A. Ponse, and S. A. Smolka, Eds. North- Holland / Elsevier, 2001, pp. 3–99. [Online]. A vailable: https://doi.org/10.1016/b978-044482830-9/50019-9

    work page doi:10.1016/b978-044482830-9/50019-9 2001

  18. [18]

    The linear time - branching time spectrum II,

    ——, “The linear time - branching time spectrum II,” in CONCUR ’93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings, ser. Lecture Notes in Computer Science, E. Best, Ed., vol. 715. Springer, 1993, pp. 66–81. [Online]. A vailable:https://doi.org/10.1007/3-540-57208-2_6

    work page doi:10.1007/3-540-57208-2_6 1993

  19. [19]

    Concurrent hyperproperties,

    B. Finkbeiner and E. Olderog, “Concurrent hyperproperties,” in Theories of Programming and Formal Methods - Essays Dedicated to Jifeng He on the Occasion of His 80th Birthday, ser. Lecture Notes in Computer Science, J. P. Bowen, Q. Li, and Q. Xu, Eds., vol. 14080. Springer, 2023, pp. 211–231. [Online]. A vailable: https://doi.org/10.1007/ 978-3-031-40436-8_8

    2023

  20. [20]

    lattice,

    nLab, “lattice,” https://ncatlab.org/nlab/show/lattice, as of July 2025

    2025

  21. [21]

    P. T. Johnstone, Stone Spaces. Cambridge University Press, 1986

    1986

  22. [22]

    A generalized deadlock- free process calculus,

    E. Sumii and N. Kobayashi, “A generalized deadlock- free process calculus,” in 3rd International Workshop on High-Level Concurrent Languages, HLCL 1998, Satellite Workshop of CONCUR 1998, Nice, France, September 12, 1998 , ser. Electronic Notes in Theoretical Computer Science, U. Nestmann and B. C. Pierce, Eds., vol. 16, no. 3. Elsevier, 1998, pp. 225–247...

    work page doi:10.1016/s1571-0661(04)00144-6 1998

  23. [23]

    Linear logic,

    J. Girard, “Linear logic,” Theor. Comput. Sci. , vol. 50, pp. 1–102, 1987. [Online]. A vailable: https://doi.org/10.1016/ 0304-3975(87)90045-4

    1987

  24. [24]

    Sangiorgi and D

    D. Sangiorgi and D. Walker, The Pi-Calculus - a theory of mobile processes. Cambridge University Press, 2001

    2001

  25. [25]

    Type systems for concurrent processes: From deadlock-freedom to livelock-freedom, time-boundedness,

    N. Kobayashi, “Type systems for concurrent processes: From deadlock-freedom to livelock-freedom, time-boundedness,” in Theoretical Computer Science, Exploring New Frontiers of Theoretical Informatics, International Conference IFIP TCS 2000, Sendai, Japan, August 17-19, 2000, Proceedings , ser. Lecture Notes in Computer Science, J. van Leeuwen, O. Watanabe...

    work page doi:10.1007/3-540-44929-9_27 2000

  26. [26]

    Lemma A.4

    By ( SP-Commut) and ( SP-Par), we see P0 j P1 P 0 0 j P1 (SP-Par) P1 j P 0 0 (SP-Commut) P 0 1 j P 0 0 (SP-Par) P 0 0 j P 0 1 (SP-Commut). Lemma A.4. P0 j (P1 j P2) (P0 j P1) j P2. Proof. By ( SP-Commut), ( SP-Assoc) and ( SP-Par), we see P0 j (P1 j P2) (P1 j P2) j P0 (SP-Commut) (P2 j P1) j P0 (SP-Commut) and ( SP-Par) P2 j (P1 j P0) (SP-Assoc) P2 j (P0 ...

  27. [27]

    By ( UP-Commut) and ( UP-CongP), we see U0 j U1 U 0 0 j U1 (UP-CongP) U1 j U 0 0 (UP-Commut) U 0 1 j U 0 0 (UP-CongP) U 0 0 j U 0 1 (UP-Commut). (2) By ( UP-Commut), ( UP-Assoc) and ( UP-CongP), we see U0 j (U1 j U2) (U1 j U2) j U0 (UP-Commut) (U2 j U1) j U0 (UP-Commut) and ( UP-CongP) U2 j (U1 j U0) (UP-Assoc) U2 j (U0 j U1) (UP-Commut) and ( UP-CongP) (...

  28. [28]

    By the induction hypothesis, we have cap α(U1) capα(U 0

    We also assume U = U1 j U2 and U 0 = U 0 1 j U2. By the induction hypothesis, we have cap α(U1) capα(U 0

  29. [29]

    ( , )). Assume U =

    and ob α(U1) obα(U 0 1). Then capα(U ) = capα(U1 j U2) = min(capα(U1), capα(U2)) min(capα(U 0 1), capα(U2)) = capα(U 0 1 j U2) = capα(U 0) and obα(U ) = obα(U1 j U2) = min(obα(U1), obα(U2)) min(obα(U 0 1), obα(U2)) = obα(U 0 1 j U2) = obα(U 0). Case 7. ( UP-Rep). Assume U = U0 and U 0 = U0 j U0. Then capα(U 0) = capα( U0 j U0) = min(capα( U0), capα(U0)) =...

  30. [30]

    By the induction hypothesis, we have cap α(U0) capα(U 0

  31. [31]

    (tI ,tO) U0 = capα(U0) capα(U 0 0) = capα

    and ob α(U0) obα(U 0 0). Then capα(U ) = capα "(tI ,tO) U0 = capα(U0) capα(U 0 0) = capα "(tI ,tO) U 0 0 = capα(U 0) and obα(U ) = obα "(tI ,tO) U0 = max(tα, obα(U0)) max(tα, obα(U 0 0)) = obα "(tI ,tO) U 0 0 = obα(U 0). Case 12. ( UP-Commut "( , )). Assume U = "(tI ,tO) "(t′ I ,t′ O) U0 and U 0 = "(t′ I ,t′ O) "(tI ,tO) U0. Then capα(U ) = capα "(tI ,tO)...

  32. [32]

    By induction and Definition 3.7 (b), we see that there exists a usage U 0 0 such that U0 ! !U 0 0 and U 0 0 <: U 0

  33. [33]

    By (1) in this proposition, we have con (U 0 1)

    Since rel (U0), we have con(U 0 0). By (1) in this proposition, we have con (U 0 1). Thus, rel (U1). (3) Since it is obvious that the identity relation on closed usages satisfies all the conditions of Definition 3.7 , we have the reflexivity of the subusage relation. We show the transitivity of the subusage relation. Let R = 8 < :(U0, U1) U0 <: U1, or the...

  34. [34]

    By Definition 3.7 (b), there exists U 0 2 such that U2 !U 0 2 and U 0 2 <: U 0

  35. [35]

    By Definition 3.7 (b), there exists U 0 0 such that U0 !U 0 0 and U 0 0 <: U 0

  36. [36]

    Then, we see that there exists U 0 0 such that U0 !U 0 0 and (U 0 0, U 0

  37. [37]

    (to,tc) U < : U for a usage U and to, tc 2 N [ f1g. (8)

    2 R. (c) By Definition 3.7 (c), we have cap α(U0) capα(U2) and cap α(U2) capα(U1), for each α 2 f I, Og. Then, we have cap α(U0) capα(U1), for each α 2 fI, Og. (d) Fix α 2 f I, Og. Assume con α(U0). By Proposition 3.8 (1), we have con α(U2). Then, by Definition 3.7 (d), we have ob α(U0) obα(U2) and ob α(U2) obα(U1). Thus, ob α(U0) obα(U1). B.3. Property o...

  38. [38]

    Since FV (U0) fρg and FV (U 0

    = fρ0g. Since FV (U0) fρg and FV (U 0

  39. [39]

    Hence, (U 0 0[ρ0 7! (U0[ρ 7! U ])], U 0 0[ρ0 7! (U0[ρ 7! U 0])]) 2 R(U,U ′) 1

    = fρ0g, we have U 0 0[ρ0 7! (U0[ρ 7! U ])] = ( U 0 0[ρ0 7! U0])[ρ 7! U ] and U 0 0[ρ0 7! (U0[ρ 7! U 0])] = ( U 0 0[ρ0 7! U0])[ρ 7! U 0]. Hence, (U 0 0[ρ0 7! (U0[ρ 7! U ])], U 0 0[ρ0 7! (U0[ρ 7! U 0])]) 2 R(U,U ′) 1 . (b) To show that R(U,U ′) 1 satisfies Definition 3.7 (b), we show that if (U0[ρ 7! U ], U0[ρ 7! U 0]) 2 R(U,U ′) 1 , and U0[ρ 7! U 0] ˆV , t...

  40. [40]

    ( , )). Assume U0 =

    fρg, ˇV1 = U 0 1[ρ 7! U ], and ˆV1 = U 0 1[ρ 7! U 0]. Let ˇV = U 0 1[ρ 7! U ] j U2[ρ 7! U ]. Then, we have ˇV , ˆV 2 R(U,U ′) 1 . By ( UP-CongP) and transitivity, we see U1[ρ 7! U ] j U2[ρ 7! U ] U 0 1[ρ 7! U ] j U2[ρ 7! U ]. Case 7. ( UP-Rep). Assume U0 = U1 and ˆV = U1[ρ 7! U 0] j U1[ρ 7! U 0]. Let ˇV = U1[ρ 7! U ] j U1[ρ 7! U 0]. Then, we have U0[ρ 7! ...

  41. [41]

    ( , )). Assume U0 =

    f ρg, ˇV1 = U 0 1[ρ 7! U ], and ˆV1 = U 0 1[ρ 7! U 0]. Hence, we see ˇV = U 0 1[ρ 7! U ] j U2[ρ 7! U ] and ˆV = U 0 1[ρ 7! U 0] j U2[ρ 7! U 0]. Then, we have U0[ρ 7! U ] !ˇV and ˇV , ˆV 2 R(U,U ′) 1 . Case 3. Assume that there exist usages ˆV1 and ˆV2 such that U0[ρ 7! U 0] ˆV1, ˆV1 ! ˆV2, and ˆV2 ˆV . Since (U0[ρ 7! U ], U0[ρ 7! U 0]) 2 R(U,U ′) 1 and U0...

  42. [42]

    ( , )). Assume U =

    j U 0 2 and ˆV = U 0 0[ρ 7! W1] j (U 0 1[ρ 7! W1] j U 0 2[ρ 7! W1]). Let ˆV = U 0 0[ρ 7! W0] j (U 0 1[ρ 7! W0] j U 0 2[ρ 7! W0]). Then, we have U [ρ 7! W0] ˇV and ˇV , ˆV 2 R(U0,U1) 4 . Case 6. ( UP-CongP). Assume U = U 0 0 j U 0 1, U 0 0[ρ 7! W1] ˆV0, and ˆV = ˆV0 j U 0 1[ρ 7! W1]. By the induction hypoth- esis, there exists a closed usage ˇV0 such that ...

  43. [43]

    (tI 0,tO 0) U0, . . . , ρn 7!

    By Definition 3.7 (a), we have U0 j U1 <: U 0 0 j U1. We also have U 0 0 j U1 <: U 0 0 j U 0 1. By Proposition 3.8 (3), we see U0 j U1 <: U 0 0 j U 0 1. (7) For a tuple of variables ˜ρ = ( ρ0, . . . , ρn) and a tuple of usages ˜U = ( U0, . . . , Un), we abbreviate U [ρ0 7! U0, . . . , ρn 7! Un] for U h ˜ρ 7! ˜U i . Let R5 = 1[ n=0 ( V h ρ0 7! " (tI 0,tO 0...

  44. [44]

    Assume τ0 = ξ/U0 and τ1 = ξ/U1

    Hence, we have τ0 j τ1 <: τ 0 0 j τ 0 1. Assume τ0 = ξ/U0 and τ1 = ξ/U1. Then τ0 j τ1 ξ/U0 j U1. For each i = 0 , 1, because of τi <: τ 0 i , we have τ 0 i = ξ/U 0 i and Ui <: U 0 i . By Proposition B.4 (6), we have U0 j U1 <: U 0 0 j U 0

  45. [45]

    (tI ,tO) τ < : τ . Assume τ is a base type. Then

    Then τ0 j τ1 ξ/U0 j U1 <: ξ/U 0 0 j U 0 1 τ 0 0 j τ 0 1. (4) We show τ0 j (τ1 j τ2) <: (τ0 j τ1) j τ2. By (1), (2), (3), and transitivity of <:, we have τ0 j (τ1 j τ2) <: (τ1 j τ2) j τ0 <: (τ2 j τ1) j τ0 <: τ2 j (τ1 j τ0) <: (τ1 j τ0) j τ2 25 <: (τ0 j τ1) j τ2. Thus, τ0 j (τ1 j τ2) <: (τ0 j τ1) j τ2. (5) Assume ob (τ ) = 1. Assume that τ is a base type. S...

  46. [46]

    (a) Since Γ0 <: Γ 0 0, we have Dom (Γ0) Dom(Γ0 0)

    We show Γ0 j Γ1 <: Γ 0 0 j Γ1. (a) Since Γ0 <: Γ 0 0, we have Dom (Γ0) Dom(Γ0 0). Thus, Dom(Γ0 j Γ1) = Dom(Γ0) [ Dom(Γ1) Dom(Γ0

  47. [47]

    (b) Let x 2 Dom(Γ0 0 j Γ1)

    [ Dom(Γ1) = Dom(Γ0 0 j Γ1). (b) Let x 2 Dom(Γ0 0 j Γ1). Since Dom (Γ0 j Γ1) Dom(Γ0 0 j Γ1), we have x 2 Dom(Γ0 j Γ1). Assume x 2 Dom(Γ0

  48. [48]

    Then, we have Γ0 0 j Γ1(x) = Γ 0 0(x) j Γ1(x)

    \ Dom(Γ1). Then, we have Γ0 0 j Γ1(x) = Γ 0 0(x) j Γ1(x). Since Dom (Γ0) Dom(Γ0 0), we have x 2 Dom(Γ0) \ Dom(Γ1). Then, we see Γ0 j Γ1(x) = Γ 0(x) j Γ1(x). Since Γ0 <: Γ 0 0, we have Γ0(x) <: Γ 0 0(x). By Proposition C.1 (3), Γ0(x) j Γ1(x) <: Γ 0 0(x) j Γ1(x). Thus, Γ0 j Γ1(x) <: Γ 0 0 j Γ1(x). Assume x 2 Dom(Γ0

  49. [49]

    Then Γ0 0 j Γ1(x) = Γ 0 0(x)

    n Dom(Γ1). Then Γ0 0 j Γ1(x) = Γ 0 0(x). Since Dom (Γ0) Dom(Γ0 0), we have x 2 Dom(Γ0

  50. [50]

    Then Γ0 j Γ1(x) = Γ 0(x)

    n Dom(Γ1). Then Γ0 j Γ1(x) = Γ 0(x). Since Γ0 <: Γ 0 0, we have Γ0(x) <: Γ 0 0(x). Thus, Γ0 j Γ1(x) <: Γ0 0 j Γ1(x). Assume x 2 Dom(Γ1) n Dom(Γ0 0). Then Γ0 0 j Γ1(x) = Γ 1(x). Assume x 2 Dom(Γ0). Then Γ0 j Γ1(x) = Γ 0(x) j Γ1(x). Since x 2 Dom(Γ0) n Dom(Γ0 0), and Γ0 <: Γ 0 0, we have ob(Γ0(x)) = 1. By Proposition C.1 (5), we see Γ0(x) j Γ1(x) <: Γ 1(x)....

  51. [51]

    Hence, x 2 Dom(Γ0) n Dom(Γ0

    [ Dom(Γ1)). Hence, x 2 Dom(Γ0) n Dom(Γ0

  52. [52]

    Therefore, Γ0 j Γ1(x) = Γ 0(x)

    and x /2 Dom(Γ1). Therefore, Γ0 j Γ1(x) = Γ 0(x). Since Γ0 <: Γ 0 0, we have ob (Γ0(x)) = 1. Thus, ob (Γ0 j Γ1(x)) = 1. (4) Assume Γ0 <: Γ 0 0 and Γ1 <: Γ 0

  53. [53]

    From this proposition (1), Γ0 0 j Γ1 <: Γ1 j Γ0

    By this proposition (3), Γ0 j Γ1 <: Γ 0 0 j Γ1. From this proposition (1), Γ0 0 j Γ1 <: Γ1 j Γ0

  54. [54]

    This proposition (3) implies Γ1 j Γ0 0 <: Γ 0 1 j Γ0

  55. [55]

    From this proposition (1), Γ0 1 j Γ0 0 <: Γ 0 0 j Γ0

  56. [56]

    (5) By (1), (2), (4), and transitivity of <:, we have (Γ0 j Γ1) j Γ2 <: Γ 2 j (Γ0 j Γ1) <: Γ 2 j (Γ1 j Γ0) <: (Γ 2 j Γ1) j Γ0 <: Γ 0 j (Γ2 j Γ1) <: Γ 0 j (Γ1 j Γ2)

    By transitivity, Γ0 j Γ1 <: Γ 0 0 j Γ0 1. (5) By (1), (2), (4), and transitivity of <:, we have (Γ0 j Γ1) j Γ2 <: Γ 2 j (Γ0 j Γ1) <: Γ 2 j (Γ1 j Γ0) <: (Γ 2 j Γ1) j Γ0 <: Γ 0 j (Γ2 j Γ1) <: Γ 0 j (Γ1 j Γ2). Thus, (Γ0 j Γ1) j Γ2 <: Γ 0 j (Γ1 j Γ2). (6) Assume Γ <: Γ 0. We show Γ <: Γ0. 27 (a) Since Γ <: Γ 0, we have Dom (Γ) Dom(Γ0). Since Dom ( Γ) = Dom(Γ)...

  57. [57]

    (tI ,tO) Γ <: Γ. (a) Since Dom

    Thus, ob ((Γ, x : τ )(y)) = 1. (9) Assume (Γ, x : τ ) <: (Γ 0, x : τ ). Then x /2 Dom(Γ) and x /2 Dom(Γ0). We show Γ <: Γ 0. (a) Since (Γ, x : τ ) <: (Γ 0, x : τ ), x /2 Dom(Γ), and x /2 Dom(Γ0), we have Dom (Γ) Dom(Γ0). (b) Let y 2 Dom(Γ0). Since x /2 Dom(Γ0), we have y 6= x. We also see y 2 Dom(Γ0, x : τ ). Since (Γ, x : τ ) <: (Γ 0, x : τ ), we have (Γ...

  58. [58]

    By Γ <: Γ 0 0 jΓ0 1, we have Γ <: Γ 0

  59. [59]

    Then, we have an l-secure derivation tree as follows: π0 Γ0 0 k L ▷m′ P 0 Γ <: Γ 0 0 m L m0 (T-Weak) Γ k L ▷m P 0

    Let π0 be an l-secure derivation tree of Γ0 0 k L ▷l′ P 0. Then, we have an l-secure derivation tree as follows: π0 Γ0 0 k L ▷m′ P 0 Γ <: Γ 0 0 m L m0 (T-Weak) Γ k L ▷m P 0 . 29 Thus, we see that Γ k L ▷m P 0 is derivable. Case 4. ( SP-Zero2). Assume P 0 and P 0 (νx : ξ)0. By Lemma D.1 (1), Γ <: ;. We have an l-secure derivation tree as follows: (T-Zero) ...

  60. [60]

    Hence, Γ <: Γ 0 1 j Γ0

  61. [61]

    Then, we have an l-secure derivation tree as follows: π1 Γ0 1 k L ▷m′ P1 π0 Γ0 0 k L ▷m′ P0 (T-Par) Γ0 1 j Γ0 0 k L ▷m′ P1 j P0 Γ <: Γ 0 1 j Γ0 0 m L m0 (T-Weak) Γ k L ▷m P 0

    Let πi be an l-secure derivation tree of Γ0 i k L ▷m′ Pi for each i = 0, 1. Then, we have an l-secure derivation tree as follows: π1 Γ0 1 k L ▷m′ P1 π0 Γ0 0 k L ▷m′ P0 (T-Par) Γ0 1 j Γ0 0 k L ▷m′ P1 j P0 Γ <: Γ 0 1 j Γ0 0 m L m0 (T-Weak) Γ k L ▷m P 0 . Thus, we see that Γ k L ▷m P 0 is l-securely derivable. In case P P1 j P0 and P 0 P0 j P1, we have an l-...

  62. [62]

    Thus, we see that Γ k L ▷m P 0 is l-securely derivable

    k L ▷m′ P0 j (P1 j P2) (T-Weak) Γ k L ▷m P 0 . Thus, we see that Γ k L ▷m P 0 is l-securely derivable. Case 7. ( SP-New). Assume P (νx : ξ)(P0) j P1, P 0 (νx : ξ)(P0 j P1), and x /2 FN(P1). By Lemma D.1 (2), there exist two type environments Γ0 0, Γ0 1, and m0 2 L such that Γ <: Γ 0 0 j Γ0 1, and m L m0 and Γ0 0 k L ▷m′ (νx : ξ)P0 and Γ0 1 k L ▷m′ P1 are ...

  63. [63]

    (tc+1,tc+1) Γ0 j ˜w :

    n fxg). Then (Γ00 0 , x : ξ/U ) j Γ00 1 (Γ00 0 j Γ00 1 ), x : ξ/U . Since Γ0 0 <: Γ 00 0 and Γ0 1 <: Γ 00 1 , Proposition C.2 (4) implies that Γ0 0 j Γ0 1 <: Γ 00 0 j Γ00 1 . By transitivity of <:, we have Γ <: Γ 00 0 j Γ00 1 . Let π0 be an l-secure derivation tree of Γ00 0 , x : ξ/U k L ▷m′′ P0, and π1 be an l-secure derivation tree of Γ00 1 k L ▷m′ P1. ...

  64. [64]

    By Definition 3.7 (b), there exists a usage U 0 0 such that U0 !U 0 0 and U 0 0 <: U 0

    Since Γ0 <: Γ 1, there exists a core channel type ξ, and a usage U0 such that Γ0(x) = ξ/U0 and U0 <: U1. By Definition 3.7 (b), there exists a usage U 0 0 such that U0 !U 0 0 and U 0 0 <: U 0

  65. [65]

    Then Γ0 !Γ0 0 and Γ0 0 <: Γ 0 1

    Let Γ0 0 = Γ 0[x 7! ξ/U 0 0]. Then Γ0 !Γ0 0 and Γ0 0 <: Γ 0 1. Lemma D.7. For type environments Γ0, Γ0 0, and Γ1, if Γ0 !Γ0 0, then Γ0 j Γ1 !Γ0 0 j Γ1. Proof. Since Γ0 !Γ0 0, there exist a name x, a core channel type ξ, and usages U0, U 0 0 such that Γ0(x) = ξ/U0, Γ0 0(x) = ξ/U 0 0, and U0 !U 0 0. Then Γ0 j Γ1(x) = ξ/U0 or Γ0 j Γ1(x) = ξ/U0 j U1 with some...

  66. [66]

    (tc+1,tc+1) Γ00 0 j ˜v :

    Hence, Γ0 j Γ1 !Γ0 0 j Γ1. If Γ0 j Γ1(x) = ξ/U0 j U1 with some usage U1, then we have Γ0 0 j Γ1(x) = ξ/U 0 0 j U1. Hence, Γ0 j Γ1 !Γ0 0 j Γ1. Now, we prove Proposition 4.5 . Proof of Proposition 4.5. Let P and P 0 be processes. Assume that Γ k L ▷m P is l-securely derivable and (P, L) ! (P 0, L0). We show that there exist a type environment Γ0 such that e...

  67. [67]

    (t′ c+1,t′ c+1) Γ00 1 , x : ˜τ 0 l′′ 10 /I 0 t′c U 0 , l1 L l00 10, and l1 L m00 11,

    By Lemma D.1 (4), there exist a type environments Γ00 1 l00 10 2 L, m00 11 2 L, types ˜τ 0, a usage U 0 and t0 c 2 N [ f1g such that Γ00 1 <: "(t′ c+1,t′ c+1) Γ00 1 , x : ˜τ 0 l′′ 10 /I 0 t′c U 0 , l1 L l00 10, and l1 L m00 11, "(t′ c+1,t′ c+1) Γ00 1 , x : ˜τ 0 l′′ 10 /I 0 t′c U 0 k L is ˇl- secure, Γ00 1 , x : ˜τ 0 l′′ 10 /U , ˜y : ˜τ 0 k L ▷m′′ 11 P1 is...

  68. [68]

    Assume Γ0 0 ! Γ0

    Since Γ <: Γ 0 0 jΓ0 1, we see that Γ k L0 ▷m P0 j P1 is l-securely derivable. Assume Γ0 0 ! Γ0

  69. [69]

    By Lemma D.7 , we have Γ0 0 j Γ0 1 ! Γ0 0 j Γ0

  70. [70]

    By Lemma D.6 , there exists Γ0 such that Γ !Γ0 and Γ0 <: Γ 0 0 j Γ0

  71. [71]

    (tc+1,tc+1) Γ0 j ˜v :

    Since Γ0 <: Γ 0 0 j Γ0 1, we see that Γ0 k L0 ▷m P0 j P1 is l-securely derivable. Case 4. We consider the case ( R-New). In this case, P = ((νx : ξ)P0, L) and P 0 = ((νx : ξ)P 0 0, L0), where (P0, L) ! (P 0 0, L0). By Lemma D.1 (6), there exist a type environments Γ0, a usage U , and m0 2 L0 such that m L m0, rel (U ) and Γ <: Γ 0, and Γ0, x : ξ/U k L ▷m′...

  72. [72]

    (1) Assume (P 0 0, L0) ! (P 00 0 , L0 0)

    We note R R 0. (1) Assume (P 0 0, L0) ! (P 00 0 , L0 0). We show that there exists (P 00 1 , L0

  73. [73]

    such that (P 0 1, L1) ! !(P 00 1 , L0

  74. [74]

    Since P 0 0 ' P0, we have (P0, L0) !(P 00 0 , L0 0)

    and ((P 00 0 , L0 0), (P 00 1 , L0 1)) 2 R 0. Since P 0 0 ' P0, we have (P0, L0) !(P 00 0 , L0 0). Since ((P0, L0), (P1, L1)) 2 R, there exists (P 00 1 , L0

  75. [75]

    such that (P1, L1) ! !(P 00 1 , L0

  76. [76]

    By P1 ' P 0 1, we have (P 0 1, L1) ! !(P 00 1 , L0 1)

    and ((P 00 0 , L0 0), (P 00 1 , L0 1)) 2 R. By P1 ' P 0 1, we have (P 0 1, L1) ! !(P 00 1 , L0 1). By R R 0, we see ((P 00 0 , L0 0), (P 00 1 , L0 1)) 2 R 0. (2) In the same way to (1). (3) By Lemma F.1 , we have Barbs (P 0 0, L) = Barbs(P0, L) and Barbs (P1, L) = Barbs(P 0 1, L). Since ((P0, L0), (P1, L1)) 2 R, we have Barbs (P0, L) = Barbs(P1, L). Hence...

  77. [77]

    We proceed by induction on the construction of C[P0] P 0

    We show that there exists a context C 0 such that P 0 0 = C 0[P0] and C[P1] C 0[P1]. We proceed by induction on the construction of C[P0] P 0

  78. [78]

    If [ ] does not occur in C, then the required condition holds obviously

    We consider cases according to the form of C. If [ ] does not occur in C, then the required condition holds obviously. Assume C = [ ] . Let C 0 = [ ] . Then, the required condition holds. Assume C 6= [ ] . We consider cases according to the last rule of the construction of C[P0] P 0 0. Case 1. Assume P 0 0 = C[P0]. Let C 0 = C. Then, the required conditio...

  79. [79]

    Then, we have C 00[P0] P 0

    By the induction hypothesis, we see that there exists a context C 00 such that Q = C 00[P0] and C[P1] C 00[P1]. Then, we have C 00[P0] P 0

  80. [80]

    Since C[P1] C 00[P1] and C 00[P1] C 0[P1], we have C[P1] C 0[P1]

    By the induction hypothesis, we see that there exists a context C 0 such that C 00[P0] = C 0[P0] and C 00[P1] C 0[P1]. Since C[P1] C 00[P1] and C 00[P1] C 0[P1], we have C[P1] C 0[P1]. Case 3. ( SP-Zero1). Assume P 0 0 = C[P0] j 0. Let C 0 = C j 0. Then C[P1] C 0[P1]. Assume C = C0 j [ ] and P0 = 0 for some context C0. Then P 0 0 = C0[P0]. Let C 0 = C0. T...

Showing first 80 references.