6.4. Example deduction system
Recall that Messages is the finite subset of the Encryption datatype that includes all the bodies of messages of the forms used in the protocol that are type-correct (have nonces in the right place, use keys as the key in encryptions, and so on). We can decompose these using the components function discussed above, to give the set Fact (of which the set KnowableFact over which we replicate the intruder’s knowledge cells is a subset).
There are standard axioms concerning encryption that will apply whenever the relevant type of encryption is part of the protocol:
EncryptionDeductions = {(Encrypt.(k,fs), unknown(union({k}, set(fs)))) | Encrypt.(k,fs) <- Fact} DecryptionDeductions = {(f, unknown({Encrypt.(k,fs), inverse(k)})) ...Get The Modelling and Analysis of Security Protocols: the CSP Approach now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
