B.2. Casper output
Casper produces the following FDR script from the above description of the protocol and its requirements.
Data
datatype Encryption = Anne | Bob | Yves | Jeeves | Kab | Na | Nb | Garbage | ServerKey.Agent | Sq.Seq(Encryption) | Encrypt.(ALL_KEYS,Seq(Encryption)) | Hash.(HashFunction, Seq(Encryption)) | Xor.(Encryption, Encryption) ALL_KEYS = Union({SessionKey, ServerKeys}) HashFunction = {} ATOM= {Anne, Bob, Yves, Jeeves, Kab, Na, Nb, Garbage} encrypt(m,k) = Encrypt.(k,m) decrypt(Encrypt.(k1,m),k) = if k == inverse(k1) then m else Garbage decrypt(_,_) = Garbage decryptable(Encrypt.(k1,m),k) = k == inverse(k1) decryptable(_,_) = false nth(ms,n) = if n == 1 then head(ms) else nth(tail(ms), n - 1) addGarbage(S) = if S=={} then ...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.
