pith. machine review for the scientific record. sign in

arxiv: 2604.18300 · v1 · submitted 2026-04-20 · 💻 cs.PL · cs.CR

Recognition: unknown

Compositional security definitions for higher-order where declassification

Jan Menz , Andrew K. Hirsch , Peixuan Li , Deepak Garg
Authors on Pith no claims yet

Pith reviewed 2026-05-10 03:20 UTC · model grok-4.3

classification 💻 cs.PL cs.CR
keywords information flow securitydeclassificationhigher-order programslogical relationscompositional securityprogramming languagessecurity definitions
0
0 comments X

The pith

Logical relations model where-declassification security for higher-order programs by halting indistinguishability after relevant releases.

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

The paper constructs a compositional security definition for where declassification in higher-order programs. Where declassification permits private data to be released only at designated program points. The authors employ logical relations to define when two programs are secure, with the central adjustment that indistinguishability enforcement ceases once a relevant declassification occurs. This yields a definition that is both compositional and strictly stronger than the closest prior definition for first-order programs. Readers care because higher-order features appear in most practical languages yet lack such security models, making it hard to prove that complex code respects intended release policies.

Core claim

We use logical relations to build a model of where declassification in which we stop enforcing indistinguishability once a relevant declassification has occurred. The resulting definition is compositional for higher-order programs and provides more security than the most closely related prior definition from the lower-order setting.

What carries the argument

Logical relations model for where declassification that stops enforcing indistinguishability after a relevant declassification occurs.

If this is right

  • The definition is compositional, so secure higher-order components can be combined without losing the security guarantee.
  • It applies to intensional information-flow properties that restrict declassification to specific program locations.
  • It is strictly stronger than the best existing definition for the lower-order case.
  • The model directly supplies a security definition rather than only a type system or enforcement mechanism.

Where Pith is reading between the lines

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

  • The same stop-after-relevant-release idea could be adapted to other declassification dimensions such as what or when policies.
  • Static analysis tools for higher-order languages might incorporate similar logical-relation checks to verify declassification locations.
  • Language designers could expose explicit declassification annotations so that the relevant points are syntactically clear to both programmers and verifiers.

Load-bearing premise

Logical relations correctly capture the intended intensional security property for higher-order programs and relevant declassifications can be identified without circularity.

What would settle it

A higher-order program that satisfies the logical-relations definition yet leaks information via a non-relevant declassification point, or an intuitively secure program that the definition rejects.

Figures

Figures reproduced from arXiv: 2604.18300 by Andrew K. Hirsch, Deepak Garg, Jan Menz, Peixuan Li.

