Article

Non-Interference in Constructive Authorization Logic

Authors:

Deepak Garg,

Frank PfennAuthors Info & Claims

CSFW '06: Proceedings of the 19th IEEE workshop on Computer Security Foundations

Pages 283 - 296

https://doi.org/10.1109/CSFW.2006.18

Published: 05 July 2006 Publication History

Publisher Site

Abstract

We present a constructive authorization logic where the meanings of connectives are defined by their associated inference rules. This ensures that the logical reading of access control policies expressed in the logic and their implementation coincide. We study the proof-theoretic consequences of our design including cut-elimination and two non-interference properties that allow administrators to explore the correctness of their policies by establishing that for a given policy, assertions made by certain principals will not affect the truth of assertions made by others.

Cited By

View all

de Groot JLitak TPattinson DGorla D(2021)Gödel-McKinsey-Tarski and Blok-Esakia for Heyting-Lewis implicationProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470508(1-15)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470508
Lippmeier BRobinson AMuys AKomendantskaya E(2019)Smart Contracts as Authorized Production RulesProceedings of the 21st International Symposium on Principles and Practice of Declarative Programming10.1145/3354166.3354179(1-14)Online publication date: 7-Oct-2019
https://dl.acm.org/doi/10.1145/3354166.3354179
Crary KSullivan M(2015)Peer-to-peer affine commitment using bitcoinACM SIGPLAN Notices10.1145/2813885.273799750:6(479-488)Online publication date: 3-Jun-2015
https://dl.acm.org/doi/10.1145/2813885.2737997
Show More Cited By

Index Terms

Non-Interference in Constructive Authorization Logic

Recommendations

Constructive linear-time temporal logic: Proof systems and Kripke semantics

In this paper we study a version of constructive linear-time temporal logic (LTL) with the ''next'' temporal operator. The logic is originally due to Davies, who has shown that the proof system of the logic corresponds to a type system for binding-time ...
Constructive Game Logic
Programming Languages and Systems
Abstract
Game Logic is an excellent setting to study proofs-about-programs via the interpretation of those proofs as programs, because constructive proofs for games correspond to effective winning strategies to follow in response to the opponent’s actions. ...
Constructive Logic with Strong Negation as a Substructural Logic

Spinks and Veroff have shown that constructive logic with strong negation (CLSN for short), can be considered as a substructural logic. We use algebraic tools developed to study substructural logics to investigate some axiomatic extensions of CLSN. For ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

CSFW '06: Proceedings of the 19th IEEE workshop on Computer Security Foundations

July 2006

307 pages

ISBN:0769526152

Publisher

IEEE Computer Society

United States

Publication History

Published: 05 July 2006

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

32
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 07 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

de Groot JLitak TPattinson DGorla D(2021)Gödel-McKinsey-Tarski and Blok-Esakia for Heyting-Lewis implicationProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470508(1-15)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470508
Lippmeier BRobinson AMuys AKomendantskaya E(2019)Smart Contracts as Authorized Production RulesProceedings of the 21st International Symposium on Principles and Practice of Declarative Programming10.1145/3354166.3354179(1-14)Online publication date: 7-Oct-2019
https://dl.acm.org/doi/10.1145/3354166.3354179
Crary KSullivan M(2015)Peer-to-peer affine commitment using bitcoinACM SIGPLAN Notices10.1145/2813885.273799750:6(479-488)Online publication date: 3-Jun-2015
https://dl.acm.org/doi/10.1145/2813885.2737997
Crary KSullivan MGrove DBlackburn S(2015)Peer-to-peer affine commitment using bitcoinProceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2737924.2737997(479-488)Online publication date: 3-Jun-2015
https://dl.acm.org/doi/10.1145/2737924.2737997
Hirsch AClarkson MSadeghi AGligor VYung M(2013)Belief semantics of authorization logicProceedings of the 2013 ACM SIGSAC conference on Computer & communications security10.1145/2508859.2516667(561-572)Online publication date: 4-Nov-2013
https://dl.acm.org/doi/10.1145/2508859.2516667
Amir-Mohammadian SFallah M(2013)Noninterference in a predicative polymorphic calculus for access controlComputer Languages, Systems and Structures10.1016/j.cl.2013.06.00139:3(109-120)Online publication date: 1-Oct-2013
https://dl.acm.org/doi/10.1016/j.cl.2013.06.001
Garg DPfenning F(2012)Stateful authorization logic --Proof theory and a case studyJournal of Computer Security10.5555/2590602.259060520:4(353-391)Online publication date: 1-Jul-2012
https://dl.acm.org/doi/10.5555/2590602.2590605
Cave APientka BField JHicks M(2012)Programming with binders and indexed data-typesProceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/2103656.2103705(413-424)Online publication date: 25-Jan-2012
https://dl.acm.org/doi/10.1145/2103656.2103705
Cave APientka B(2012)Programming with binders and indexed data-typesACM SIGPLAN Notices10.1145/2103621.210370547:1(413-424)Online publication date: 25-Jan-2012
https://dl.acm.org/doi/10.1145/2103621.2103705
Nigam V(2012)On the Complexity of Linear Authorization LogicsProceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer Science10.1109/LICS.2012.61(511-520)Online publication date: 25-Jun-2012
https://dl.acm.org/doi/10.1109/LICS.2012.61
Show More Cited By

Abstract

Cited By

Index Terms

Recommendations

Constructive linear-time temporal logic: Proof systems and Kripke semantics

Constructive Game Logic

Constructive Logic with Strong Negation as a Substructural Logic

Comments

Information

Published In

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations