8 Search Results for "Morgan, Carroll"


Document
Invited Talk
How to Develop an Intuition for Risk... and Other Invisible Phenomena (Invited Talk)

Authors: Natasha Fernandes, Annabelle McIver, and Carroll Morgan

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)


Abstract
The study of quantitative risk in security systems is often based around complex and subtle mathematical ideas involving probabilities. The notations for these ideas can pose a communication barrier between collaborating researchers even when those researchers are working within a similar framework. This paper describes the use of geometrical representation and reasoning as a way to share ideas using the minimum of notation so as to build intuition about what kinds of properties might or might not be true. We describe a faithful geometrical setting for the channel model of quantitative information flow (QIF) and demonstrate how it can facilitate "proofs without words" for problems in the QIF setting.

Cite as

Natasha Fernandes, Annabelle McIver, and Carroll Morgan. How to Develop an Intuition for Risk... and Other Invisible Phenomena (Invited Talk). In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 2:1-2:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{fernandes_et_al:LIPIcs.CSL.2022.2,
  author =	{Fernandes, Natasha and McIver, Annabelle and Morgan, Carroll},
  title =	{{How to Develop an Intuition for Risk... and Other Invisible Phenomena}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{2:1--2:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.2},
  URN =		{urn:nbn:de:0030-drops-157227},
  doi =		{10.4230/LIPIcs.CSL.2022.2},
  annote =	{Keywords: Geometry, Quantitative Information Flow, Proof, Explainability, Privacy}
}
Document
Optimal Strategies in Concurrent Reachability Games

Authors: Benjamin Bordais, Patricia Bouyer, and Stéphane Le Roux

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)


Abstract
We study two-player reachability games on finite graphs. At each state the interaction between the players is concurrent and there is a stochastic Nature. Players also play stochastically. The literature tells us that 1) Player 𝖡, who wants to avoid the target state, has a positional strategy that maximizes the probability to win (uniformly from every state) and 2) from every state, for every ε > 0, Player 𝖠 has a strategy that maximizes up to ε the probability to win. Our work is two-fold. First, we present a double-fixed-point procedure that says from which state Player 𝖠 has a strategy that maximizes (exactly) the probability to win. This is computable if Nature’s probability distributions are rational. We call these states maximizable. Moreover, we show that for every ε > 0, Player 𝖠 has a positional strategy that maximizes the probability to win, exactly from maximizable states and up to ε from sub-maximizable states. Second, we consider three-state games with one main state, one target, and one bin. We characterize the local interactions at the main state that guarantee the existence of an optimal Player 𝖠 strategy. In this case there is a positional one. It turns out that in many-state games, these local interactions also guarantee the existence of a uniform optimal Player 𝖠 strategy. In a way, these games are well-behaved by design of their elementary bricks, the local interactions. It is decidable whether a local interaction has this desirable property.

Cite as

