Protocol Composition Logic IIAnupam DattaFall 2007-0818739A: Foundations of Security and PrivacyProtocol Analysis TechniquesCrypto Protocol AnalysisFormal Models Computational ModelsProtocol LogicsModel CheckingInductive ProofsDolev-Yao(perfect cryptography)Random oracleProbabilistic process calculiProbabilistic I/O automata…Process Calculi…Applied Π-calculusBAN, PCLMurphi, AVISPAPaulson, MSRProtocol Composition Logic uIntuitionuFormalism• Protocol programming language• Protocol logic• Proof SystemuExample• Signature-based challenge-responseuProof techniquesTODAYExample: JFK ProtocoluRecall earlier lecture about JFK designuToday we will describe corresponding proof techniquesIngredient 1: Diffie-HellmanA → B: gaB → A: gb• Shared secret: gab• Authentication• Identity protectionIngredient 2: Challenge-ResponseA → B: m, AB → A: n, sigB{m, n, A}A → B: sigA{m, n, B}• Shared secret • Authentication• Identity protectionDH + Challenge-Response ISO 9798-3 protocol:A → B: ga, AB → A: gb, sigB{ga, gb, A}A → B: sigA{ga, gb, B}• Shared secret: gab• Authentication• Identity protectionm := gan := gbFormalized as sequential compositionIngredient 3: EncryptionEncrypt signatures to protect identities:A → B: ga, AB → A: gb, EK{sigB{ga, gb, A}}A → B: EK{sigA{ga, gb, B}}• Shared secret: gab• Authentication• Identity protection Formalized using abstraction-refinementuModular Proofs• Parallel Composition• Sequential CompositionuGeneric Template-style Proofs• Function variables• Higher-order logic extensionPCL Proof TechniquesParallel Composition of ProtocolsuThe parallel composition Q1 | Q2 of protocols Q1 and Q2 is the union of the sets of roles of Q1 and Q2.uExample: • IKEv2 | SSLCompositional Proofs: IntuitionuProtocol specific reasoning• “if honest Bob generates a signature of the form sigB {m, n, A}, – he sends it as part of msg2 …”• Could break: Bob’s signature from one protocol could be used to attack another• PCL proof system: Invariant ruleuProtocol independent reasoning• Axiom stating unforgeability of signatures• Still good: unaffected by composition• All other axioms and proof rules for PCLProof TreeAxiomINV ruleOther rulesSecurity propertyInv |-AuthAuthQ1 |- InvInvBulk of proof reusedAdditional work to prove Q2|- InvQ1 | Q2 |-InvTheorem: If Q |- Inv and Q’ |- Inv, then Q | Q’|-Inv[DDMP CSF’03 -> JCS Special Issue, MFPS’03]Parallel Composition TheoremIF •Q1 satisfies security property Ψ in isolation• Q2 respects the invariants Γ of Q1 used in the proof of security property ΨTHEN•Q1 | Q2 also satisfies security property ΨSequential Composition of ProtocolsuRun protocols in sequenceuExamples• Key exchange followed by secure sessions that use the exchanged key• Diffie-Hellman followed by Challenge-Response = ISO-9798-3ISO-9798-3 Key ExchangeuAuthentication• Do we need to prove it from scratch?uShared secret: gabA Bga, Agb, sigB{ga, gb, A}sigA{ga, gb, B}Goal: Combine proofs of Diffie-Hellman and challenge-response sub-protocolsAbstract challenge response u Free variables m and n instead of noncesu Modal form: φ [ actions ] ϕ• precondition: Fresh(A,m)• actions: [ InitACR ]A• postcondition: Honest(B) ⊃ Authenticationu Secrecy is proved from properties of Diffie-HellmanInitACR(A, X, m) = [send A, X, {m};receive X, A, {x, sigX{m, x}};send A, X, sigA{m, x}};]RespACR(B, n) = [receive Y, B, {y};send B, Y, {n, sigB{y, n}};receive Y, B, sigY{y, n}};]Diffie-Hellman: PropertyuFormulautrue [ new a ] AFresh(A, ga)uDiffie-Hellman property:uCan compute gabgiven ga and b or gb and auCannot compute gabgiven ga and gbChallenge Response: PropertyuModal form: ϕ [ actions ]Pψ• precondition: Fresh(A,m)• actions: [ Initiator role actions ]A • postcondition: Honest(B) ⊃ ActionsInOrder(send(A, {A,B,m}), receive(B, {A,B,m}), send(B, {B,A,{n, sigB{m, n, A}}}), receive(A, {B,A,{n, sigB{m, n, A}}}) )Composition: DH+CR = ISO-9798-3• Additive CombinationuDH post-condition matches CR preconditionuSequential Composition:• Substitute gafor m in CR to obtain ISO.• Apply composition rule• ISO initiator role inherits CR authentication.uDH secrecy is also preserved• Proved using another application of composition rule.• Nondestructive Combination• DH and CR satisfy each other’s invariantsDefinition of Sequential CompositionSequential Composition TheoremuBoth protocols should satisfy each other’s invariants (similar to parallel composition)uPost-condition of first should match pre-condition of second protocoluModular Proofs• Parallel Composition• Sequential CompositionuGeneric Template-style Proofs• Function variables• Higher-order logic extensionPCL Proof TechniquesProtocol TemplatesuProtocols with function variables instead of specific cryptographic operationsuIdea: One template can be instantiated to many protocols uAdvantages:• proof reuse• design principles/patterns[DDMP CSF’04]ExampleA → B: mB → A: n, F(B,A,n,m)A → B: G(A,B,n,m)A → B: mB → A: n,EKAB(n,m,B)A → B: EKAB(n,m)A → B: mB → A: n,HKAB(n,m,B) A → B: HKAB(n,m,A) A → B: mB → A: n, sigB(n,m,A)A → B: sigA(n,m,B)Challenge-Response TemplateISO-9798-2ISO-9798-3SKID3InstantiationsExtending FormalismuLanguage Extensions• Add function variables to term language for cords and logic (HOL)uSemantics• Q |= f ó sQ |= sf , for all substitutions seliminating all function variablesuSoundness Theorem • Every provable formula is validAbstraction-Instantiation Method(1)uCharacterizing protocol concepts• Step 1: Under hypotheses about function variables and invariants, prove security property of template • Step 2: Instantiate function variables to cryptographic operations and prove hypotheses.uBenefit: • Proof reuseExampleChallenge-Response TemplateA → B: mB → A: n, F(B,A,n,m)A → B: G(A,B,n,m)•Step 1:•Hypotheses: Function F(B,A,n,m) can be computed only by B or A,…•Property: Mutual authentication•Step 2:•Instantiate F() to signature, keyed hash, encryption (ISO-9798-2,3, SKID3)•Satisfies hypotheses => Guarantees mutual authenticationProof StructureTemplateaxiom hypothesisInstanceDischarge hypothesisProof reuseAbstraction-Instantiation Method(2)uCombining protocol templatesIf protocol P is a hypotheses-respecting instance of two different templates, then it has the properties of both.uBenefits:• Modular proofs of