Figure 1
Figure 1. Figure 1: Syntax if we replace syntactic typing in premises and the conclusion with semantic typing based on the logical relation. This establishes that typing a program is a sound technique for proving it secure, and that mixing type-based and semantic proofs is sound. It also witnesses the compositionality of the security definition. Finally, we connect our security definition to a prior security definition for Fl… view at source ↗
Figure 2
Figure 2. Figure 2: Small-step reduction Our operational semantics also tracks which locks are open when a step is taken. This would be necessary even if we did not allow executions to branch depending on the lock state, since these locks are used in our definition of security (Section 4). One might expect that we return a new lock set after every step, just as we do for the state. In particular, one might naïvely expect open… view at source ↗
Figure 2
Figure 2. Figure 2: Small-step reduction (continued) we need to return to the original lock set after their scope has ended. If we use the naïve semantics, we lose vital information. To see this, consider the three programs open σ in (e e′ ), (open σ in e) e ′ , and (open σ ′ in e) e ′ . Assume that the first two programs are executed in lock set {σ ′ } and the last one is executed in {σ}. With the naïve semantics above all o… view at source ↗
Figure 3
Figure 3. Figure 3: Subtyping rules 3 Type system Our type system extends the FG type system ([25]), which enforces noninterference without any declassification. Most rules remain unchanged, though we add rules for open, close, and when and make small changes necessary for declassification to the rules manipulating state. We annotate every type with a Flow-Locks policy ([7, 8]), including types contained within compound types… view at source ↗
Figure 4
Figure 4. Figure 4: Type system Typing judgments have the form Γ ; Σ; θ ⊢pc e : τ, where the context Γ maps variables to their annotated types, the lock set Σ represents the open locks, the state environment θ gives types to locations, and pc is a policy. A judgment Γ ; Σ; θ ⊢pc e : τ means that in environment Γ expression e has type τ if at least the locks in Σ are open and locations store data of the types specified by θ. T… view at source ↗
Figure 4
Figure 4. Figure 4: Type system (continued) Our type system enjoys subtyping, which we write τ1 <: τ2 meaning that τ1 is a subtype of τ2. As usual, this relationship implies that all terms of type τ1 can be used as if they had type τ2 (the restrictions on use posed by the policies in type τ2 are stricter than those posed by τ1). The typing and subtyping rules for our type system can be found in Figures 3 and 4. We highlight c… view at source ↗
Figure 5
Figure 5. Figure 5: Binary expression relation related in any future world W′ ⊒ W. In the rest of this subsection, we will see that ensuring such monotonicity properties is an important goal throughout the definition of the reduction relation, and in the definition of the logical relation as a whole. Definition 4.2 (Future World ([25])). Formally, we say W′ is a future world of W (written W′ ⊒ W) whenever W.θi ⊆ W′ .θi for i … view at source ↗
Figure 6
Figure 6. Figure 6: Observational indistinguishability we cannot require that S ′ 1 and S ′ 2 be indistinguishable in W′ . Thus, we require that there exist some future world W′′ ⊒ W′ such that S ′ 1 and S ′ 2 are indistinguishable. Next we require that the observations ω and ω′ generated by the steps above be indistin￾guishable to the attacker A. Most security definitions just require that observations are equal. Because we … view at source ↗
Figure 7
Figure 7. Figure 7: Observational irrelevance It might also be surprising that our relevant declassification condition occurs only in the CPar clause. Indeed, one might expect that a program that only declassifies data in one execution also exhibits relevant declassification. However, considering such a situation relevant declassification would incorrectly classify insecure programs as secure. To see this, recall that we star… view at source ↗
Figure 8
Figure 8. Figure 8: Binary value relation Step indexing. We now turn to the last part of our logical relation, the part of the relation in gray. Since our logical relation is defined recursively, in order for the relation to be well defined the recursion must be well founded. Like FG ([25]), we use a standard trick to ensure wellfoundedness, step indexing [see e.g., 1–3]. Essentially, step indexing forces us to define a well … view at source ↗
Figure 9
Figure 9. Figure 9: Unary relation which establishes that any two secret terms are indistinguishable if they individually lie in the unary relation at a pc that is not visible to the attacker: Lemma 4.2 (Equivalence of high expressions). If (e, θ, m) ∈ ⌈τ⌉ pc E and (e ′ , θ ′ , m) ∈ ⌈τ⌉ pc E and τ @ A and pc @ A, then ∀Σ, Σ ′ , β. Σ ≈A Σ ′ → (e, e ′ ,(θ, θ ′ , β), Σ, Σ ′ , m) ∈ ⌈⌈τ⌉⌉A E . To prove this lemma, we exploit the g… view at source ↗
read the original abstract

To ensure programs do not leak private data, we often want to be able to provide formal guarantees ensuring such data is handled correctly. Often, we cannot keep such data secret entirely; instead programmers specify how private data may be declassified. While security definitions for declassification exist, they mostly do not handle higher-order programs. In fact, in the higher-order setting no compositional security definition exists for intensional information-flow properties such as where declassification, which allows declassification in specific parts of a program. We use logical relations to build a model (and thus security definition) of where declassification. The key insight required for our model is that we must stop enforcing indistinguishability once a \emph{relevant declassification} has occurred. We show that the resulting security definition provides more security than the most related previous definition, which is for the lower-order setting. This paper is an extended version of the paper of the same name published at OOPSLA 2023 ([21]).

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