Benjamin Bordais, Patricia Bouyer, and Stéphane Le Roux. Optimal Strategies in Concurrent Reachability Games. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{bordais_et_al:LIPIcs.CSL.2022.7,
  author =	{Bordais, Benjamin and Bouyer, Patricia and Le Roux, St\'{e}phane},
  title =	{{Optimal Strategies in Concurrent Reachability Games}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{7:1--7:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.7},
  URN =		{urn:nbn:de:0030-drops-157278},
  doi =		{10.4230/LIPIcs.CSL.2022.7},
  annote =	{Keywords: Concurrent reachability games, Game forms, Optimal strategies}
}
Document
Characteristic Logics for Behavioural Metrics via Fuzzy Lax Extensions

Authors: Paul Wild and Lutz Schröder

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)


Abstract
Behavioural distances provide a fine-grained measure of equivalence in systems involving quantitative data, such as probabilistic, fuzzy, or metric systems. Like in the classical setting of crisp bisimulation-type equivalences, the wide variation found in system types creates a need for generic methods that apply to many system types at once. Approaches of this kind are emerging within the paradigm of universal coalgebra, based either on lifting pseudometrics along set functors or on lifting general real-valued (fuzzy) relations along functors by means of fuzzy lax extensions. An immediate benefit of the latter is that they allow bounding behavioural distance by means of fuzzy bisimulations that need not themselves be (pseudo-)metrics, in analogy to classical bisimulations (which need not be equivalence relations). The known instances of generic pseudometric liftings, specifically the generic Kantorovich and Wasserstein liftings, both can be extended to yield fuzzy lax extensions, using the fact that both are effectively given by a choice of quantitative modalities. Our central result then shows that in fact all fuzzy lax extensions are Kantorovich extensions for a suitable set of quantitative modalities, the so-called Moss modalities. For non-expansive fuzzy lax extensions, this allows for the extraction of quantitative modal logics that characterize behavioural distance, i.e. satisfy a quantitative version of the Hennessy-Milner theorem; equivalently, we obtain expressiveness of a quantitative version of Moss' coalgebraic logic.

Cite as

Paul Wild and Lutz Schröder. Characteristic Logics for Behavioural Metrics via Fuzzy Lax Extensions. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 27:1-27:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{wild_et_al:LIPIcs.CONCUR.2020.27,
  author =	{Wild, Paul and Schr\"{o}der, Lutz},
  title =	{{Characteristic Logics for Behavioural Metrics via Fuzzy Lax Extensions}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{27:1--27:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.27},
  URN =		{urn:nbn:de:0030-drops-128394},
  doi =		{10.4230/LIPIcs.CONCUR.2020.27},
  annote =	{Keywords: Modal logic, behavioural distance, coalgebra, bisimulation, lax extension}
}
Document
Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security

Authors: Robert Sison and Toby Murray

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)


Abstract
It is common to prove by reasoning over source code that programs do not leak sensitive data. But doing so leaves a gap between reasoning and reality that can only be filled by accounting for the behaviour of the compiler. This task is complicated when programs enforce value-dependent information-flow security properties (in which classification of locations can vary depending on values in other locations) and complicated further when programs exploit shared-variable concurrency. Prior work has formally defined a notion of concurrency-aware refinement for preserving value-dependent security properties. However, that notion is considerably more complex than standard refinement definitions typically applied in the verification of semantics preservation by compilers. To date it remains unclear whether it can be applied to a realistic compiler, because there exist no general decomposition principles for separating it into smaller, more familiar, proof obligations. In this work, we provide such a decomposition principle, which we show can almost halve the complexity of proving secure refinement. Further, we demonstrate its applicability to secure compilation, by proving in Isabelle/HOL the preservation of value-dependent security by a proof-of-concept compiler from an imperative While language to a generic RISC-style assembly language, for programs with shared-memory concurrency mediated by locking primitives. Finally, we execute our compiler in Isabelle on a While language model of the Cross Domain Desktop Compositor, demonstrating to our knowledge the first use of a compiler verification result to carry an information-flow security property down to the assembly-level model of a non-trivial concurrent program.

Cite as

Robert Sison and Toby Murray. Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 27:1-27:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{sison_et_al:LIPIcs.ITP.2019.27,
  author =	{Sison, Robert and Murray, Toby},
  title =	{{Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{27:1--27:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.27},
  URN =		{urn:nbn:de:0030-drops-110829},
  doi =		{10.4230/LIPIcs.ITP.2019.27},
  annote =	{Keywords: Secure compilation, Information flow security, Concurrency, Verification}
}
Document
Kleene Algebra with Observations

Authors: Tobias Kappé, Paul Brunet, Jurriaan Rot, Alexandra Silva, Jana Wagemaker, and Fabio Zanasi

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)


Abstract
Kleene algebra with tests (KAT) is an algebraic framework for reasoning about the control flow of sequential programs. Generalising KAT to reason about concurrent programs is not straightforward, because axioms native to KAT in conjunction with expected axioms for concurrency lead to an anomalous equation. In this paper, we propose Kleene algebra with observations (KAO), a variant of KAT, as an alternative foundation for extending KAT to a concurrent setting. We characterise the free model of KAO, and establish a decision procedure w.r.t. its equational theory.

Cite as

Tobias Kappé, Paul Brunet, Jurriaan Rot, Alexandra Silva, Jana Wagemaker, and Fabio Zanasi. Kleene Algebra with Observations. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 41:1-41:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{kappe_et_al:LIPIcs.CONCUR.2019.41,
  author =	{Kapp\'{e}, Tobias and Brunet, Paul and Rot, Jurriaan and Silva, Alexandra and Wagemaker, Jana and Zanasi, Fabio},
  title =	{{Kleene Algebra with Observations}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{41:1--41:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.41},
  URN =		{urn:nbn:de:0030-drops-109431},
  doi =		{10.4230/LIPIcs.CONCUR.2019.41},
  annote =	{Keywords: Concurrent Kleene algebra, Kleene algebra with tests, free model, axiomatisation, decision procedure}
}
Document
Graded Monads and Graded Logics for the Linear Time - Branching Time Spectrum

Authors: Ulrich Dorsch, Stefan Milius, and Lutz Schröder

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)


Abstract
State-based models of concurrent systems are traditionally considered under a variety of notions of process equivalence. In the case of labelled transition systems, these equivalences range from trace equivalence to (strong) bisimilarity, and are organized in what is known as the linear time - branching time spectrum. A combination of universal coalgebra and graded monads provides a generic framework in which the semantics of concurrency can be parametrized both over the branching type of the underlying transition systems and over the granularity of process equivalence. We show in the present paper that this framework of graded semantics does subsume the most important equivalences from the linear time - branching time spectrum. An important feature of graded semantics is that it allows for the principled extraction of characteristic modal logics. We have established invariance of these graded logics under the given graded semantics in earlier work; in the present paper, we extend the logical framework with an explicit propositional layer and provide a generic expressiveness criterion that generalizes the classical Hennessy-Milner theorem to coarser notions of process equivalence. We extract graded logics for a range of graded semantics on labelled transition systems and probabilistic systems, and give exemplary proofs of their expressiveness based on our generic criterion.

Cite as

Ulrich Dorsch, Stefan Milius, and Lutz Schröder. Graded Monads and Graded Logics for the Linear Time - Branching Time Spectrum. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 36:1-36:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{dorsch_et_al:LIPIcs.CONCUR.2019.36,
  author =	{Dorsch, Ulrich and Milius, Stefan and Schr\"{o}der, Lutz},
  title =	{{Graded Monads and Graded Logics for the Linear Time - Branching Time Spectrum}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{36:1--36:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.36},
  URN =		{urn:nbn:de:0030-drops-109384},
  doi =		{10.4230/LIPIcs.CONCUR.2019.36},
  annote =	{Keywords: Linear Time, Branching Time, Monads, System Equivalences, Modal Logics, Expressiveness}
}
Document
On Coinduction and Quantum Lambda Calculi

Authors: Yuxin Deng, Yuan Feng, and Ugo Dal Lago

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)


Abstract
In the ubiquitous presence of linear resources in quantum computation, program equivalence in linear contexts, where programs are used or executed once, is more important than in the classical setting. We introduce a linear contextual equivalence and two notions of bisimilarity, a state-based and a distribution-based, as proof techniques for reasoning about higher-order quantum programs. Both notions of bisimilarity are sound with respect to the linear contextual equivalence, but only the distribution-based one turns out to be complete. The completeness proof relies on a characterisation of the bisimilarity as a testing equivalence.

Cite as

Yuxin Deng, Yuan Feng, and Ugo Dal Lago. On Coinduction and Quantum Lambda Calculi. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 427-440, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{deng_et_al:LIPIcs.CONCUR.2015.427,
  author =	{Deng, Yuxin and Feng, Yuan and Dal Lago, Ugo},
  title =	{{On Coinduction and Quantum Lambda Calculi}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{427--440},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.427},
  URN =		{urn:nbn:de:0030-drops-53883},
  doi =		{10.4230/LIPIcs.CONCUR.2015.427},
  annote =	{Keywords: Quantum lambda calculi, contextual equivalence, bisimulation}
}
Document
Toward Automatic Verification of Quantum Cryptographic Protocols

Authors: Yuan Feng and Mingsheng Ying

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)


Abstract
Several quantum process algebras have been proposed and successfully applied in verification of quantum cryptographic protocols. All of the bisimulations proposed so far for quantum processes in these process algebras are state-based, implying that they only compare individual quantum states, but not a combination of them. This paper remedies this problem by introducing a novel notion of distribution-based bisimulation for quantum processes. We further propose an approximate version of this bisimulation that enables us to prove more sophisticated security properties of quantum protocols which cannot be verified using the previous bisimulations. In particular, we prove that the quantum key distribution protocol BB84 is sound and (asymptotically) secure against the intercept-resend attacks by showing that the BB84 protocol, when executed with such an attacker concurrently, is approximately bisimilar to an ideal protocol, whose soundness and security are obviously guaranteed, with at most an exponentially decreasing gap.

Cite as

Yuan Feng and Mingsheng Ying. Toward Automatic Verification of Quantum Cryptographic Protocols. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 441-455, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{feng_et_al:LIPIcs.CONCUR.2015.441,
  author =	{Feng, Yuan and Ying, Mingsheng},
  title =	{{Toward Automatic Verification of Quantum Cryptographic Protocols}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{441--455},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.441},
  URN =		{urn:nbn:de:0030-drops-53936},
  doi =		{10.4230/LIPIcs.CONCUR.2015.441},
  annote =	{Keywords: Quantum cryptographic protocols, Verification, Bisimulation, Security}
}
  • Refine by Author
  • 2 Feng, Yuan
  • 2 Schröder, Lutz
  • 1 Bordais, Benjamin
  • 1 Bouyer, Patricia
  • 1 Brunet, Paul
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Modal and temporal logics
  • 1 Security and privacy → Formal methods and theory of security
  • 1 Security and privacy → Information flow control
  • 1 Security and privacy → Logic and verification
  • 1 Software and its engineering → Compilers
  • Show More...

  • Refine by Keyword
  • 2 Verification
  • 2 bisimulation
  • 1 Bisimulation
  • 1 Branching Time
  • 1 Concurrency
  • Show More...

  • Refine by Type
  • 8 document

  • Refine by Publication Year
  • 3 2019
  • 2 2015
  • 2 2022
  • 1 2020

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail