DOC PREVIEW
UT CS 395T - Analyzing SET with Inductive Method

This preview shows page 1-2-16-17-18-34-35 out of 35 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 35 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 35 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 35 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 35 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 35 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 35 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 35 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 35 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

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 AnalysisProve correctness instead of looking for bugs• Use higher-order logic to reason about all possibleprotocol executionsNo finite bounds• Any number of interleaved runs• Algebraic theory of messages• No finite bounds on the attackerMechanized proofs• Automated tools can fill in parts of proofs[Paulson]Inductive MethodDefine the set of protocol traces• Given a protocol, a trace is one possible sequence of events, including attacker actionsProve 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 InductionUsual 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 AnalysisGiven 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 PaulsonIsabelle theorem prover• General tool; security protocols work since 1997Many 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.htmlIsabelleAutomated support for proof development• Higher-order logic• Serves as a logical framework• Supports ZF set theory & HOL• Generic treatment of inference rulesPowerful simplifier & classical reasonerStrong 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 protocolsOperational model for honest agents• Similar to pi calculus or protocol composition logicAlgebraic 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 attackerProofs mechanized using Isabelle/HOLA Few DefinitionsTraces• 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 evsInformation 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 EventsSeveral 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 buyCardholders and merchants must register and receive electronic credentials• Proof of identity• Evidence of trustworthinessExpensive development effort, little deploymentIsabelle verification byLarry Paulson, Giampaolo Bella, and Fabio MassacciSET DocumentationBusiness Description• General overview• 72 pagesProgrammer’s Guide• Message formats & English description of actions• 619 pagesFormal 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 ProtocolsSeveral sub-protocolsComplex cryptographic primitives• Dual signatures for partial sharing of secretsMany types of principals• Cardholder, Merchant, Payment Gateway, CAs1000 pages of specification and descriptionSET is


View Full Document

UT CS 395T - Analyzing SET with Inductive Method

Documents in this Course
TERRA

TERRA

23 pages

OpenCL

OpenCL

15 pages

Byzantine

Byzantine

32 pages

Load more
Download Analyzing SET with Inductive Method
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Analyzing SET with Inductive Method and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Analyzing SET with Inductive Method 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?