Abstract | ||
---|---|---|
We present an authorization logic that permits reasoning with explicit time. Following a proof-theoretic approach, we study the meta-theory of the logic, including cut elimination. We also demonstrate formal connections to proof-carrying authorization's existing approach for handling time and comment on the enforceability of our logic in the same framework. Finally, we illustrate the expressiveness of the logic through examples, including those with complex interactions between time, authorization, and mutable state. |
Year | DOI | Venue |
---|---|---|
2008 | 10.1109/CSF.2008.15 | CSF |
Keywords | Field | DocType |
cut elimination,explicit time,formal connection,complex interaction,existing approach,proof-carrying authorization,authorization logic,mutable state,proof-theoretic approach,interactions,computer security,hybrid systems,access control,security,elimination,principal component analysis,linearity,reasoning,authorization,logic programming,logic,cognition,computer access control,control,theory | Signature (logic),Computer access control,Hybrid logic,Temporal logic of actions,Autoepistemic logic,Computer science,Multimodal logic,Description logic,Theoretical computer science,Logic programming | Conference |
Citations | PageRank | References |
11 | 0.69 | 33 |
Authors | ||
3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Henry DeYoung | 1 | 69 | 4.74 |
Deepak Garg | 2 | 581 | 45.48 |
Frank Pfenning | 3 | 3376 | 265.34 |