@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}

}