Security in Process CalculiOverviewPi CalculusA Little Bit of HistoryPi Calculus SyntaxModeling Secrecy with ScopingSecrecy as EquivalenceAnother Formulation of SecrecyModeling Authentication with ScopingSpecifying AuthenticationA Key Establishment ProtocolKey Establishment in Pi CalculusApplied Pi CalculusApplied Pi Calculus: TermsApplied Pi Calculus: ProcessesModeling Crypto with FunctionsMore Equational TheoriesYet More Equational TheoriesDynamically Generated DataBetter Protocol with CapabilitiesCS 395TSecurity in Process CalculiOverviewPi calculus• Core language for parallel programming• Modeling security via name scopingApplied pi calculus• Modeling cryptographic primitives with functions and equational theories• Equivalence-based notions of security• A little bit of operational semantics• Security as testing equivalencePi Calculus[Milner et al.]Fundamental language for concurrent systems• High-level mathematical model of parallel processes• The “core” of concurrent programming languages• By comparison, lambda-calculus is the “core” of functional programming languagesMobility is a basic primitive • Basic computational step is the transfer of a communication link between two processes• Interconnections between processes change as they communicateCan be used as a general programming languageA Little Bit of History1980: Calculus of communicating systems (CCS)1992: Pi calculus[Milner, Parrow, Walker]• Ability to pass channel names between processes1998: Spi calculus [Abadi, Gordon]• Adds cryptographic primitives to pi calculus• Security modeled as scoping• Equivalence-based specification of security properties• Connection with computational models of cryptography2001: Applied pi calculus [Abadi, Fournet]• Generic functions, including crypto primitives[Milner]Pi Calculus SyntaxTerms• M, N ::= xvariables| nnamesProcesses• P,Q ::= nil empty process| ū〈N〉.Psend term N on channel u| u(x).Preceive term from channel P and assign to x| !Preplicate process P| P|Qrun processes P and Q in parallel| (νn)Prestrict name n to process P}Let u range overnames and variablesModeling Secrecy with ScopingA sends M to B over secure channel cA BMchannel cA(M) = c〈M〉B = c(x).nilP(M) = (νc)(A(M)|B)This restriction ensures that channel c is “invisible” to any process except A and B(other processes don’t know name c)-Secrecy as EquivalenceA(M) = c〈M〉.nilB = c(x).nilP(M) = (νc)(A(M)|B)Without (νc), attacker could run process c(x) and tell the differencebetween P(M) and P(M’)-P(M) and P(M’) are “equivalent” for any values of M and M’• No attacker can distinguish P(M) and P(M’)Different notions of “equivalence”• Testing equivalence or observational congruence• Indistinguishability by any probabilistic polynomial-time Turing machineAnother Formulation of SecrecyA(M) = c〈M〉.nilB = c(x).nilP(M) = (νc)(A(M)|B)-No attacker can learn name n from P(n)• Let Q be an arbitrary attacker process, and suppose it runs in parallel with P(n)• Specification of secrecy:For any process Q in which n does not occur free, P(n) | Q will never output nModeling Authentication with ScopingA sends M to B over secure channel cB announces received value on public channel dA BA(M) = c〈M〉B = c(x).d〈x〉P(M) = (νc)(A(M)|B)MMchannel cchannel d--Specifying AuthenticationA(M) = c〈M〉B = c(x).d〈x〉P(M) = (νc)(A(M)|B)--Specification of authentication:For any value of M, if B outputs M on channel d, then A previously sent M on channel cA Key Establishment ProtocolA BSCASCSBCreate newchannel CABSend name CABSend name CABMchannel dSend data on CABM1. A and B have pre-established pairwise keys with server S Model these keys as names of pre-existing communication channels3. A sends M to B encrypted with the new key, B outputs M2. A creates a new key and sends it to S, who forwards it to B Model this as creation of a new channel nameKey Establishment in Pi CalculusA(M) =S =B =P(M) = (νcAS)(νcSB)(A(M)|B|S).cSB〈x〉cSB(x)__Note communication on a channelwith a dynamically generated nameA BSCASCSBSend name CABSend name CABMchannel dSend data on CABM.d〈y〉_Create newchannel CAB(νcAB)cAS〈cAB〉__cAS(x).cAB〈M〉__.x(y)Applied Pi CalculusIn pi calculus, channels are the only primitiveThis is enough to model some forms of security• Name of a communication channel can be viewed as an “encryption key” for traffic on that channel– A process that doesn’t know the name can’t access the channel• Channel names can be passed between processes– Useful for modeling key establishment protocolsTo simplify protocol specification, applied pi calculus adds functions to pi calculus• Crypto primitives modeled by functions and equationsApplied Pi Calculus: TermsM, N ::= xVariable| nName| f(M1,...,Mk)Function applicationStandard functions• pair(), encrypt(), hash(), …Simple type system for terms• Integer, Key, Channel〈Integer〉, Channel〈Key〉Applied Pi Calculus: ProcessesP,Q ::= nil empty process| ū〈N〉.Psend term N on channel u| u(x).Preceive from channel P and assign to x| !Preplicate process P| P|Qrun processes P and Q in parallel| (νn)Prestrict name n to process P| if M = Nconditionalthen P else QModeling Crypto with FunctionsIntroduce special function symbols to model cryptographic primitivesEquational theory models cryptographic propertiesPairing• Functions pair, first, second with equations:first(pair(x,y)) = xsecond(pair(x,y)) = ySymmetric-key encryption• Functions symenc, symdec with equation:symdec(symenc(x,k),k)=xMore Equational TheoriesPublic-key encryption• Functions pk,sk generate public/private key pair pk(x),sk(x) from a random seed x• Functions pdec,penc model encryption and decryption with equation:pdec(penc(y,pk(x)),sk(x)) = y• Can also model “probabilistic” encryption:pdec(penc(y,pk(x),z),sk(x)) = y Hashing• Unary function hash with no equations• hash(M) models applying a one-way function to term MModels random salt (necessary for semantic security)Yet More Equational TheoriesPublic-key digital signatures• As before, functions pk,sk generate public/private key pair pk(x),sk(x) from a random seed x• Functions sign,verify model signing and verification with equation:verify(y,sign(y,sk(x)),pk(x)) = yXOR• Model self-cancellation property with
View Full Document
Unlocking...