Computational Soundness of Formal ModelsBridging the Gap (Again)Goal: Soundness of Formal AnalysisState of the ArtOutlineIND-CCA in Multi-User SettingSimple Protocol LanguageAbstract vs. Concrete ExecutionAbstract vs. Concrete AdversaryEquivalence of Concrete & AbstractConcrete and Abstract TracesHow Can This Fail?Main TheoremProof OutlineConstructing Abstract AdversaryReduction to IND-CCAOverview of ReductionWhat’s Illegal in Abstract Model?What if Encryption is Malleable?Winning the CCA Game (Simplified)SummaryCS 395TComputational Soundness ofFormal ModelsBridging the Gap (Again)Cryptography: computational constructions •Define actual algorithms operating on bit strings•For example, RSA is defined as a triple of algorithms–Key generation: public key is (n,e), private key is d where n=pq for some large primes p,q; ed=1 mod (p-1)(q-1)–Encryption of m: me mod n–Decryption of c: cd mod nFormal model: axiomatic interpretation of crypto•Instead of defining cryptographic algorithms, simply say that they satisfy a certain set of properties–Given ciphertext, obtain plaintext if have exactly the right key–Cannot learn anything from ciphertext without the right keyGoal: Soundness of Formal Analysis Prove that axioms assumed in the formal model are true for some cryptographic constructionsFormal proofs must be sound in following sense:•For any attack in concrete (computational) model…•…there is matching attack in abstract (formal) model•…or else the concrete attack violates computational security of some cryptographic primitiveIf we don’t find an attack in the formal model, then no computational attack exists–More precisely, probability that a computational attack exists is negligibleState of the Art Abadi, Rogaway. “Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption)”. J. Cryptology, 2002.•Symmetric encryption only, passive adversaryMicciancio, Warinschi. “Completeness Theorems for the Abadi-Rogaway Logic of Encrypted Expressions”. JCS 2004.•Fixes some bugs in the Abadi-Rogaway paper•Notion of “confusion-free” encryptionMicciancio, Warinschi. “Soundness of Formal Encryption in the Presence of Active Adversaries”. TCC 2004.•Public-key encryption, active adversaryWe’ll look at this paper todayOutlineDefine what it means for an encryption scheme to be secure against adaptive chosen-ciphertext attack in the multi-user settingDefine a formal language for describing protocolsDefine concrete trace semantics for protocols•Actual execution traces of protocols obtained by instantiating nonces with bit strings, etc.•Traces include actions of the concrete adversaryShow that almost every action of concrete adversary maps to an action of abstract adversary•This will follow from security of encryption schemeIND-CCA in Multi-User Setting[Boldyreva, Bellare, Micali]adversaryusersm0m1Left-right selector LR(m0,m1,b)(returns m0 or m1 depending on bit b)1. Generate n public-private key pairs (pki,ski); give public keys to adversary A. pk1 … pkn b…2. A may send any two plaintexts m0 and m1 to any user. A receives encpki(mb).mo, m1 An encryption oracle for every key pair 3. A may send any c (not received previously). If c= encpkj(m), A receives m.m encpkj(m)A decryption oracle for every key pair 4. A wins if he guesses b correctly.encpki(m0) or encpki(m1)Encryption scheme is IND-CCA secure if this probability is within a negligible factor of ½Simple Protocol LanguagePairing and encryption onlyTerm ::= Id | Identity Key | Public keys onlyNonce |Pair | CiphertextPair ::= (Term, Term)Ciphertext ::= {Term}KeyCan write simple protocols with this syntax•Must describe valid computations of honest parties–For example, (B receives {X}pk(A), B sends {X}pk(B)) is not valid because B can’t decrypt {X}pk(A)Abstract vs. Concrete ExecutionA {Na,A}pk(X) B {Nb,NA}pk(A)A {Nb}pk(X) Abstract execution A bits(m1ex mod nx) B bits(m2ea mod na) A bits(m3ex mod nx)Concrete execution (with RSA)(ex, nx) is responder’s RSA public key; m1 is a number encoding a concatentation of a random bit string representing nonce Na and a fixed bit string representing A’s identity (ea, na) is A’s RSA public key; m2 is a number encoding a concatentation of a random bit string representing nonce Nb and the bit string extracted from the message received by B (ex, nx) is responder’s RSA public key; m3 is a number encoding the bit string extracted from the message received by AAbstract vs. Concrete AdversaryFix some set of corrupt users C. Let M be messages sent prior to some point in protocol execution.• M know(C,M)• If t,t’ know(C,M), then (t,t’) know(C,M)• If (t,t’) know(C,M), then t,t’ know(C,M)• If t know(C,M), then {t}k know(C,M) for any key k Keys- Adversary can access any encryption oracle• If {t}ki know(C,M) and Ai C, then t know(C,M) - Adversary can decrypt only messages encrypted with public keys of corrupt usersAbstract adversary Concrete adversaryAny polynomial-time algorithm (maybe probabilistic)Equivalence of Concrete & AbstractNeed to prove that concrete adversary cannot achieve more than the abstract adversary except with negligible probability•E.g., may guess secret key with negligible probabilityShow that almost any concrete trace is an implementation of some valid abstract trace•Concrete traces represent everything that the concrete adversary can achieve•If almost any concrete trace can be achieved by the abstract adversary, it is sufficient to look only at the abstract adversary when doing analysisConcrete and Abstract Traces Representation function R maps abstract symbols (nonces, keys, identities) to bit strings•Defines concrete “implementation” of abstract protocolConcrete trace is an implementation of an abstract trace if exists a representation function R such that every message in concrete trace is a bit string instantiation of a message in abstract trace•Intuitively, concrete trace is an implementation if it is created by plugging bit strings in place of abstract symbols in the abstract trace •Denote implementation relation as How Can This Fail?A {Na,A}pk(B) B ???Abstract executionA meb mod nb B m2eb mod nb Concrete execution (with RSA)Suppose encryption scheme is malleable•Can change encrypted
View Full Document
Unlocking...