External Consistency and the Verification of Security Protocols

Abstract

I have been wondering what is meant by system integrity and I came up with an interesting result, at least I think it’s interesting. And there’s a tie-in to security protocols in the answer and I get to that later on in the talk. If you look at conventional models of system integrity, we talk about things like Clark and Wilson and Biba, they’re all implementation oriented. They say: this is how we achieve integrity, we achieve integrity using things like segregation of duties, well-formed transactions, audit, and so on. And they say these are good things to use in your systems. So if you were to take Clark and Wilson and try to evaluate a particular system configuration according to their model, all it’s going to tell you is that your system uses good design principles. It’s not going to tell you that it actually guarantees integrity. So it’s not going to say that if you use a particular system configuration you can bypass integrity by some very obscure circuitous route which you hadn’t anticipated, so Clark and Wilson and Biba are operational models, they say this is how we achieve integrity they don’t say what integrity is.