SPiSPi Calculus: Outline Calculus: Outline•• What is it? What is it?•• Basic Basic SPiSPi Calculus Notation Calculus Notation•• Basic Example Basic Example•• Example with Channel Establishment Example with Channel Establishment•• Example using Cryptography Example using CryptographySPiSPi Calculus: What is it? Calculus: What is it?• SPi Calculus is an executable model for thedescription and analysis of cryptographicprotocols• Spi Calculus is an extension to Pi CalculusSPiSPi Calculus: Processes Calculus: ProcessesSpi Calculus is made up of Processes. Whenall the processes are combined we have aprogram or protocol.SPiSPi Calculus: Processes Calculus: ProcessesP ӂ (some action our process does)Processes are defined as follows:Where P is our processSPiSPi Calculus: Processes Calculus: ProcessesProcesses can do many things• They can create other processes• They can send messages• They can receive messages• They can run other processesYou can think of a process as the set of actionsa principal takes (Alice, Bob, Malory etc.)SPiSPi Calculus: Processes Calculus: ProcessesWhen processes send or receive messagesthey do this over channelsSPiSPi Calculus: Basic Calculus: BasicDefinitionsDefinitions•A channel is a named communicationsmedium•Channels can be restricted so that onlycertain processes can communicate on themChannelsSPiSPi Calculus: Basic Calculus: BasicDefinitionsDefinitionsChannel Example:A BcABProcess A communicates to Process B through ChannelABSPiSPi Calculus: Basic Definitions Calculus: Basic DefinitionsUnfortunately we can’t just say:Process A ӂ Listen on Channel AB for a Message MWe have to use SPi Calculus NotationPi Calc: Basic Notation (1)Pi Calc: Basic Notation (1)Process Grammar-OutputThe above is how we state “Output the messageM on Channel C and then run process P”SequentialOperatorPi Calc: Basic Notation (2)Pi Calc: Basic Notation (2)Process Grammar-Input C(x).PInput the message x on the channel Cand then run process P (P will have accessto x)Pi Calc: Basic Notation (3)Pi Calc: Basic Notation (3)Process Grammar-CompositionP|Q•A composition P|Q behaves as processes Pand Q running in parallel. Each may interactwith the other on channels known to both,or with the outside world, independently ofthe other.Pi Calc: Basic Notation (4)Pi Calc: Basic Notation (4)Process Grammar-Restriction(vn)P•A restriction (vn)P is a process thatmakes a new, private name n, andthen behaves as P. (Note that n isrestricted to P)Pi Calc: Restriction ExamplePi Calc: Restriction ExampleCAB is restricted to process A and BABcABProcess D cannot use cABD(vcAB)(A | B)Pi Calc: Basic ExamplePi Calc: Basic ExampleA basic example of a Protocolusing the notation we just learnedPrincipal A uses the channel AB to send a singlePrincipal A uses the channel AB to send a singlemessage M to Principal Bmessage M to Principal BChannelChannel ABABPrincipal APrincipal APrincipal BPrincipal BMMPi Calc: Basic ExamplePi Calc: Basic ExampleMother, I comebearing a gift. I'llgive you a hint: it'sin my diaper andit's not a toaster.*Pi Calc: Basic Example (2)Pi Calc: Basic Example (2)Message 1 A → B: M on cABChannel AB Principal A Principal BMMPi Calc: Basic Example (3)Pi Calc: Basic Example (3)A(M) ӂOutputProcess(Principal A)Is Defined AscAB A BMMOutput M onChannel AB*Pi Calc: Basic Example (4)Pi Calc: Basic Example (4)A(M) ӂcAB A BMMB ӂInputProcess(Principal B)ApplyF to xInput x fromChannel AB*Pi Calc: Basic Example (5)Pi Calc: Basic Example (5)cAB A BMMA(M) ӂB ӂInst(M) ӂRun ProcessA & B inparallelCreateChannel ABBasic Example Protocol Final (6)Basic Example Protocol Final (6)A(M) ӂB ӂInst(M) ӂPi Calc: Basic Example PropertiesPi Calc: Basic Example Properties1)Authenticity (Integrity)2)SecrecyWe will show why the basic protocol has these properties using informal and then formal syntaxPi Calc: Authenticity (2)Pi Calc: Authenticity (2)Process B always applies the function F to The message M, that A sends.A(M)=B =Inst(M) =AlwaysM*Why is that?Inst(M) ӂScope of theRestrictionRestriction onChannel ABPi Calc: Authenticity (3)Pi Calc: Authenticity (3)The restriction operator restrictsthe channel AB to principal A(M) and BThe Channel AB is Secure*Pi Calc: Authenticity (4)Pi Calc: Authenticity (4)Since only process A and B communicate oncAB, and the only thing being sent on thatchannel is M, F(x) is really always F(M)A(M)=B =Inst(M) =AlwaysMPi Calc: Authenticity (5)Pi Calc: Authenticity (5)An attacker cannot cause B to apply F to somemessage other than M.Pi Calc: SecrecyPi Calc: SecrecyA(M)=B =Inst(M) =The message M cannot be read in transit fromPrincipal A to Principal B(Since cAB is secure)Pi Calc: Secrecy (2)Pi Calc: Secrecy (2)A(M)=B =Inst(M) =If F does not reveal M, then the whole protocoldoes not reveal MPi Calc: Pi Calc: IndistinguishabilityIndistinguishabilityP 䍎㻃QThe behaviors of process P and Q are indistinguishablePi Calc: Pi Calc: IndistinguishabilityIndistinguishability (2) (2)P 䍎㻃QInternally P and Q might be different. However,a third process R cannot tell the different betweenrunning P and running Q.Pi Calc: Secrecy (Formally)Pi Calc: Secrecy (Formally)We can state the secrecy property using The concept of indistinguishability.If F(M) 󲰳 F(M') for all M and M', thenInst(M) 󲰳 Inst(M')If F does not reveal M, then the wholeprotocol does not reveal MPi Calc: Secrecy (Formally) (2)Pi Calc: Secrecy (Formally) (2)F(M) 󲰳 F(M') = F does not reveal MInst(M) 󲰳 Inst(M') = Protocol does not reveal M*Pi Calc: Authenticity (Formally)Pi Calc: Authenticity (Formally)To formally show authenticity for our basicprotocol we are going to compare the basicprotocol to a specification.A(M)=Bspec =Instspec(M) =Pi Calc: Authenticity: SpecificationPi Calc: Authenticity: SpecificationWe need to show that our protocol behaves thesame as the above specification.Inst(M) 󲰳 Instspec(M) *Pi Calc: Authenticity FormallyPi Calc: Authenticity FormallyBspec =B =AlwaysMAre these two indistinguishable?Yes, because x is always M since the cABis secure and M is the only thing sent on it.(Remember Informally: An attacker cannot cause B to apply F to some other message. )Pi Pi Calc:PropertiesCalc:PropertiesAuthenticity:Authenticity: Inst(M) 󲰳 Instspec(M), for all MSecrecy:Secrecy: Inst(M) 󲰳 Inst(M') if F(M) 󲰳 F(M'), for all M and M'.To sum upPi Calc: Channel EstablishmentPi Calc: Channel EstablishmentWide Mouth Frog