Compositional Protocol LogicOutlineFloyd-Hoare LogicWhile ProgramsAssignment and Rule of ConsequenceSimple ExamplesConditionalSequenceLoop InvariantExample: Compute d=x-yGoal: Logic for Security ProtocolsIntuitionAlice’s “View” of the ProtocolExample: Challenge-ResponseProtocol Composition LogicTermsActionsChallenge-Response ThreadsExecution ModelAction FormulasFormulasTrace SemanticsSpecifying AuthenticationSpecifying SecrecyProof SystemSample AxiomsReasoning About CryptographySample Inference RulesHonesty RuleCorrectness of Challenge-Response1: A Reasons about Own Actions2: Properties of SignaturesHonesty InvariantReminder: Honesty Rule3: Use Honesty Rule4: Nonces Imply Temporal OrderComplete ProofProperties of Proof SystemWeak Challenge-Response1: A Reasons about Own Actions2: Properties of SignaturesHonesty Invariant3: Use Honesty RuleFailed Proof and CounterexampleFurther Work on Protocol LogicCS 395TCompositional Protocol LogicOutlineFloyd-Hoare logic of programs• Compositional reasoning about properties of programsDDMP protocol logic• Developed by Datta, Derek, Mitchell, and Pavlovic for logical reasoning about security propertiesFloyd-Hoare LogicMain idea: before-after assertions• F <P> G– If F is true before executing P, then G is true afterTotal correctness or partial correctness• Total correctness: F [P] G– If F is true, then P will halt and G will be true• Partial correctness: F {P} G– If F is true and if P halts, then G will be trueWhile ProgramsP ::= x := e |P ; P |if B then P else P |while B do Pwhere x is any variablee is any integer expressionB is a Boolean expression(true or false)Assignment and Rule of ConsequenceAssignment axiom: F(t) { x := t } F(x)• If F holds for t, and t is assigned to x, then F holds for x aftewards• This assumes that there is no aliasing!• Examples:7=7 { x := 7 } x=7(y+1)>0 { x := y+1 } x>0x+1=2 { x := x+1 } x=2Rule of consequence:If F { P } G and F’ → F and G → G’,then F’ { P } G’Simple Examples Assertion: y>0 { x := y+1 } x>0Proof:(y+1)>0 { x := y+1 } x>0 (assignment axiom)y>0 { x := y+1 } x>0 (rule of consequence) Assertion: x=1 { x := x+1 } x=2Proof:x+1=2 { x := x+1 } x=2 (assignment axiom)x=1 { x := x+1 } x=2 (rule of consequence)y>0 → y+1>0ConditionalF & B { P } GF &¬B { Q } GF { if B then P else Q } G• Example:true { if y ≥ 0 then x := y else x := -y } x ≥ 0SequenceF { P } GG { Q } HF { P; Q } H• Example:x=0 { x := x+1 ; x := x+1 } x=2Loop InvariantF & B { P } FF { while B do P } F &¬B • Example:true { while x ≠ 0 do x := x-1 } x=0F is the loop invariant; it should hold before and after the loop bodyExample: Compute d=x-y Assertion: y≤x {d:=0; while (y+d)<x do d := d+1} y+d=x Proof:• Choose loop invariant F = y+d≤xy+d≤x & B {Q} y+d≤xy+d≤x {while B do Q} y+d≤x &¬B –Important: proving a property of the entire loop has been reduced to proving a property of one iteration of the loop• To prove y+d≤x & B {Q} y+d≤x, use assignment axiom and sequence rulePBQAfter loop execution, y+d≤x&¬(y+d<x), thus y+d=xGoal: Logic for Security Protocols“Floyd-Hoare” reasoning about security properties• Would like to derive global properties of protocols from localassertions about each protocol participant• Use a rigorous logical framework to formalize the reasoning that each participant carries out Compositionality is important• Security properties must hold even if the protocol is executed in parallel with other protocols• Compositionality is the main advantage of process calculi and protocol logicsIntuition Reason about local information• I chose a fresh, unpredictable number• I sent it out encrypted• I received it decrypted • Therefore: someone decrypted it Incorporate knowledge about protocol into reasoning• According to the protocol specification, server only sends m if it received m’• If server not corruptand I receive m signed by server, then server received m’{Na}pk(B)ANaAlice’s “View” of the ProtocolHonest principals,attackerProtocolspecPrivate dataSent and received messagesExample: Challenge-ResponseABm, A Alice’s reasoning:• If Bob is honest, then only Bob can generate his signature • If honest Bob generates a signature of the form sigB{m, n, A}, then1. Bob must have received m, A from Alice2. Bob sent sigB{m, n, A} as part of his 2ndmessage Alice concludes:• Received(B,msg1) & Sent(B,msg2)n, sigB{m, n, A}sigA{m, n, B}protocol-independent reasoningprotocol-specific reasoningProtocol Composition Logic[Datta et al.]A formal language for describing protocols• Terms and actions instead of informal arrows-and-messages notationOperational semantics• Describe how the protocol executesProtocol logic• State security properties (in particular, secrecy and authentication)Proof system• Axioms and inference rules for formally proving security propertiesTermst ::= c | constant x | variableN | nameK | keyt, t | tuplesigK{t} | signatureencK{t} encryptionActionsnew m generate fresh valuesend U, V, t send term t from U to Vreceive U, V, x receive term and assign into variable xmatch t/p(x) match term t against pattern p(x) A thread is a sequence of actions• Defines the “program” for a protocol participant, i.e., what messages he sends and receives and the checks he performs• For notational convenience, omit “match” actions– Write “receive sigB{A, n}” instead of “receive x; match x/sigB{A, n}”Challenge-Response ThreadsABm, 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};]Execution ModelA protocol is a finite set of roles• Initial configuration specifies a set of principals and keys; assignment of ≥1 role to each principalA run is a concurrent execution of the roles• Models a protocol session• Send and receive actions are matched upPosition in runsend{x}Bnew xAreceive{x}BBreceive{z}Bsend{z}Bnew zCAction FormulasPredicates over action sequencesa ::= Send(X,m) | Message m was sent in thread XReceive(X,m) | Message m was received in thread XNew(X,t) | Term t was generated as new in XDecrypt(X,t) |
View Full Document
Unlocking...