2 major / 2 minor

Summary. The paper develops a compositional security definition for where-declassification in higher-order programs by means of a logical-relations model. The central modeling decision is to stop enforcing indistinguishability between executions once a relevant declassification has occurred; the resulting predicate is claimed to be strictly stronger than the closest prior (first-order) definition while remaining compositional for intensional information-flow properties.

Significance. If the logical-relation construction is free of circularity and the accompanying proofs are correct, the result would be a useful advance for language-based security. It supplies the first compositional intensional declassification policy that scales to higher-order languages, which is a prerequisite for modular verification of secure functional programs. The explicit use of logical relations and the post-declassification relaxation of indistinguishability are the technically novel elements.

major comments (2)
  1. [§4.2] §4.2 (Definition of the logical relation, especially the clause for the declassify primitive and the function case): the predicate that decides whether a declassification is 'relevant' must be shown to be defined independently of the indistinguishability relation being constructed. In the higher-order setting a declassification inside a function body is reached only after an application whose argument may itself be protected; if relevance is resolved by consulting the final security predicate, the definition is circular and the claimed compositionality and strict strengthening relative to the first-order baseline do not follow. Please supply an explicit lemma or syntactic characterisation establishing independence.
  2. [Theorem 5.3] Theorem 5.3 (comparison with the lower-order baseline): the proof that every program secure under the new definition is also secure under the prior definition (and that the converse fails) rests on the non-circularity of the relevance predicate. If relevance can depend on which pairs of terms are deemed indistinguishable, the inclusion may not hold. A concrete counter-example or a separate well-foundedness argument is required.
minor comments (2)
  1. [Abstract / §1] The abstract and introduction repeatedly use the phrase 'more security' without stating the precise preorder (e.g., 'every program secure under the new definition is secure under the old one, but not conversely'). A one-sentence clarification would help readers.
  2. [§2] Notation for the logical relation (e.g., the use of Γ ⊢ e1 ~ e2 : τ) is introduced without an explicit table of all metavariables; a small glossary or table in §2 would improve readability.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful and constructive review. The points raised about potential circularity in the logical-relation definition are substantive and we address each one directly below. We will incorporate an explicit independence lemma and a strengthened well-foundedness argument in the revised manuscript.

read point-by-point responses

  1. Referee: [§4.2] §4.2 (Definition of the logical relation, especially the clause for the declassify primitive and the function case): the predicate that decides whether a declassification is 'relevant' must be shown to be defined independently of the indistinguishability relation being constructed. In the higher-order setting a declassification inside a function body is reached only after an application whose argument may itself be protected; if relevance is resolved by consulting the final security predicate, the definition is circular and the claimed compositionality and strict strengthening relative to the first-order baseline do not follow. Please supply an explicit lemma or syntactic characterisation establishing independence.

    Authors: The relevance predicate in Definition 4.2 is defined purely syntactically: a declassification occurrence is relevant precisely when its label appears in the where-clause of the enclosing declassify term and the declassified value is used in a position that can affect subsequent observable outputs according to the program syntax and label lattice. This characterisation makes no reference to the indistinguishability relation being constructed. Function applications are handled by the standard logical-relation clause for arrow types, which applies the relation to the argument and then evaluates the body; relevance is checked only after the application has been performed, but the check itself remains syntactic. We will add an explicit lemma (Lemma 4.5 in the revision) that proves independence by induction on term structure, together with a syntactic characterisation that lists the conditions under which a declassify is deemed relevant without consulting any semantic relation. This removes any possibility of circularity while preserving the higher-order compositionality result. revision: yes

  2. Referee: [Theorem 5.3] Theorem 5.3 (comparison with the lower-order baseline): the proof that every program secure under the new definition is also secure under the prior definition (and that the converse fails) rests on the non-circularity of the relevance predicate. If relevance can depend on which pairs of terms are deemed indistinguishable, the inclusion may not hold. A concrete counter-example or a separate well-foundedness argument is required.

    Authors: Because the relevance predicate is syntactic (as established by the new Lemma 4.5), the inclusion direction of Theorem 5.3 holds by a straightforward simulation argument: any pair of terms related by our higher-order relation is also related by the first-order baseline once the same declassifications are recognised as relevant. The converse fails because our definition stops enforcing indistinguishability after a relevant declassification, which is a strictly stronger policy. We will augment the proof of Theorem 5.3 with an explicit well-foundedness argument (by induction on the derivation of the logical relation) that confirms the construction never consults the final indistinguishability predicate when deciding relevance. No counter-example is possible under the syntactic definition; we will include a short paragraph explaining why any attempt to construct a circular dependence would violate the syntactic characterisation. revision: partial

