ACTUAL PN 3006 FINAL EXAM COMPLETE REAL QUESTIONS AND CORRECT ANSWERS (100 CORRECT VERIFIED SOLUTIONS) LATEST UPDATED VERSION GUARANTEED PASS.PN 3006 EXAM

Compositional properties of crypto-based components
f f f f




MariafSpichkovafApri

lf18,f2022
arXiv:1405.3006v1 [cs.CR] 13 May 2014




Abstract
Thisf paperf presentsf anf Isabelle/HOL+Isarf [1,f 4]f setf off theoriesfwhic
f




hf allowsf tof specifyf crypto-
basedf componentsf andf tof verifyf theirfcompositionf propertiesf wrt.f crypt
ographicf aspects.f Wef introducef afformalisationfoffthefsecurityfpropertyf
offdatafsecrecy,fthefcorrespond-
f




fingfdefinitionsfandfproofs. f Afpartfoffthesefdefinitionsfisfbasedfonf[3].fPleas

efnotefthatfherefwefimportfherefthefIsabelle/HOLftheoryfListEx-
f




ftras.thy,fpresentedfinf[2].




Contents
f




1 Auxiliaryf dataf types 2

2 Correctnessf off thef relationsf betweenf setsf off Input/Outputfcha
nnels 2

3 Secrecy:f Definitionsf andf properties 4

4 Localf Secretsf off af component 19

5 Knowledgef off Keysf andf Secrets 26




1

,1 Auxiliary data types
f f



theoryfSecrecy-
typesfimportsfMain
f begin



— Wef assumef disjointf sets:f Dataf off dataf values,
— Secretsf off unguessablef values,f Keysf -f setf off cryptographicf keys.
— Basedf onf thesef sets,f wef specifyf thef setsf EncTypef off encryptorsf thatf mayf be
— usedf forf encryptionf orf decryption,f andf Expressionfoff expressionf items.
— Thef specificationf (component)f identifiersf shouldf bef listedf inf thef setf specID,
— thef channelf indentifiersf shouldf bef listedf inf thef setf chanID.

datatypef Keysf =f CKeyf |f CKeyPf |f SKeyf |f SKeyPf |f genKey
datatypef Secretsf =f secretDf |fNf |fNA
type-synonymfVarf =fnat
type-synonymf Dataf =f nat
datatypef KS =f kKSf Keysf |fsKSf Secrets
datatypef EncTypef =f kEncf Keysf |fvEncf Var
datatypef specIDf =f sComp1f |fsComp2f |fsComp3f |fsComp4f datatypef
Expressionf =fkEf Keysf |fsEf Secretsf |fdEf Dataf |fidEf specIDfdatatypefcha
nIDf =fch1f |fch2 |fch3f |fch4

primrecf Expression2KSL::f Expressionf listf ⇒fKSf list
where
Expression2KSLf[]f=f[]f|fExpressi
on2KSLf (xf#xs)f =f ((casefxfoff (k
Efm)f⇒f[kKSfm]
|f (sEf m)f ⇒f [sKSf m]
|f(dEf m)f ⇒f[]
|f (idEf m)f ⇒f [])f @f Expression2KSLf xs)

primrecfKS2Expression::fKSf ⇒fExpression
where
KS2Expressionf (kKSf m)f =f (kEf m)f f |
KS2Expressionf (sKSf m)f =f (sEf m)

end


2 Correctness of the relations between sets of In-
f f f f f f f


put/Output channels
f f



theoryf inoutf import
sfSecrecy-typesfbegin

consts
subcomponentsf ::f specIDf ⇒fspecIDf set




2

,— Mappings,f definingf setsf off input,f local,f andf outputf channels
— off af component
consts
insf::fspecIDf⇒fchanIDfsetflocf
::fspecIDf⇒fchanIDfsetfoutf ::f
specIDf ⇒f chanIDf set

