[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Bell and LaPadula in PVS



> Is there a published or reference version of the Bell and LaPadula model 
> implemented in PVS?

Not that I know of, but noninterference is one of the tutorial
examples for PVS, from which Bell and La Padula can be derived as an
access control interpretation:

http://www.csl.sri.com/papers/csl-95-10/ (chapter 3 for noninterference in PVS)
http://www.csl.sri.com/papers/csl-92-2/ (chapter 3 for deriviation of Bell and La Padula)

John Rushby