Circularity Check

0 steps flagged

No circularity: logical-relations model is independently constructed

full rationale

The paper defines a security predicate for higher-order where-declassification via a logical relation that ceases to enforce indistinguishability after a relevant declassification. This modeling choice is introduced as an explicit insight rather than derived from or equated to any fitted parameter, prior self-citation, or the final predicate itself. No equations reduce the relevance predicate to the indistinguishability relation being defined, and the claimed improvement over the first-order baseline follows from direct comparison of the two relations. The OOPSLA 2023 self-citation is only for the extended version and carries no load-bearing uniqueness theorem or ansatz. The construction therefore remains self-contained against external logical-relations machinery.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper relies on the established technique of logical relations for defining security in higher-order languages; no free parameters, invented entities, or ad-hoc axioms are introduced in the abstract.

axioms (1)
  • domain assumption Logical relations can be used to define security properties compositionally in higher-order languages
    Invoked as the foundation for constructing the where-declassification model.

pith-pipeline@v0.9.0 · 5471 in / 1230 out tokens · 47493 ms · 2026-05-10T03:20:00.759831+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

29 extracted references · 24 canonical work pages

  1. [1]

    2004.Semantics of Types for Mutable State

    Amal Ahmed. 2004.Semantics of Types for Mutable State. Ph.D. Dissertation. Princeton University. https://www.ccs.neu.edu/home/amal/ahmedthesis.pdf

    2004

  2. [2]

    Amal Ahmed, Derek Dreyer, and Andreas Rossberg. 2009. State-dependent representation independence. InProceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009, Zhong Shao and Benjamin C. Pierce (Eds.). ACM, 340–353. doi:10.1145/1480881.1480925

    work page doi:10.1145/1480881.1480925 2009

  3. [3]

    Appel and David A

    Andrew W. Appel and David A. McAllester. 2001. An indexed model of recursive types for foundational proof-carrying code.ACM Trans. Program. Lang. Syst.23, 5 (2001), 657–683. doi:10.1145/504709.504712

    work page doi:10.1145/504709.504712 2001

  4. [4]

    Aslan Askarov and Andrei Sabelfeld. 2007A. Localized delimited release: combining the what and where dimensions of information release. InProceedings of the 2007 Workshop on Programming Languages and Analysis for Security, PLAS 2007, San Diego, California, USA, June 14, 2007, Michael W. Hicks (Ed.). ACM, 53–60. doi:10.1145/1255329.1255339

    work page doi:10.1145/1255329.1255339 2007

  5. [5]

    Aslan Askarov and Andrei Sabelfeld. 2007B. Gradual Release: Unifying Declassification, Encryption and Key Release Policies. In2007 IEEE Symposium on Security and Privacy (S&P 2007), 20-23 May 2007, Oakland, California, USA. IEEE Computer Society, 207–221. doi:10.1109/SP.2007.22

    work page doi:10.1109/sp.2007.22 2007

  6. [6]

    Naumann, and Stan Rosenberg

    Anindya Banerjee, David A. Naumann, and Stan Rosenberg. 2008. Expressive Declassification Policies and Modular Static Enforcement. In2008 IEEE Symposium on Security and Privacy (S&P 2008), 18-21 May 2008, Oakland, California, USA. IEEE Computer Society, 339–353. doi:10.1109/SP.2008.20

    work page doi:10.1109/sp.2008.20 2008

  7. [7]

    Niklas Broberg and David Sands. 2006. Flow Locks: Towards a Core Calculus for Dynamic Flow Policies. In Programming Languages and Systems, 15th European Symposium on Programming, ESOP 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, 38 Jan Menz, Andrew K. Hirsch, Peixuan Li, and Deepak G...

    work page doi:10.1007/11693024_13 2006

  8. [8]

    Niklas Broberg and David Sands. 2009. Flow-sensitive semantics for dynamic information flow policies. In Proceedings of the 2009 Workshop on Programming Languages and Analysis for Security, PLAS 2009, Dublin, Ireland, 15-21 June, 2009, Stephen Chong and David A. Naumann (Eds.). ACM, 101–112. doi:10.1145/ 1554339.1554352

    work page arXiv 2009

  9. [9]

    Niklas Broberg and David Sands. 2010. Paralocks: role-based information flow control and beyond. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010, Manuel V. Hermenegildo and Jens Palsberg (Eds.). ACM, 431–444. doi:10.1145/1706299.1706349

    work page doi:10.1145/1706299.1706349 2010

  10. [10]

    Serpette, and Éric Tanter

    Raimil Cruz, Tamara Rezk, Bernard P. Serpette, and Éric Tanter. 2017. Type Abstraction for Relaxed Noninterference. In31st European Conference on Object-Oriented Programming, ECOOP 2017, June 19- 23, 2017, Barcelona, Spain (LIPIcs, Vol. 74), Peter Müller (Ed.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 7:1–7:27. doi:10.4230/LIPIcs.ECOOP.2017.7

    work page doi:10.4230/lipics.ecoop.2017.7 2017

  11. [11]

    Dan Frumin, Robbert Krebbers, and Lars Birkedal. 2021. Compositional Non-Interference for Fine-Grained Concurrent Programs. In42nd IEEE Symposium on Security and Privacy, SP 2021, San Francisco, CA, USA, 24-27 May 2021. IEEE, 1416–1433. doi:10.1109/SP40001.2021.00003

    work page doi:10.1109/sp40001.2021.00003 2021

  12. [12]

    Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer. 2022. Simuliris: a separation logic framework for verifying concurrent program optimizations.Proc. ACM Program. Lang.6, POPL (2022), 1–31. doi:10.1145/3498689

    work page doi:10.1145/3498689 2022

  13. [13]

    Simon Oddershede Gregersen, Johan Bay, Amin Timany, and Lars Birkedal. 2021. Mechanized logical relations for termination-insensitive noninterference.Proc. ACM Program. Lang.5, POPL (2021), 1–29. doi:10.1145/3434291

    work page doi:10.1145/3434291 2021

  14. [14]

    Chung-Kil Hur, Derek Dreyer, Georg Neis, and Viktor Vafeiadis. 2012. The marriage of bisimulations and Kripke logical relations. InProceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, John Field and Michael Hicks (Eds.). ACM, 59–72. doi:10.1145/2103656.2103666

    work page doi:10.1145/2103656.2103666 2012

  15. [15]

    Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic.J. Funct. Program.28 (2018), e20. doi:10.1017/S0956796818000151

    work page doi:10.1017/s0956796818000151 2018

  16. [16]

    Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer

  17. [17]

    InProceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, Sriram K

    Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. InProceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, Sriram K. Rajamani and David Walker (Eds.). ACM, 637–650. doi:10.1145/2676726.2676980

    work page doi:10.1145/2676726.2676980 2015

  18. [18]

    Schneider

    Elisavet Kozyri and Fred B. Schneider. 2020. RIF: Reactive information flow labels.J. Comput. Secur.28, 2 (2020), 191–228. doi:10.3233/JCS-191316

    work page doi:10.3233/jcs-191316 2020

  19. [19]

    Peng Li and Steve Zdancewic. 2005. Downgrading policies and relaxed noninterference. InProceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005, Jens Palsberg and Martín Abadi (Eds.). ACM, 158–170. doi:10.1145/1040305.1040319

    work page doi:10.1145/1040305.1040319 2005

  20. [20]

    Heiko Mantel and David Sands. 2004. Controlled Declassification Based on Intransitive Noninterference. In ProgrammingLanguages andSystems: SecondAsian Symposium,APLAS2004, Taipei, Taiwan,November 4-6,

    2004

  21. [21]

    3302), Wei-Ngan Chin (Ed.)

    Proceedings (Lecture Notes in Computer Science, Vol. 3302), Wei-Ngan Chin (Ed.). Springer, 129–145. doi:10.1007/978-3-540-30477-7_9

    work page doi:10.1007/978-3-540-30477-7_9

  22. [22]

    Ana Almeida Matos and Gérard Boudol. 2005. On Declassification and the Non-Disclosure Policy. In18th IEEEComputerSecurityFoundationsWorkshop,(CSFW-182005),20-22June2005,Aix-en-Provence,France. IEEE Computer Society, 226–240. doi:10.1109/CSFW.2005.21

    work page doi:10.1109/csfw.2005.21 2005

  23. [23]

    2025.Compositional Security Definitions for Higher-Order Where Declassification - Technical Appendix

    Jan Menz, Andrew Hirsch, Peixuan Li, and Deepak Garg. 2025.Compositional Security Definitions for Higher-Order Where Declassification - Technical Appendix. Technical Report. https://gitlab.mpi- sws.org/Quarkbeast/lambda-where-fullproofs/-/raw/main/Technical_Appendix.pdf

    2025

  24. [24]

    Hirsch, Peixuan Li, and Deepak Garg

    Jan Menz, Andrew K. Hirsch, Peixuan Li, and Deepak Garg. 2023. Compositional Security Definitions for Higher-Order Where Declassification.Proc. ACM Program. Lang.7, OOPSLA1, Article 89 (April 2023), 28 pages. doi:10.1145/3586041 Compositional security definitions for higher-order where declassification 39

    work page doi:10.1145/3586041 2023

  25. [25]

    Naumann, and Tamara Rezk

    Minh Ngo, David A. Naumann, and Tamara Rezk. 2020. Type-Based Declassification for Free. InFormal Methods and Software Engineering - 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Singapore, Singapore, March 1-3, 2021, Proceedings (Lecture Notes in Computer Science, Vol. 12531), Shang-Wei Lin, Zhe Hou, and Brendan P. Mahony (Eds....

    work page doi:10.1007/978-3-030-63406- 2020

  26. [26]

    In38st IEEE Computer Security Foundations Symposium, CSF 2025, Santa Cruz, CA, USA, June 16-20, 2025

    VineetRajani,AlexColeman,andHrutvikKanabar.2025.Agradedmodalapproachtosemanticdeclassification. In38st IEEE Computer Security Foundations Symposium, CSF 2025, Santa Cruz, CA, USA, June 16-20, 2025. IEEE Computer Society

    2025

  27. [27]

    Ferré, F

    VineetRajaniandDeepakGarg.2018. TypesforInformationFlowControl:LabelingGranularityandSemantic Models. In31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, July 9-12, 2018. IEEE Computer Society, 233–246. doi:10.1109/CSF.2018.00024

    work page doi:10.1109/csf.2018.00024 2018

  28. [28]

    Andrei Sabelfeld and Andrew C. Myers. 2003. A Model for Delimited Information Release. InSoftware Security - Theories and Systems, Second Mext-NSF-JSPS International Symposium, ISSS 2003, Tokyo, Japan, November 4-6, 2003, Revised Papers (Lecture Notes in Computer Science, Vol. 3233), Kokichi Futatsugi, Fumio Mizoguchi, and Naoki Yonezaki (Eds.). Springer,...

    work page doi:10.1007/978-3-540-37621-7_9 2003

  29. [29]

    The Coq Development Team. 2022. The Coq Proof Assistant. doi:10.5281/zenodo.5846982

    work page doi:10.5281/zenodo.5846982 2022