Protocol Composition Logic (PCL)Protocol Analysis TechniquesProtocol LogicsBAN Logic (1)BAN Logic (2)TodayProtocol Composition LogicRoadmapExample: Challenge-ResponseFormalizing the ApproachProtocol Programming LanguageTermsActionsChallenge-Response ProgramsProtocol ExecutionProcess Calc. Op. SemanticsReaction stepsAttacker capabilitiesPCL: SyntaxChallenge-Response PropertyPCL: SemanticsSemantics of action formulasSemantics of other formulasProof SystemSample axioms about actionsReasoning about knowledge Encryption and signatureSample inference rulesHonesty rule (example use)Correctness of CRCorrectness of CR – step 1Correctness of CR – step 2Correctness of CR – HonestyCorrectness of CR – step 3Correctness of CR – step 4Freshness and temporal ordering rulesWe have a proof. So what?PCL Proof TechniquesModular Analysis / CompositionSlide Number 40Proof TreeGeneric Template-style ProofsProtocol TemplateTemplate Proof MethodProof StructureExtending FormalismSummarySlide Number 48Protocol Composition Logic (PCL)Anupam DattaFall 2007-0815-819: Logics and Languages for SecurityProtocol 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, MSR18-739: Foundations of Security and PrivacyProtocol LogicsBAN LogicA Logic of Authenticationby Michael Burrows, Martin Abadi, Roger Needham (1989)Historically, the first logic for reasoning about security protocolsSyntax and proof system (axioms and rules) for proving authentication properties (semantics added in a later paper)BAN Logic (1)Advantages• Proofs are relatively short (~ 2-3 pages)– cf. Paulson’s inductive proofs• Proofs follow protocol design intuition– cf. model-checking, low-level theorem-proving• Relatively easy to use– Still taught widely in security courses • No explicit reasoning about traces and intruder– cf. Paulson’s inductive proofsBAN Logic (2)Disadvantages• Not sound wrt now accepted model of protocol execution and attack– Protocols “proved” secure may be insecuree.g. NS was proved secure using BAN• Protocols are modeled using logical formulas (idealizationstep) as opposed to state machines or programs• Many uses of non-standard logical concepts – Jurisdiction, control, “belief”, messages = propositions• Only authentication properties, not secrecy• Applicable to restricted classes of protocolsSee Harper’s slides on BAN from last lectureTodayProtocol Composition Logic (PCL)• Developed over the last few years (2001- 07)• Retain advantages of BAN; rectify deficiencies• Semantic model similar to Paulson’s Inductive Method• New proof techniques– Modular proofs– Cryptographic soundnessProtocol Composition LogicA logic for proving security of network protocolsIllustrates use of programming language methods in computer security• Concurrency theory– Network protocols are concurrentprograms • Floyd-Hoare style logic– Before-after assertions15-812: Semantics of programming languagesRoadmapIntuitionFormalism• Protocol programming language• Protocol logic• Proof SystemExample• Signature-based challenge-responseProof techniquesFormulated by Datta, Derek, Durgin, Mitchell, PavlovicExample: Challenge-ResponseA Bm, An, sigB {m, n, A}sigA {m, n, B}Alicereasons: if Bobis honest, then:• only Bobcan generate his signature • if Bobgenerates a signature of the form sigB {m, n, A}, – he sends it as part of msg2 of the protocol, and – he must have received msg1 from AliceAlicededuces: Received (B, msg1) Λ Sent (B, msg2)Formalizing the ApproachLanguage for protocol description• Arrows-and-messages are informal.Protocol Operational Semantics• How does the protocol execute?Protocol logic• Stating security properties.Proof system• Formally proving security properties.Protocol Programming LanguageA protocol is described by specifying a “program” for each role– Server = [receive x; new n; send {x, n}]Building blocks• Terms (think “messages”)– names, nonces, keys, encryption, …• Actions (operations on terms)– send, receive, pattern match, …Termst ::= c constant termx variableN nameK keyt, t tuplingsigK {t} signatureencK {t} encryptionExample: x, sigB {m, x, A} is a termTyped term algebraActionssend t; send a term treceive x; receive a term into variable xmatch t/p(x); match term t against p(x)A program or cord is a sequence of actionsNotation:• we often omit match actions• receive sigB {A, n} = receive x; match x/sigB {A, n}Challenge-Response ProgramsA Bm, An, sigB {m, n, A}sigA {m, n, B}InitCR(A, X) = [new m;send A, X, {m, A};receive X, A, {x, sigX {m, x, A}};send A, X, sigA {m, x, X}};]RespCR(B) = [receive Y, B, {y, Y};new n;send B, Y, {n, sigB {y, n, Y}};receive Y, B, sigY {y, n, B}};]Protocol Execution Initial configuration Protocol is a finite set of roles Set of principals and keys Assignment of ≥1 role to each principal Run (trace)new xsend {x}Breceive {x}BABCreceive {z}Bnew zsend {z}BProcess calculus operational semanticsProcess Calc. Op. SemanticsCord space is a multiset of cordsCords may react• via communication• via internal actionsSample reaction steps:• Communication:[send t; S]X | [receive x; T]Y ⇒ [S]X | [T(t/x) ]Y• Matching:[ match p(t)/p(x); S ]X ⇒ [S(t/x) ]XReaction stepsAttacker capabilitiesControls complete network• Can read, remove, inject messages Fixed set of operations on terms• Pairing• Projection• Encryption with known key• Decryption with known key• …Commonly referred to as “Dolev-Yao” attackerPCL: SyntaxAction formulasa ::= Send(P,t) | Receive (P,t) | Verify(P,T) | …Formulasϕ ::= a | Has(P,t) | Honest(N) | ¬ϕ | ϕ1∧ϕ2 | ∃x ϕ| a < a | …Modal formulaϕ [ actions] P ϕExampleHas(X, secret) ⊃ ( X = A ∨ X = B)Specifying secrecyChallenge-Response PropertySpecifying authentication for Initiatortrue [ InitCR(A, B) ] A Honest(B) ⊃(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}}}))Semantics: Property must hold in all protocol traces (similar to Paulson’s Inductive Method)PCL: SemanticsProtocol Q• Defines set of roles (e.g,