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 OrderProperties of Proof SystemWeak Challenge-ResponseSlide 40Slide 41Slide 42Slide 43Failed Proof and CounterexampleFurther Work on Protocol LogicCompositional Protocol LogicCS 395TOutlineFloyd-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 variable e is any integer expression B 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>0 x+1=2 { x := x+1 } x=2Rule of consequence: If F { P } G and F’ F and G G’, then F’ { P } G’Simple ExamplesAssertion: y>0 { x := y+1 } x>0 Proof: (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=2 Proof: x+1=2 { x := x+1 } x=2 (assignment axiom) x=1 { x := x+1 } x=2 (rule of consequence)y>0 y+1>0Conditional F & B { P } G F &B { Q } GF { if B then P else Q } G•Example: true { if y 0 then x := y else x := -y } x 0Sequence F { P } G G { Q } H F { P; Q } H•Example: x=0 { x := x+1 ; x := x+1 } x=2Loop Invariant F & B { P } F F { 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-yAssertion: yx {d:=0; while (y+d)<x do d := d+1} y+d=xProof:•Choose loop invariant F = y+dx y+dx & B {Q} y+dx y+dx {while B do Q} y+dx &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+dx & B {Q} y+dx, use assignment axiom and sequence ruleP B QAfter loop execution, y+dx &(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 local assertions 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 logicsIntuitionReason about local information•I chose a fresh, unpredictable number•I sent it out encrypted•I received it decrypted •Therefore: someone decrypted itIncorporate knowledge about protocol into reasoning•According to the protocol specification, server only sends m if it received m’•If server not corrupt and I receive m signed by server, then server received m’ A{Na}pk(B)NaAlice’s “View” of the ProtocolHonest principals,attackerProtocolspecPrivate dataSent and received messagesExample: Challenge-ResponseA Bm, An, sigB{m, n, A} sigA{m, n, B}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 2nd messageAlice concludes:•Received(B,msg1) & Sent(B,msg2)protocol-independent reasoningprotocol-specific reasoningProtocol Composition LogicA 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 properties[Datta et al.]Terms t ::= c | constant x | variableN | nameK | keyt, t | tuplesigK{t} | signatureencK{t} encryptionActions new m generate fresh value send U, V, t send term t from U to V receive U, V, x receive term and assign into variable x match 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 ThreadsInitCR(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};]A Bm, An, sigB{m, n, A} sigA{m, 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 upnew xsend{x}Breceive{x}BABCPosition in runreceive{z}Bnew zsend{z}BAction FormulasPredicates over action sequencesa ::= Send(X,m) | Message m was sent in thread X Receive(X,m) | Message m was received in thread X New(X,t) | Term t was generated as new in X Decrypt(X,t) | Term t was decrypted in
View Full Document
Unlocking...