Analyzing SET with Inductive MethodTheorem Proving for Protocol AnalysisInductive MethodTwo Forms of InductionInduction for Protocol AnalysisWork by Larry PaulsonIsabelleAgents and MessagesProtocol SemanticsA Few DefinitionsProtocol EventsAttacker Capabilities: AnalysisAttacker Capabilities: SynthesisEquations and ImplicationsAttacker EventsCorrectness ConditionsSecure Electronic Transactions (SET)SET DocumentationDual SignaturesVerifying the SET ProtocolsSET TerminologySET Certificate HierarchyPlayersSET Consists in 5 SubprotocolsCardholder RegistrationSET Registration SubprotocolCertificate Request in IsabelleSecrecy of Session Keys and NoncesSET Purchase SubprotocolSET Messages (Purchase Phase)Dual Signatures for PrivacyPurchase Request in IsabelleSET Proofs are ComplicatedInductive Method: Pros & ConsCS 395TAnalyzing SET with Inductive MethodTheorem Proving for Protocol AnalysisProve correctness instead of looking for bugs• Use higher-order logic to reason about all possibleprotocol executionsNo finite bounds• Any number of interleaved runs• Algebraic theory of messages• No finite bounds on the attackerMechanized proofs• Automated tools can fill in parts of proofs[Paulson]Inductive MethodDefine the set of protocol traces• Given a protocol, a trace is one possible sequence of events, including attacker actionsProve correctness by induction• For every state in every trace, prove that no security condition fails– Works for safety properties only• Induction is on the length of the traceTwo Forms of InductionUsual form for ∀n∈Nat. P(n)• Base case: P(0)• Induction step: P(x) ⇒ P(x+1)• Conclusion: ∀n∈Nat. P(n)Minimal counterexample form• Assume: ∃x [ ¬P(x) ∧∀y<x. P(y) ]• Prove contradiction• Conclusion: ∀n∈Nat. P(n)Both equivalent to “the natural numbers are well-ordered”Induction for Protocol AnalysisGiven a set of traces, choose shortest sequence to a bad state• Bad state = state in which an invariant is violated• Assume all steps before that are OK• Derive contradiction– Consider all possible actions taken at this stepAll states are good Bad stateWork by Larry PaulsonIsabelle theorem prover• General tool; security protocols work since 1997Many case studies of security protocols• Verification of SET protocol (6 papers)• Kerberos (3 papers)• TLS protocol• Yahalom protocol, smart cards, etchttp://www.cl.cam.ac.uk/users/lcp/papers/protocols.htmlIsabelleAutomated support for proof development• Higher-order logic• Serves as a logical framework• Supports ZF set theory & HOL• Generic treatment of inference rulesPowerful simplifier & classical reasonerStrong support for inductive definitionsAgents and Messagesagent A,B,… = Server | Friend i| Spymsg X,Y,… = Agent A|NonceN|KeyK|{X,Y}|Crypt(K) XTyped, free term algebra, …Protocol Semantics“Set of event traces” semantics for protocolsOperational model for honest agents• Similar to pi calculus or protocol composition logicAlgebraic theory of messages defines attacker• Primitive operations: encrypt, decrypt, …• Inductive closure of the intercepted messages under primitive operations defines the set of all messages available to the attackerProofs mechanized using Isabelle/HOLA Few DefinitionsTraces• A protocol is a set of traces• A trace is a sequence of events• Inductive definition involves implications if ev1, …, evn∈ evs, then add ev’ to evsInformation from a set of messages• parts H : parts of messages in H• analz H : parts of messages in H that can belearned by attacker– Not every message part can be learned by attacker!• synth H : messages that can be constructed from HProtocol EventsSeveral types of events• A sends B message X• A receives X• A stores XIf ev is a trace and Na is unused, addSays A B Crypt(pk B){A,Na}A→B {A,NA}pk(B)If Says A’ B Crypt(pk B){A,X} ∈ evand Nb is unused, addSays B A Crypt(pk A){Nb,X}B→A {NB,NA}pk(A)A→B {NB}pk(B)If Says ...{X,Na}... ∈ ev , addSays A B Crypt(pk B){X}Attacker Capabilities: AnalysisX ∈H⇒X∈ analzH{X,Y} ∈ analzH⇒X∈ analzH{X,Y} ∈ analzH⇒Y∈ analzHCryptX K ∈ analzH&K-1∈ analzH⇒X∈ analzHanalzHis what attacker can learn from HAttacker Capabilities: SynthesissynthHis what attacker can create from Hinfinite set!X ∈H⇒X∈ synthHX∈ synthH & Y∈ synthH ⇒ {X,Y} ∈ synthHX∈ synthH & K∈ synthH ⇒ Crypt(K) X∈ synthHEquations and Implicationsanalz(analzH) = analzHsynth(synthH) = synthHanalz(synthH) = analzH∪ synthHsynth(analzH) = ???Nonce N∈ synthH⇒ Nonce N∈HCrypt (K) X∈ synthH⇒ Crypt (K) X∈HorX∈ synthH& K∈HBut only if keys are atomicAttacker EventsIf X∈ synth(analz(spiesevs)),add Says Spy B XX is not secret because attacker can constructit from the parts he learned from eventsevs(attacker announces all secrets he learns)Correctness ConditionsIfSays B A {Nb,X}pk(A)∈evs&Says A’ B {Nb}pk(B)∈evs,Then Says A B {Nb}pk(B)∈evsIf B thinks he’s talking to A,then A must think she’s talking to BSecure Electronic Transactions (SET)Goal: privacy of online credit card transactions• Merchant doesn’t learn credit card details• Bank (credit card issuer) doesn’t learn what you buyCardholders and merchants must register and receive electronic credentials• Proof of identity• Evidence of trustworthinessExpensive development effort, little deploymentIsabelle verification byLarry Paulson, Giampaolo Bella, and Fabio MassacciSET DocumentationBusiness Description• General overview• 72 pagesProgrammer’s Guide• Message formats & English description of actions• 619 pagesFormal Protocol Definition• Message formats & the equivalent ASN.1 definitions• 254 pagesTotal: 945 pagesDual Signatures Link two messages sent to different receivers Each receiver can only read one message• Alice checks (message1, digest2, dual sig)• Bob checks (message2, digest1, dual sig)MESSAGE 1DIGEST 1NEW DIGESTHASH 1 & 2WITH SHAMESSAGE 2DIGEST 2CONCATENATE DIGESTSTOGETHERHASH WITH SHA TOCREATE NEW DIGESTSIGN NEW DIGESTWITH SIGNER’S PRIVATE KEYPRIVATE KEYDUAL SIGNATUREVerifying the SET ProtocolsSeveral sub-protocolsComplex cryptographic primitives• Dual signatures for partial sharing of secretsMany types of principals• Cardholder, Merchant, Payment Gateway, CAs1000 pages of specification and descriptionSET is
View Full Document