— Predicatef insuringf thef correctf mappingf fromf thef componentf identifier
— tof thef setf off inputf channelsf off af component
definition
inStreamf ::f specIDf ⇒fchanIDf setf ⇒fbool
where
inStreamf xf yf ≡f(insf xf =fy)

— Predicatef insuringf thef correctf mappingf fromf thef componentf identifier
— tof thef setf off localf channelsf off af component
definition
locStreamf ::f specIDf ⇒fchanIDf setf ⇒fbool
where
locStreamfxfyf ≡f(locfxf =fy)

— Predicatef insuringf thef correctf mappingf fromf thef componentf identifier
— tof thef setf off outputf channelsf off af component
definition
outStreamf ::f specIDf ⇒fchanIDf setf ⇒f bool
where
outStreamf xf yf ≡f(outf xf =fy)

— Predicatef insuringf thef correctf relationsf between
— tof thef setf off input,f outputf andf localf channelsf off af component
definition
correctInOutLocf ::f specIDf ⇒fbool
where
correctInOutLocfxf ≡
(insfxf)f∩f(outfxf)f=f{}
∧f(insf xf)f ∩f(locf xf)f=f{}
∧f(locf xf)f ∩f(outf xf)f =f {}

— Predicatef insuringf thef correctf relationsf between
— setsf off inputf channelsf withinf af composedf component
definition
correctCompositionInf ::f specIDf ⇒fbool
where
correctCompositionIn f xf ≡
S
(insf xf)f =f ( S(insf‘f (subcomponentsfxf))f−f(locfxf))
∧f(insfxf)f ∩f( (outf‘f (subcomponentsfxf)))f=f{}

— Predicatef insuringf thef correctf relationsf between


3

, — setsf off outputf channelsf withinf af composedf component
definition
correctCompositionOutf ::f specIDf ⇒fbool
where
correctCompositionOut f xf ≡
S
(outf xf)f =f ( S(outf‘f (subcomponentsfxf))−f(locfxf))
∧f(outf xf)f ∩f( (insf ‘f (subcomponentsf xf)))f =f{}

— Predicatef insuringf thef correctf relationsf between
— setsf off localf channelsf withinf af composedf component
definition
correctCompositionLocf ::f specIDf ⇒fbool
where
correctCompositionLoc fxf ≡
S
(locfxf)f= S (insf ‘f (subcomponentsf xf))
∩ (outf‘f (subcomponentsf xf))

— Iff af componentf isf anf elementaryf onef (hasf nof subcomponents)
— itsf setf off localf channelsf shouldf bef empty
lemmaf subcomponents-loc:
assumesf correctCompositionLocf x
andfsubcomponentsfxf =f{}
showsflocfxf =f{}
usingf assmsf byf (simpf addf:f correctCompositionLoc-deff)

end


3 Secrecy: Definitions and properties
f f f



theoryf Secrecy
importsf Secrecy-typesf inoutf ListExtras
begin

— Encryption,f decryption,f signaturef creationf andf signaturef verificationf functions
— Forfthesef functionsf wef definef onlyftheirf signaturesfandf generalfaxioms,
— becausefinforderftofreasonfeffectively,fwefviewf themfasfabstractffunctionsf and
— abstractf fromf theirf implementationf details
consts
Encf ::fKeysf⇒fExpressionflistf⇒fExpressionflistfDec
rf::fKeysf⇒fExpressionflistf⇒fExpressionflistfSignf::f
Keysf⇒fExpressionflistf⇒fExpressionflistfExtf f ::f Ke
ysf ⇒fExpressionf listf ⇒fExpressionf list

— Axiomsf onf relationsf betweenf encriptionf andf decriptionf keys
axiomatization
EncrDecrKeysf ::f Keysf f ⇒f Keysf ⇒f bool
where
ExtSign:
EncrDecrKeysfK1fK2f −→f(ExtfK1f (SignfK2fEf))f=fEf and


4