@article{guttman2005verifying, title={{V}erifying {I}nformation {F}low {G}oals in {S}ecurity-{E}nhanced {L}inux}, author={J.~D.~Guttman and A.~L.~Herzog and J.~D.~Ramsdell and C.~W.~Skorupka}, journal={Journal of Computer Security}, volume={13}, number={1}, pages={115-134}, year={2005}, publisher={IOS Press}}@inproceedings{ottrc, author = {A.~Ott}, title = {{T}he {R}ole {C}ompatibility {S}ecurity {M}odel}, booktitle = {Proc.~of the 7th Nordic Workshop on Secure IT Systems (NordSec)}, year = {2002} }@phdthesis{ottthesis, author = {A.~Ott}, title = {{M}andatory {R}ule {S}et {B}ased {A}ccess {C}ontrol in {L}inux: {A} {M}ulti-{P}olicy {S}ecurity {F}ramework and {R}ole {M}odel {S}olution for {A}ccess {C}ontrol in {N}etworked {L}inux {S}ystems}, year = {2007}, school = {University of Hamburg} }@Unpublished{ottweb, author = {A.~Ott and S.~Fischer-H\"ubner}, title = {{A} {R}ole-{C}ompatibility {M}odel for {S}ecure {S}ystem {A}dministration}, note = {\url{http://www.rsbac.org/doc/media/rc-paper.php}}}@article{Jha08, author = {S.~Jha and N.~Li and M.~V.~Tripunitara and Q.~Wang and W.~H.~Winsborough}, title = {{T}owards {F}ormal {V}erification of {R}ole-{B}ased {A}ccess {C}ontrol {P}olicies}, journal = {IEEE Transactions Dependable and Secure Computing}, volume = {5}, number = {4}, year = {2008}, pages = {242--255}}@INPROCEEDINGS{sanity01, author = {B.~Sarna-Starosta and S.~D.~Stoller}, title = {{P}olicy {A}nalysis for {S}ecurity-{E}nhanced {L}inux}, booktitle = {Proc.~of the 2004 Workshop on Issues in the Theory of Security (WITS)}, year = {2004}, pages = {1--12}}@inproceedings{sanity02, author = {E.~Uzun and V.~Atluri and S.~Sural and J.~Vaidya and G.~Parlato and A.~L.~Ferrara and P.~Madhusudan}, title = {{A}nalyzing {T}emporal {R}ole {B}ased {A}ccess {C}ontrol {M}odels}, booktitle = {Proc.~of the 17th ACM Symposium on Access Control Models and Technologies (SACMAT)}, year = {2012}, pages = {177--186}}@inproceedings{Archer03, author = {M.~Archer and E.~I.~Leonard and M.~Pradella}, title = {{A}nalyzing {S}ecurity-{E}nhanced {L}inux {P}olicy {S}pecifications}, booktitle = {Proc.~of the 4th IEEE International Workshop on Policies for Distributed Systems and Networks (POLICY)}, year = {2003}, pages = {158--169}}@inproceedings{ZhangUrbanWu12, author = {X.~Zhang and C.~Urban and C.~Wu}, title = {{P}riority {I}nheritance {P}rotocol {P}roved {C}orrect}, booktitle = {Proc.~of the 3rd Conference on Interactive Theorem Proving (ITP)}, year = {2012}, pages = {217--232}, series = {LNCS}, volume = {7406}}@inproceedings{Wang09, author = {J.~Wang and H.~Yang and X.~Zhang}, title = {{L}iveness {R}easoning with {I}sabelle/{HOL}}, booktitle = {Proc.~of the 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs)}, year = {2009}, pages = {485--499}, volume = {5674}, series = {LNCS}}@Article{Paulson98, author = {L.~C.~Paulson}, title = {{T}he {I}nductive {A}pproach to {V}erifying {C}ryptographic {P}rotocols}, journal = {Journal of Computer Security}, year = {1998}, volume = {6}, number = {1--2}, pages = {85--128}}