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

@inproceedings{gran12,
  author    = {M.~Bugliesi and
               S.~Calzavara and
               R.~Focardi and
               M.~Squarcina},
  title     = {{G}ran: {M}odel {C}hecking {G}rsecurity {RBAC} {P}olicies},
  booktitle = {Proc.~of the 25th IEEE Computer Security Foundations Symposium (CSF)},
  year      = {2012},
  pages     = {126--138}
}