B.1. The Casper input file
#Free variables a, b : Agent s : Server na, nb : Nonce kab : SessionKey ServerKey : Agent -> ServerKeys InverseKeys = (kab, kab), (ServerKey, ServerKey) #Processes INITIATOR(a,na) knows ServerKey(a) RESPONDER(b,s,nb) knows ServerKey(b) SERVER(s,kab) knows ServerKey #Protocol description 0. -> a : b 1. a -> b : na 2. b -> s : {a, na, nb}{ServerKey(b)} 3a. s -> a : {b, kab, na, nb}{ServerKey(a)} 3b. s -> b : {a, kab}{ServerKey(b)} 4. a -> b : {nb}{kab} #Specification Secret(a, kab, [b,s]) Secret(b, kab, [a,s]) Agreement(b, a, [na,nb]) -- Agreement(b, a, [kab]) Agreement(a, b, [kab]) #Actual variables Anne, Bob, Yves : Agent Jeeves : Server Kab : SessionKey Na, Nb : Nonce InverseKeys = (Kab, Kab) #Inline functions symbolic ...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.
