资源描述
Click to edit Master title style,Click to edit Master text styles,Second level,Third level,Fourth level,Fifth level,*,Applications of Logic in Computer Security,Jonathan Millen,SRI International,Areas of Application,Multilevel Operating System Security,“Orange Book,Commercial Trusted Product Evaluation,A1-level,Emphasis on secrecy,security/clearance levels,Access Control Policies,Discretionary or role-based policies,Emphasis on application-specific policies,integrity,Public-Key Infrastructure and Trust Management,Network and distributed system security,Digitally signed certificates for identity and privileges,Cryptographic Authentication Protocols,For network communication confidentiality and authentication,Other areas:databases,firewalls/routers,intrusion detection,Computer Security,Network Security,Contributions of Logic,Undecidability Results,Safety problem for discretionary access control,Cryptographic protocol analysis,Theorem Proving Environments,Verifying correctness of formal OS specifications,Inductive proofs of cryptographic protocols,Logic Programming,Prolog programs for cryptographic protocol analysis,trust management,Model Checking,For cryptographic protocol analysis,Specialized Logics,For cryptographic protocol analysis,trust management,Multilevel Operating System Security,Motivated by protection of classified information in shared systems,High-assurance(A1)systems may protect Secret data from uncleared users,Architecture:trusted OS kernel,hardware support,Abstract system model of access control:Bell-LaPadula(ca.1975),Structured state-transition system:subject-object access matrix,levels,Security invariants and transition rules(for OS functions),“Formal Top-Level Specification(FTLS),More detailed state-transition system,Formal Proofs:,Model transitions satisfy invariants,FTLS is an interpretation of the system model,Carried out in environments like Gypsy,FDM,HDM,Some FTLS errors reflected in code were discovered,Of Historical Interest,Access Control Policies,Safety Problem,Subject-object-rights matrix,“rights were arbitrary,representing different kinds of access,Operations:create/delete subjects,objects;enter/remove rights,System of conditional rules to apply operations,Harrison-Ruzzo-Ullman Undecidability Result,Whether S can ever receive right r to object O,Comm.ACM 19(8),1976,Decidable if number of subjects is bounded,Historical Impact,Led to interest in efficiently decidable systems,Take-Grant,DAC,RBAC,O,j,S,i,r,Public-Key Certificates,Based on asymmetric encryption,Key pair KA,KA-1:one made public,one kept secret,Text block encrypted with KA can be decrypted only with KA-1.,Impractical to compute secret key from public key,Digital signature,Text string T,Apply one-way(hash)function,Encrypt with secret key,Verify by decrypting with signers public key,compare hash result,Public Key Certificate,Binds name to public key,signed by trusted party,Logical Equivalent,“A says(KB is the public key of B),provided that KA is the public key of A,T,h(T),h(T)K,A,-1,B,K,B,h(B,K,B,)K,A,-1,Logic of Distributed Authentication,Origination:,“Authentication in distributed systems:theory and practice,by Lampson,Abadi,Burrows,and Wobber,ACM Trans.Comp.Sys.,10(4),1992,Theory of says and speaks for(relation),(A B)(A says s)(B says s)(P8),(A says(B A)(B A)(P10),Application to distributed systems,A and B are principals:users or keys(can say something),A says s means:A authorizes command(operation,access)s,A B means:B delegates authority to A,Certificate T,T KA-1 means KA says T,Public key certificate means KA A,Credentials sent from one network node to another to authorize resources,Implemented in Taos operating system,“credentials,Trust Management,Policymaker,“Decentralized trust management,Blaze,Feigenbaum,Lacy,1996 IEEE Symposium on Security and Privacy,Identified trust management as a distinct problem,Purpose:to define and implement policy using credentials to process queries,Delegation Logic,“A logic-based knowledge representation for Authorization with Delegation,Li,Feigenbaum,Grosof,1999 Computer Security Foundations Workshop,Language to express policies,Primitives include says,delegates(speaks for with object),Access permission is decidable,Logic program implementation(in Datalog),Cryptographic Protocols,Cryptographic protocol,an exchange of messages over an insecure communication medium,using cryptographic transformations to ensure authentication and secrecy of data and keying material.,Applications,military communications,business communications,electronic commerce,privacy,Examples,Kerberos:MIT protocol for unitary login to network services,SSL(Secure Socket Layer,used in Web browsers),IPSec:standard suite of Internet protocols due to the IETF,SET(Secure Electronic Transaction)protocol,PGP(Pretty Good Privacy),A Popular Example,The Needham-Schroeder public-key handshake,R.M.Needham and M.D.Schroeder,“Using Encryption for Authentication in Large Networks of Computers,Comm.ACM,Dec.,1978,A B:A,NaKb,B A:Na,NbKa
展开阅读全文